Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ο be given.
Assume H0: ∀ x2 . and (and (and (x0 ∈ x2) (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ⊆ x3 ⟶ x4 ∈ x2)) (∀ x3 . x3 ∈ x2 ⟶ ∃ x4 . and (x4 ∈ x2) (∀ x5 . x5 ⊆ x3 ⟶ x5 ∈ x4))) (∀ x3 . x3 ⊆ x2 ⟶ or (∃ x4 : ι → ι . bij x3 x2 x4) (x3 ∈ x2)) ⟶ x1.
Apply H0 with prim6 x0.
Apply ZF_closed_E with prim6 x0, and (and (and (x0 ∈ prim6 x0) (∀ x2 . x2 ∈ prim6 x0 ⟶ ∀ x3 . x3 ⊆ x2 ⟶ x3 ∈ prim6 x0)) (∀ x2 . x2 ∈ prim6 x0 ⟶ ∃ x3 . and (x3 ∈ prim6 x0) (∀ x4 . x4 ⊆ x2 ⟶ x4 ∈ x3))) (∀ x2 . x2 ⊆ prim6 x0 ⟶ or (∃ x3 : ι → ι . bij x2 (prim6 x0) x3) (x2 ∈ prim6 x0)) leaving 2 subgoals.
The subproof is completed by applying UnivOf_ZF_closed with x0.
Assume H1: Union_closed (prim6 x0).
Assume H2: Power_closed (prim6 x0).
Assume H3: Repl_closed (prim6 x0).
Apply and4I with x0 ∈ prim6 x0, ∀ x2 . x2 ∈ prim6 x0 ⟶ ∀ x3 . x3 ⊆ x2 ⟶ x3 ∈ prim6 x0, ∀ x2 . x2 ∈ prim6 x0 ⟶ ∃ x3 . and (x3 ∈ prim6 x0) (∀ x4 . x4 ⊆ x2 ⟶ x4 ∈ x3), ∀ x2 . x2 ⊆ prim6 x0 ⟶ or (∃ x3 : ι → ι . bij x2 (prim6 x0) x3) (x2 ∈ prim6 x0) leaving 4 subgoals.
The subproof is completed by applying UnivOf_In with x0.
Let x2 of type ι be given.
Assume H4: x2 ∈ prim6 x0.
Let x3 of type ι be given.
Assume H5: x3 ⊆ x2.
Claim L6: prim4 x2 ∈ prim6 x0
Apply H2 with x2.
The subproof is completed by applying H4.
Claim L7: x3 ∈ prim4 x2
Apply PowerI with x2, x3.
The subproof is completed by applying H5.
Apply UnivOf_TransSet with x0, prim4 x2, x3 leaving 2 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L7.
Let x2 of type ι be given.
Assume H4: x2 ∈ prim6 x0.
Let x3 of type ο be given.
Assume H5: ∀ x4 . and (x4 ∈ prim6 x0) (∀ x5 . x5 ⊆ x2 ⟶ x5 ∈ x4) ⟶ x3.
Apply H5 with prim4 x2.
Apply andI with prim4 x2 ∈ prim6 x0, ∀ x4 . x4 ⊆ x2 ⟶ x4 ∈ prim4 x2 leaving 2 subgoals.
Apply H2 with x2.
The subproof is completed by applying H4.
The subproof is completed by applying PowerI with x2.
Let x2 of type ι be given.
Assume H4: x2 ⊆ prim6 x0.
Apply xm with x2 ∈ prim6 x0, or (∃ x3 : ι → ι . bij x2 (prim6 x0) x3) (x2 ∈ prim6 x0) leaving 2 subgoals.
The subproof is completed by applying orIR with ∃ x3 : ι → ι . bij x2 (prim6 x0) x3, x2 ∈ prim6 x0.
Assume H5: nIn x2 (prim6 x0).
Apply orIL with ∃ x3 : ι → ι . bij ... ... ..., ....
...
■