Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: ZF_closed x0.
Let x1 of type ι be given.
Assume H1: x1 ∈ x0.
Let x2 of type ι be given.
Assume H2: x2 ∈ x0.
Claim L3: {If_i (x1 ∈ x3) x1 x2|x3 ∈ prim4 (prim4 x1)} = UPair x1 x2
Apply set_ext with {If_i (x1 ∈ x3) x1 x2|x3 ∈ prim4 (prim4 x1)}, UPair x1 x2 leaving 2 subgoals.
Let x3 of type ι be given.
Assume H3: x3 ∈ {If_i (x1 ∈ x4) x1 x2|x4 ∈ prim4 (prim4 x1)}.
Apply ReplE_impred with prim4 (prim4 x1), λ x4 . If_i (x1 ∈ x4) x1 x2, x3, x3 ∈ UPair x1 x2 leaving 2 subgoals.
The subproof is completed by applying H3.
Let x4 of type ι be given.
Assume H4: x4 ∈ prim4 (prim4 x1).
Apply xm with x1 ∈ x4, x3 = If_i (x1 ∈ x4) x1 x2 ⟶ x3 ∈ UPair x1 x2 leaving 2 subgoals.
Assume H5: x1 ∈ x4.
Apply If_i_1 with x1 ∈ x4, x1, x2, λ x5 x6 . x3 = x6 ⟶ x3 ∈ UPair x1 x2 leaving 2 subgoals.
The subproof is completed by applying H5.
Assume H6: x3 = x1.
Apply H6 with λ x5 x6 . x6 ∈ UPair x1 x2.
The subproof is completed by applying UPairI1 with x1, x2.
Assume H5: nIn x1 x4.
Apply If_i_0 with x1 ∈ x4, x1, x2, λ x5 x6 . x3 = x6 ⟶ x3 ∈ UPair x1 x2 leaving 2 subgoals.
The subproof is completed by applying H5.
Assume H6: x3 = x2.
Apply H6 with λ x5 x6 . x6 ∈ UPair x1 x2.
The subproof is completed by applying UPairI2 with x1, x2.
Let x3 of type ι be given.
Assume H3: x3 ∈ UPair x1 x2.
Claim L4: ...
...
Claim L5: ...
...
Apply UPairE with x3, x1, x2, x3 ∈ {If_i (x1 ∈ x4) x1 x2|x4 ∈ prim4 (prim4 x1)} leaving 3 subgoals.
The subproof is completed by applying H3.
Assume H6: x3 = x1.
Apply H6 with λ x4 x5 . x5 ∈ {If_i (x1 ∈ x6) x1 x2|x6 ∈ prim4 (prim4 x1)}.
Apply If_i_1 with x1 ∈ prim4 x1, x1, x2, λ x4 x5 . x4 ∈ {...|x6 ∈ prim4 ...} leaving 2 subgoals.
...
...
...
Apply L3 with λ x3 x4 . x3 ∈ x0.
Claim L4: prim4 (prim4 x1) ∈ x0
Apply ZF_Power_closed with x0, prim4 x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply ZF_Power_closed with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Claim L5: ∀ x3 . x3 ∈ prim4 (prim4 x1) ⟶ If_i (x1 ∈ x3) x1 x2 ∈ x0
Let x3 of type ι be given.
Assume H5: x3 ∈ prim4 (prim4 x1).
Apply xm with x1 ∈ x3, If_i (x1 ∈ x3) x1 x2 ∈ x0 leaving 2 subgoals.
Assume H6: x1 ∈ x3.
Apply If_i_1 with x1 ∈ x3, x1, x2, λ x4 x5 . x5 ∈ x0 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H1.
Assume H6: nIn x1 x3.
Apply If_i_0 with x1 ∈ x3, x1, x2, λ x4 x5 . x5 ∈ x0 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H2.
Apply ZF_Repl_closed with x0, prim4 (prim4 x1), λ x3 . If_i (x1 ∈ x3) x1 x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L4.
The subproof is completed by applying L5.
■