Let x0 of type ι be given.

Let x1 of type (ι → ο) → ο be given.

Let x2 of type ι → ο be given.

Assume H0: ∀ x3 . x2 x3 ⟶ x3 ∈ x0.

Apply prop_ext_2 with decode_c (encode_c x0 x1) x2, x1 x2 leaving 2 subgoals.

Assume H1: decode_c (encode_c x0 x1) x2.

Apply H1 with x1 x2.

Let x3 of type ι be given.

Assume H2: (λ x4 . and (∀ x5 . iff (x2 x5) (x5 ∈ x4)) (x4 ∈ encode_c x0 x1)) x3.

Apply H2 with x1 x2.

Assume H3: ∀ x4 . iff (x2 x4) (x4 ∈ x3).

Assume H4: x3 ∈ encode_c x0 x1.

Claim L5: x1 (λ x4 . x4 ∈ x3)

Apply SepE2 with prim4 x0, λ x4 . x1 (λ x5 . x5 ∈ x4), x3.

The subproof is completed by applying H4.

Claim L6: (λ x4 . x4 ∈ x3) = x2

Apply pred_ext_2 with λ x4 . x4 ∈ x3, x2 leaving 2 subgoals.

Let x4 of type ι be given.

Apply H3 with x4, (λ x5 . x5 ∈ x3) x4 ⟶ x2 x4.

Assume H6: x2 x4 ⟶ x4 ∈ x3.

Assume H7: x4 ∈ x3 ⟶ x2 x4.

The subproof is completed by applying H7.

Let x4 of type ι be given.

Apply H3 with x4, x2 x4 ⟶ (λ x5 . x5 ∈ x3) x4.

Assume H6: x2 x4 ⟶ x4 ∈ x3.

Assume H7: x4 ∈ x3 ⟶ x2 x4.

The subproof is completed by applying H6.

Apply L6 with λ x4 x5 : ι → ο . x1 x4.

The subproof is completed by applying L5.

Assume H1: x1 x2.

Let x3 of type ο be given.

Assume H2: ∀ x4 . and (∀ x5 . iff (x2 x5) (x5 ∈ x4)) (x4 ∈ encode_c x0 x1) ⟶ x3.

Apply H2 with Sep x0 x2.

Apply andI with ∀ x4 . iff (x2 x4) (x4 ∈ Sep x0 x2), Sep x0 x2 ∈ encode_c x0 x1 leaving 2 subgoals.

Let x4 of type ι be given.

Apply iffI with x2 x4, x4 ∈ Sep x0 x2 leaving 2 subgoals.

Assume H3: x2 x4.

Apply SepI with x0, x2, x4 leaving 2 subgoals.

Apply H0 with x4.

The subproof is completed by applying H3.

Assume H3: x4 ∈ Sep x0 x2.

Apply SepE2 with x0, x2, x4.

The subproof is completed by applying H3.

Apply SepI with prim4 x0, λ x4 . x1 (λ x5 . x5 ∈ x4), Sep x0 x2 leaving 2 subgoals.

The subproof is completed by applying Sep_In_Power with x0, x2.

Claim L3: x2 = λ x4 . x4 ∈ Sep x0 x2

Apply pred_ext_2 with x2, λ x4 . x4 ∈ Sep x0 x2 leaving 2 subgoals.

Let x4 of type ι be given.

Assume H3: x2 x4.

Apply SepI with x0, x2, x4 leaving 2 subgoals.

Apply H0 with x4.

The subproof is completed by applying H3.

Let x4 of type ι be given.

Assume H3: x4 ∈ Sep x0 x2.

Apply SepE2 with x0, x2, x4.

The subproof is completed by applying H3.

Apply L3 with λ x4 x5 : ι → ο . x1 x4.

The subproof is completed by applying H1.

■

Proofgold Proof