Claim L0: ∀ x0 . IrreflexiveTransitiveReln x0 ⟶ struct_r x0

Let x0 of type ι be given.

Assume H0: IrreflexiveTransitiveReln x0.

Apply H0 with struct_r x0.

Assume H1: struct_r x0.

Assume H2: unpack_r_o x0 (λ x1 . λ x2 : ι → ι → ο . and (∀ x3 . x3 ∈ x1 ⟶ not (x2 x3 x3)) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x5 ⟶ x2 x3 x5)).

The subproof is completed by applying H1.

Claim L1: ∀ x0 x1 x2 x3 . IrreflexiveTransitiveReln x0 ⟶ IrreflexiveTransitiveReln x1 ⟶ BinRelnHom x0 x1 x2 ⟶ BinRelnHom x0 x1 x3 ⟶ IrreflexiveTransitiveReln (05907.. x0 x1 x2 x3)

Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H1: IrreflexiveTransitiveReln x0.

Assume H2: IrreflexiveTransitiveReln x1.

Assume H3: BinRelnHom x0 x1 x2.

Assume H4: BinRelnHom x0 x1 x3.

Apply unknownprop_2d7c7a9916fa2967cfb4d546f4e37c43b64368ed4a60618379328e066e9b7e0e with x0, λ x4 . IrreflexiveTransitiveReln (05907.. x4 x1 x2 x3) leaving 2 subgoals.

The subproof is completed by applying H1.

Let x4 of type ι be given.

Let x5 of type ι → ι → ο be given.

Assume H5: ∀ x6 . x6 ∈ x4 ⟶ not (x5 x6 x6).

Assume H6: ∀ x6 . x6 ∈ x4 ⟶ ∀ x7 . x7 ∈ x4 ⟶ ∀ x8 . x8 ∈ x4 ⟶ x5 x6 x7 ⟶ x5 x7 x8 ⟶ x5 x6 x8.

Apply unknownprop_f1f0d0235cc3f72918ba3b7bc6e671feb556f667a17378616f96007dc95611ad with x4, x5, x1, x2, x3, λ x6 x7 . IrreflexiveTransitiveReln x7.

Apply unknownprop_dbb6377af3127d2bf8cd888143d856b4a86f0ec975822a440e0313d91ee07474 with {x6 ∈ x4|ap x2 x6 = ap x3 x6}, x5 leaving 2 subgoals.

Let x6 of type ι be given.

Assume H7: x6 ∈ {x7 ∈ x4|ap x2 x7 = ap x3 x7}.

Apply H5 with x6.

Apply SepE1 with x4, λ x7 . ap x2 x7 = ap x3 x7, x6.

The subproof is completed by applying H7.

Let x6 of type ι be given.

Assume H7: x6 ∈ {x7 ∈ x4|ap x2 x7 = ap x3 x7}.

Let x7 of type ι be given.

Assume H8: x7 ∈ {x8 ∈ x4|ap x2 x8 = ap x3 x8}.

Let x8 of type ι be given.

Assume H9: x8 ∈ {x9 ∈ x4|ap x2 x9 = ap x3 x9}.

Assume H10: x5 x6 x7.

Assume H11: x5 x7 x8.

Apply H6 with x6, x7, x8 leaving 5 subgoals.

Apply SepE1 with x4, λ x9 . ap x2 x9 = ap x3 x9, x6.

The subproof is completed by applying H7.

Apply SepE1 with x4, λ x9 . ap x2 x9 = ap x3 x9, x7.

The subproof is completed by applying H8.

Apply SepE1 with x4, λ x9 . ap x2 x9 = ap x3 x9, x8.

The subproof is completed by applying H9.

The subproof is completed by applying H10.

The subproof is completed by applying H11.

Apply unknownprop_2aabccf4699c9f902dcc37be8ad1f3aaa001e5f2bb081556c38a4bbd69d3e5c6 with IrreflexiveTransitiveReln leaving 2 subgoals.

The subproof is completed by applying L0.

The subproof is completed by applying L1.

■

Proofgold Proof