Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: ordinal x0.
Let x1 of type ι → ο be given.
Apply H0 with PNoEq_ x0 x1 (ce2d5.. (7eb85.. x0 x1) (0dfb2.. x0 x1)).
Assume H1: TransSet x0.
Assume H2: ∀ x2 . prim1 x2 x0 ⟶ TransSet x2.
Claim L3: ...
...
Apply unknownprop_6419f8fc1ff70ca950cf4e79a0f0cff9b9f9b876ea55c76aec20f2ed9adc5971 with 7eb85.. x0 x1, 0dfb2.. x0 x1, x0, PNoEq_ x0 x1 (ce2d5.. (7eb85.. x0 x1) (0dfb2.. x0 x1)) leaving 5 subgoals.
Apply unknownprop_f108c6778b2486326f32d399bd20304abef55d1e47d936156e37eb3983681f51 with x0, x1.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_b1db2370d04eeb6178d052b730fcb6295924aa036f14aa30a1494605521002e1 with x0, x1.
The subproof is completed by applying unknownprop_4a256b444b1c01564b66b1b28907359637ea99a833a2704a9682d62018db7ca5 with x0, x1.
Claim L4: ...
...
Apply L4 with λ x2 x3 . and (ordinal x3) (47618.. (7eb85.. x0 x1) (0dfb2.. x0 x1) x3 (ce2d5.. (7eb85.. x0 x1) (0dfb2.. x0 x1))) ⟶ (∀ x4 . prim1 x4 x3 ⟶ ∀ x5 : ι → ο . not (47618.. (7eb85.. x0 x1) (0dfb2.. x0 x1) x4 x5)) ⟶ PNoEq_ x0 x1 (ce2d5.. (7eb85.. x0 x1) (0dfb2.. x0 x1)).
Assume H5: and (ordinal x0) (47618.. (7eb85.. x0 x1) (0dfb2.. x0 x1) x0 (ce2d5.. (7eb85.. x0 x1) (0dfb2.. x0 x1))).
Apply H5 with (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 : ι → ο . not (47618.. (7eb85.. x0 x1) (0dfb2.. x0 x1) x2 x3)) ⟶ PNoEq_ x0 x1 (ce2d5.. (7eb85.. x0 x1) (0dfb2.. x0 x1)).
Assume H6: ordinal x0.
Assume H7: 47618.. (7eb85.. x0 x1) (0dfb2.. x0 x1) x0 (ce2d5.. (7eb85.. x0 x1) (0dfb2.. x0 x1)).
Assume H8: ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 : ι → ο . not (47618.. (7eb85.. x0 x1) (0dfb2.. x0 x1) x2 x3).
Apply H7 with PNoEq_ x0 x1 (ce2d5.. (7eb85.. x0 x1) (0dfb2.. x0 x1)).
Assume H9: cae4c.. (7eb85.. x0 x1) x0 (ce2d5.. (7eb85.. x0 x1) (0dfb2.. x0 x1)).
Assume H10: bc2b0.. (0dfb2.. x0 x1) x0 (ce2d5.. (7eb85.. x0 x1) (0dfb2.. x0 x1)).
Claim L11: ∀ x2 . ordinal x2 ⟶ prim1 x2 x0 ⟶ iff (x1 x2) (ce2d5.. (7eb85.. x0 x1) (0dfb2.. x0 x1) x2)
Apply ordinal_ind with λ x2 . prim1 x2 x0 ⟶ iff (x1 x2) (ce2d5.. (7eb85.. x0 x1) (0dfb2.. x0 x1) x2).
Let x2 of type ι be given.
Assume H11: ordinal x2.
Assume H12: ∀ x3 . ... ⟶ ... ⟶ iff (x1 x3) (ce2d5.. (7eb85.. ... ...) ... ...).
...
Let x2 of type ι be given.
Assume H12: prim1 x2 x0.
Apply L11 with x2 leaving 2 subgoals.
Apply ordinal_Hered with x0, x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H12.
The subproof is completed by applying H12.
■