Claim L0: ∀ x0 . PER x0 ⟶ struct_r x0

Let x0 of type ι be given.

Assume H0: PER x0.

Apply H0 with struct_r x0.

Assume H1: struct_r x0.

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

...

Claim L1: ∀ x0 x1 x2 x3 . PER x0 ⟶ PER x1 ⟶ BinRelnHom x0 x1 x2 ⟶ BinRelnHom x0 x1 x3 ⟶ PER (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: PER x0.

Assume H2: PER x1.

Assume H3: BinRelnHom x0 x1 x2.

Assume H4: BinRelnHom x0 x1 x3.

Apply unknownprop_c1d3826129d2eb54a8f1e40a6116497a0cdb00a6ee455a0b01d56d09477d50d0 with x0, λ x4 . PER (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 ⟶ ∀ x7 . x7 ∈ x4 ⟶ x5 x6 x7 ⟶ x5 x7 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 . PER x7.

Apply unknownprop_b2515235786361aea7c15ac6711d5751cd13b11988163a3b347abdb56aff828a 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}.

Let x7 of type ι be given.

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

Assume H9: x5 x6 x7.

Apply H5 with x6, x7 leaving 3 subgoals.

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

The subproof is completed by applying H7.

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

The subproof is completed by applying H8.

The subproof is completed by applying H9.

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 PER leaving 2 subgoals.

The subproof is completed by applying L0.

The subproof is completed by applying L1.

■

Proofgold Proof