Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: ∀ x1 . x1x0ordinal x1.
Apply andI with TransSet (prim3 x0), ∀ x1 . x1prim3 x0TransSet x1 leaving 2 subgoals.
Let x1 of type ι be given.
Assume H1: x1prim3 x0.
Apply UnionE_impred with x0, x1, x1prim3 x0 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H2: x1x2.
Assume H3: x2x0.
Claim L4: ordinal x2
Apply H0 with x2.
The subproof is completed by applying H3.
Apply L4 with x1prim3 x0.
Assume H5: TransSet x2.
Assume H6: ∀ x3 . x3x2TransSet x3.
Let x3 of type ι be given.
Assume H7: x3x1.
Claim L8: x3x2
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: x1prim3 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: x1x2.
Assume H3: x2x0.
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 . x3x1TransSet x3.
The subproof is completed by applying H6.