Search for blocks/addresses/...

Proofgold Proof

pf
Apply In_ind with λ x0 . ∀ x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (or (prim1 x0 x1) (x0 = x1)) (prim1 x1 x0).
Let x0 of type ι be given.
Assume H0: ∀ x1 . prim1 x1 x0 ⟶ ∀ x2 . ordinal x1 ⟶ ordinal x2 ⟶ or (or (prim1 x1 x2) (x1 = x2)) (prim1 x2 x1).
Apply In_ind with λ x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (or (prim1 x0 x1) (x0 = x1)) (prim1 x1 x0).
Let x1 of type ι be given.
Assume H1: ∀ x2 . prim1 x2 x1 ⟶ ordinal x0 ⟶ ordinal x2 ⟶ or (or (prim1 x0 x2) (x0 = x2)) (prim1 x2 x0).
Assume H2: ordinal x0.
Assume H3: ordinal x1.
Apply xm with prim1 x0 x1, or (or (prim1 x0 x1) (x0 = x1)) (prim1 x1 x0) leaving 2 subgoals.
Assume H4: prim1 x0 x1.
Apply or3I1 with prim1 x0 x1, x0 = x1, prim1 x1 x0.
The subproof is completed by applying H4.
Assume H4: nIn x0 x1.
Apply xm with prim1 x1 x0, or (or (prim1 x0 x1) (x0 = x1)) (prim1 x1 x0) leaving 2 subgoals.
Assume H5: prim1 x1 x0.
Apply or3I3 with prim1 x0 x1, x0 = x1, prim1 x1 x0.
The subproof is completed by applying H5.
Assume H5: nIn x1 x0.
Apply or3I2 with prim1 x0 x1, x0 = x1, prim1 x1 x0.
Apply set_ext with x0, x1 leaving 2 subgoals.
Let x2 of type ι be given.
Assume H6: prim1 x2 x0.
Claim L7: ordinal x2
Apply ordinal_Hered with x0, x2 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H6.
Apply or3E with prim1 x2 x1, x2 = x1, prim1 x1 x2, prim1 x2 x1 leaving 4 subgoals.
Apply H0 with x2, x1 leaving 3 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying L7.
The subproof is completed by applying H3.
Assume H8: prim1 x2 x1.
The subproof is completed by applying H8.
Assume H8: x2 = x1.
Apply FalseE with prim1 x2 x1.
Apply H5.
Apply H8 with λ x3 x4 . prim1 x3 x0.
The subproof is completed by applying H6.
Assume H8: prim1 x1 x2.
Apply FalseE with prim1 x2 x1.
Apply H5.
Apply ordinal_TransSet with x0, x2, x1 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H6.
The subproof is completed by applying H8.
Let x2 of type ι be given.
Assume H6: prim1 x2 x1.
Claim L7: ordinal x2
Apply ordinal_Hered with x1, x2 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H6.
Apply or3E with prim1 x0 x2, x0 = x2, prim1 x2 x0, prim1 x2 x0 leaving 4 subgoals.
Apply H1 with x2 leaving 3 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H2.
The subproof is completed by applying L7.
Assume H8: prim1 x0 x2.
Apply FalseE with prim1 x2 x0.
Apply H4.
Apply ordinal_TransSet with x1, x2, x0 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H6.
The subproof is completed by applying H8.
Assume H8: x0 = x2.
Apply FalseE with prim1 x2 x0.
Apply H4.
Apply H8 with λ x3 x4 . prim1 x4 x1.
The subproof is completed by applying H6.
Assume H8: prim1 x2 x0.
The subproof is completed by applying H8.
■