Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ιο be given.
Assume H0: ∃ x1 . and (ordinal x1) (x0 x1).
Apply dneg with ∃ x1 . and (and (ordinal x1) (x0 x1)) (∀ x2 . prim1 x2 x1not (x0 x2)).
Assume H1: not (∃ x1 . and (and (ordinal x1) (x0 x1)) (∀ x2 . prim1 x2 x1not (x0 x2))).
Claim L2: ∀ x1 . ordinal x1not (x0 x1)
Apply ordinal_ind with λ x1 . not (x0 x1).
Let x1 of type ι be given.
Assume H2: ordinal x1.
Assume H3: ∀ x2 . prim1 x2 x1not (x0 x2).
Assume H4: x0 x1.
Apply H1.
Let x2 of type ο be given.
Assume H5: ∀ x3 . and (and (ordinal x3) (x0 x3)) (∀ x4 . prim1 x4 x3not (x0 x4))x2.
Apply H5 with x1.
Apply and3I with ordinal x1, x0 x1, ∀ x3 . prim1 x3 x1not (x0 x3) leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H4.
The subproof is completed by applying H3.
Apply H0 with False.
Let x1 of type ι be given.
Assume H3: (λ x2 . and (ordinal x2) (x0 x2)) x1.
Apply H3 with False.
Assume H4: ordinal x1.
Assume H5: x0 x1.
Apply L2 with x1 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.