Search for blocks/addresses/...

Proofgold Proof

pf
Apply In_ind with λ x0 . ∀ x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (or (x0 ∈ x1) (x0 = x1)) (x1 ∈ x0).
Let x0 of type ι be given.
Assume H0: ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . ordinal x1 ⟶ ordinal x2 ⟶ or (or (x1 ∈ x2) (x1 = x2)) (x2 ∈ x1).
Apply In_ind with λ x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (or (x0 ∈ x1) (x0 = x1)) (x1 ∈ x0).
Let x1 of type ι be given.
Assume H1: ∀ x2 . x2 ∈ x1 ⟶ ordinal x0 ⟶ ordinal x2 ⟶ or (or (x0 ∈ x2) (x0 = x2)) (x2 ∈ x0).
Assume H2: ordinal x0.
Assume H3: ordinal x1.
Apply xm with x0 ∈ x1, or (or (x0 ∈ x1) (x0 = x1)) (x1 ∈ x0) leaving 2 subgoals.
Assume H4: x0 ∈ x1.
Apply or3I1 with x0 ∈ x1, x0 = x1, x1 ∈ x0.
The subproof is completed by applying H4.
Assume H4: nIn x0 x1.
Apply xm with x1 ∈ x0, or (or (x0 ∈ x1) (x0 = x1)) (x1 ∈ x0) leaving 2 subgoals.
Assume H5: x1 ∈ x0.
Apply or3I3 with x0 ∈ x1, x0 = x1, x1 ∈ x0.
The subproof is completed by applying H5.
Assume H5: nIn x1 x0.
Apply or3I2 with x0 ∈ x1, x0 = x1, x1 ∈ x0.
Apply set_ext with x0, x1 leaving 2 subgoals.
Let x2 of type ι be given.
Assume H6: 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 x2 ∈ x1, x2 = x1, x1 ∈ x2, 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: x2 ∈ x1.
The subproof is completed by applying H8.
Assume H8: x2 = x1.
Apply FalseE with x2 ∈ x1.
Apply H5.
Apply H8 with λ x3 x4 . x3 ∈ x0.
The subproof is completed by applying H6.
Assume H8: x1 ∈ x2.
Apply FalseE with 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: 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 x0 ∈ x2, x0 = x2, x2 ∈ x0, 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: x0 ∈ x2.
Apply FalseE with 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 x2 ∈ x0.
Apply H4.
Apply H8 with λ x3 x4 . x4 ∈ x1.
The subproof is completed by applying H6.
Assume H8: x2 ∈ x0.
The subproof is completed by applying H8.
■