Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: ∀ x1 . prim1 x1 x0 ⟶ ordinal x1.
Apply andI with TransSet (prim3 x0), ∀ x1 . prim1 x1 (prim3 x0) ⟶ TransSet x1 leaving 2 subgoals.
Let x1 of type ι be given.
Assume H1: prim1 x1 (prim3 x0).
Apply UnionE_impred with x0, x1, Subq x1 (prim3 x0) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H2: prim1 x1 x2.
Assume H3: prim1 x2 x0.
Claim L4: ordinal x2
Apply H0 with x2.
The subproof is completed by applying H3.
Apply L4 with Subq x1 (prim3 x0).
Assume H5: TransSet x2.
Assume H6: ∀ x3 . prim1 x3 x2 ⟶ TransSet x3.
Let x3 of type ι be given.
Assume H7: prim1 x3 x1.
Claim L8: prim1 x3 x2
Apply H5 with x1, x3 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H7.
Apply UnionI with x0, x3, x2 leaving 2 subgoals.
The subproof is completed by applying L8.
The subproof is completed by applying H3.
Let x1 of type ι be given.
Assume H1: prim1 x1 (prim3 x0).
Apply UnionE_impred with x0, x1, TransSet x1 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H2: prim1 x1 x2.
Assume H3: prim1 x2 x0.
Claim L4: ordinal x2
Apply H0 with x2.
The subproof is completed by applying H3.
Claim L5: ordinal x1
Apply ordinal_Hered with x2, x1 leaving 2 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying H2.
Apply L5 with TransSet x1.
Assume H6: TransSet x1.
Assume H7: ∀ x3 . prim1 x3 x1 ⟶ TransSet x3.
The subproof is completed by applying H6.
■