Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Assume H0: ∀ x2 . prim1 x2 x0 ⟶ ordinal (x1 x2).
Apply andI with TransSet (a842e.. x0 (λ x2 . x1 x2)), ∀ x2 . prim1 x2 (a842e.. x0 (λ x3 . x1 x3)) ⟶ TransSet x2 leaving 2 subgoals.
Let x2 of type ι be given.
Assume H1: prim1 x2 (a842e.. x0 (λ x3 . x1 x3)).
Apply unknownprop_6e713ef2b1c9d2089dead8e3d98fed6bda91ffc6b807ed8732c89724a15f5c2c with x0, x1, x2, Subq x2 (a842e.. x0 x1) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x3 of type ι be given.
Assume H2: (λ x4 . and (prim1 x4 x0) (prim1 x2 (x1 x4))) x3.
Apply H2 with Subq x2 (a842e.. x0 x1).
Assume H3: prim1 x3 x0.
Assume H4: prim1 x2 (x1 x3).
Claim L5: ordinal (x1 x3)
Apply H0 with x3.
The subproof is completed by applying H3.
Apply L5 with Subq x2 (a842e.. x0 (λ x4 . x1 x4)).
Assume H6: TransSet (x1 x3).
Assume H7: ∀ x4 . prim1 x4 (x1 x3) ⟶ TransSet x4.
Let x4 of type ι be given.
Assume H8: prim1 x4 x2.
Claim L9: prim1 x4 (x1 x3)
Apply H6 with x2, x4 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H8.
Apply unknownprop_1a58846f991745a62bb791e57f6ffb9f18f2ca362367c10b2b979fc90a3b62e1 with x0, x1, x3, x4 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying L9.
Let x2 of type ι be given.
Assume H1: prim1 x2 (a842e.. x0 (λ x3 . x1 x3)).
Apply unknownprop_6e713ef2b1c9d2089dead8e3d98fed6bda91ffc6b807ed8732c89724a15f5c2c with x0, x1, x2, TransSet x2 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x3 of type ι be given.
Assume H2: (λ x4 . and (prim1 x4 x0) (prim1 x2 (x1 x4))) x3.
Apply H2 with TransSet x2.
Assume H3: prim1 x3 x0.
Assume H4: prim1 x2 (x1 x3).
Claim L5: ordinal (x1 x3)
Apply H0 with x3.
The subproof is completed by applying H3.
Claim L6: ordinal x2
Apply ordinal_Hered with x1 x3, x2 leaving 2 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying H4.
Apply L6 with TransSet x2.
Assume H7: TransSet x2.
Assume H8: ∀ x4 . prim1 x4 x2 ⟶ TransSet x4.
The subproof is completed by applying H7.
■