Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: equip x0 x1.

Apply unknownprop_f82d0f217e1b2a36bc273d145ee21e9b9e753d654bb0c650cc08860c1b4bd1f0 with x0, x1, equip (Power x0) (Power x1) leaving 2 subgoals.

The subproof is completed by applying H0.

Let x2 of type ι → ι be given.

Assume H1: bij x0 x1 x2.

Apply unknownprop_db24d9aa1dc52b3c0eaf7cf69655226164a8ab5afc5d72e14a32016133f537ca with x0, x1, x2, equip (Power x0) (Power x1) leaving 2 subgoals.

The subproof is completed by applying H1.

Assume H2: inj x0 x1 x2.

Apply unknownprop_6a8f953ba7c3bf327e583b76a91b24ddd499843a498fbfe2514e26f3800e68b3 with x0, x1, x2, (∀ x3 . In x3 x1 ⟶ ∃ x4 . and (In x4 x0) (x2 x4 = x3)) ⟶ equip (Power x0) (Power x1) leaving 2 subgoals.

The subproof is completed by applying H2.

Assume H3: ∀ x3 . In x3 x0 ⟶ In (x2 x3) x1.

Assume H4: ∀ x3 . In x3 x0 ⟶ ∀ x4 . In x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4.

Assume H5: ∀ x3 . In x3 x1 ⟶ ∃ x4 . and (In x4 x0) (x2 x4 = x3).

Apply unknownprop_4b95783dcb3eee1943e1de5542f675166ef402c8fbdda80bdf0920b55d3fc6de with Power x0, Power x1, λ x3 . Repl x3 (λ x4 . x2 x4).

Apply unknownprop_aa42ade5598d8612d2029318c4ed81646c550ecc6cdd9ab953ce4bf73f3dd562 with Power x0, Power x1, λ x3 . Repl x3 (λ x4 . x2 x4) leaving 2 subgoals.

Apply unknownprop_57c8600e4bc6abecef2ae17962906fa2de1fc16f5d46ed100ff99cd5b67f5b1b with Power x0, Power x1, λ x3 . Repl x3 (λ x4 . x2 x4) leaving 2 subgoals.

Let x3 of type ι be given.

Assume H6: In x3 (Power x0).

Claim L7: ∀ x4 . In x4 x3 ⟶ In x4 x0

Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with x3, x0.

Apply unknownprop_b8811722bb772bba243207d8ee471ba24f8b88e821f7737307414168e638d2c6 with x0, x3.

The subproof is completed by applying H6.

Apply unknownprop_9a40b4678ae1931e61346f9ab9e405ec760f2f9d44b3be548b52a8b2ddb78559 with x1, (λ x4 . Repl x4 (λ x5 . x2 x5)) x3.

Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with (λ x4 . Repl x4 (λ x5 . x2 x5)) x3, x1.

Let x4 of type ι be given.

Assume H8: In x4 (Repl x3 (λ x5 . x2 x5)).

Apply unknownprop_89e422bb3b8a01dd209d7f2f210df650a435fc3e6005e0f59c57a5e7a59a6d0e with x3, x2, x4, In x4 x1 leaving 2 subgoals.

The subproof is completed by applying H8.

Let x5 of type ι be given.

Assume H9: In x5 x3.

Assume H10: x4 = x2 x5.

Apply H10 with λ x6 x7 . In x7 x1.

Apply H3 with x5.

Apply L7 with x5.

The subproof is completed by applying H9.

Let x3 of type ι be given.

Assume H6: In x3 (Power x0).

Let x4 of type ι be given.

Assume H7: In x4 (Power x0).

Assume H8: Repl x3 (λ x5 . x2 x5) = Repl x4 (λ x5 . x2 x5).

Claim L9: ...

...

Claim L10: ...

...

Apply unknownprop_219a5692ece616b4a88502d80a85b644180cde982b21251f92a23d11d1a5d022 with x3, x4 leaving 2 subgoals.

Let x5 of type ι be given.

Assume H11: In x5 x3.

Claim L12: In (x2 x5) (Repl x4 (λ x6 . x2 x6))

Apply H8 with λ x6 x7 . In (x2 x5) x6.

Apply unknownprop_63c308b92260dbfca8c9530846e6836ba3e6be221cc8e80fd61db913e01bdacf with x3, x2, x5.

The subproof is completed by applying H11.

Apply unknownprop_89e422bb3b8a01dd209d7f2f210df650a435fc3e6005e0f59c57a5e7a59a6d0e with x4, x2, x2 x5, In x5 x4 leaving 2 subgoals.

The subproof is completed by applying L12.

Let x6 of type ι be given.

Assume H13: In x6 x4.

Assume H14: x2 x5 = x2 x6.

Apply H4 with x5, x6, λ x7 x8 . In x8 x4 leaving 4 subgoals.

Apply L9 with x5.

The subproof is completed by applying H11.

Apply L10 with x6.

The subproof is completed by applying H13.

The subproof is completed by applying H14.

The subproof is completed by applying H13.

Let x5 of type ι be given.

Assume H11: In x5 x4.

Claim L12: ...

...

Apply unknownprop_89e422bb3b8a01dd209d7f2f210df650a435fc3e6005e0f59c57a5e7a59a6d0e with x3, x2, x2 x5, ... leaving 2 subgoals.

...

■

Proofgold Proof