Apply unknownprop_3e781d8ea4d49c4a007227d9d77ed61640aac8afd19249eaf961cfbd99889c85 with λ x0 x1 : ι → ι . ∀ x2 . x1 x2 = famunion x2 (λ x3 . Power (x1 x3)).

Claim L0: ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . In x3 x0 ⟶ x1 x3 = x2 x3) ⟶ Subq (famunion x0 (λ x3 . Power (x1 x3))) (famunion x0 (λ x3 . Power (x2 x3)))

Let x0 of type ι be given.

Let x1 of type ι → ι be given.

Let x2 of type ι → ι be given.

Assume H0: ∀ x3 . In x3 x0 ⟶ x1 x3 = x2 x3.

Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with famunion x0 (λ x3 . Power (x1 x3)), famunion x0 (λ x3 . Power (x2 x3)).

Let x3 of type ι be given.

Assume H1: In x3 (famunion x0 (λ x4 . Power (x1 x4))).

Apply unknownprop_6aa6a1e2972a64fa9285a0890d0ac4772ddcd8c250de1b168f8abb7d1edde683 with x0, λ x4 . Power (x1 x4), x3, In x3 (famunion x0 (λ x4 . Power (x2 x4))) leaving 2 subgoals.

The subproof is completed by applying H1.

Let x4 of type ι be given.

Assume H2: and (In x4 x0) (In x3 (Power (x1 x4))).

Apply andE with In x4 x0, In x3 (Power (x1 x4)), In x3 (famunion x0 (λ x5 . Power (x2 x5))) leaving 2 subgoals.

The subproof is completed by applying H2.

Assume H3: In x4 x0.

Assume H4: In x3 (Power (x1 x4)).

Apply unknownprop_4d9a081a15fdc79c67eee9fe67650a775bc97737c16f9cc2a1a6fdd7a2cc8108 with x0, λ x5 . Power (x2 x5), x4, x3 leaving 2 subgoals.

The subproof is completed by applying H3.

Apply H0 with x4, λ x5 x6 . In x3 (Power x5) leaving 2 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H4.

Claim L1: ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . In x3 x0 ⟶ x1 x3 = x2 x3) ⟶ famunion x0 (λ x3 . Power (x1 x3)) = famunion x0 (λ x3 . Power (x2 x3))

Let x0 of type ι be given.

Let x1 of type ι → ι be given.

Let x2 of type ι → ι be given.

Assume H1: ∀ x3 . In x3 x0 ⟶ x1 x3 = x2 x3.

Apply unknownprop_a23ec6a55ac212526d74cbf0d04096929ad453b0eb0f8023e32b8a33930d39fb with famunion x0 (λ x3 . Power (x1 x3)), famunion x0 (λ x3 . Power (x2 x3)) leaving 2 subgoals.

Apply L0 with x0, x1, x2.

The subproof is completed by applying H1.

Apply L0 with x0, x2, x1.

Let x3 of type ι be given.

Assume H2: In x3 x0.

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

Apply H1 with x3, λ x5 x6 . x4 x6 x5.

The subproof is completed by applying H2.

Apply unknownprop_b46ce29ff1d7f9d2e6d60e6a0f6f0736a07c8ba94a4f18feca3e51921a7ff153 with λ x0 . λ x1 : ι → ι . famunion x0 (λ x2 . Power (x1 x2)).

The subproof is completed by applying L1.

■

Proofgold Proof