Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → (ι → ο) → ο be given.
Let x1 of type ι → (ι → ο) → ο be given.
Let x2 of type ι be given.
Assume H0: ordinal x2.
Apply H0 with PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ ∀ x3 : ι → ο . PNo_rel_strict_imv x0 x1 x2 x3 ⟶ PNo_rel_strict_imv x0 x1 (ordsucc x2) (λ x4 . or (x3 x4) (x4 = x2)).
Assume H1: TransSet x2.
Assume H2: ∀ x3 . x3 ∈ x2 ⟶ TransSet x3.
Assume H3: PNo_lenbdd x2 x0.
Assume H4: PNo_lenbdd x2 x1.
Let x3 of type ι → ο be given.
Assume H5: PNo_rel_strict_imv x0 x1 x2 x3.
Apply H5 with PNo_rel_strict_imv x0 x1 (ordsucc x2) (λ x4 . or (x3 x4) (x4 = x2)).
Assume H6: PNo_rel_strict_upperbd x0 x2 x3.
Assume H7: PNo_rel_strict_lowerbd x1 x2 x3.
Claim L8: ...
...
Claim L9: ...
...
Apply andI with PNo_rel_strict_upperbd x0 (ordsucc x2) (λ x4 . or (x3 x4) (x4 = x2)), PNo_rel_strict_lowerbd x1 (ordsucc x2) (λ x4 . or (x3 x4) (x4 = x2)) leaving 2 subgoals.
Let x4 of type ι be given.
Assume H10: x4 ∈ ordsucc x2.
Let x5 of type ι → ο be given.
Assume H11: PNo_downc x0 x4 x5.
Claim L12: ...
...
Apply PNoLt_tra with x4, x2, ordsucc x2, x5, x3, λ x6 . or (x3 x6) (x6 = x2) leaving 5 subgoals.
The subproof is completed by applying L12.
The subproof is completed by applying H0.
The subproof is completed by applying L8.
Apply H11 with PNoLt x4 x5 x2 x3.
Let x6 of type ι be given.
Assume H13: (λ x7 . and (ordinal x7) (∃ x8 : ι → ο . and (x0 x7 x8) (PNoLe x4 x5 x7 x8))) x6.
Apply H13 with PNoLt x4 x5 x2 x3.
Assume H14: ordinal x6.
Assume H15: ∃ x7 : ι → ο . and (x0 x6 x7) (PNoLe x4 x5 x6 x7).
Apply H15 with PNoLt x4 x5 x2 x3.
Let x7 of type ι → ο be given.
Assume H16: (λ x8 : ι → ο . and (x0 x6 x8) (PNoLe x4 x5 x6 x8)) x7.
Apply H16 with PNoLt x4 x5 x2 x3.
Assume H17: x0 x6 x7.
Assume H18: PNoLe x4 x5 x6 x7.
Claim L19: PNo_downc x0 x6 x7
Let x8 of type ο be given.
Assume H19: ∀ x9 . and (ordinal x9) (∃ x10 : ι → ο . and (x0 x9 x10) (PNoLe x6 x7 x9 x10)) ⟶ x8.
Apply H19 with x6.
Apply andI with ordinal x6, ∃ x9 : ι → ο . and (x0 x6 x9) (PNoLe x6 x7 x6 x9) leaving 2 subgoals.
The subproof is completed by applying H14.
Let x9 of type ο be given.
Assume H20: ∀ x10 : ι → ο . and (x0 x6 x10) (PNoLe x6 x7 x6 x10) ⟶ x9.
Apply H20 with x7.
Apply andI with x0 x6 x7, PNoLe x6 x7 x6 x7 leaving 2 subgoals.
The subproof is completed by applying H17.
The subproof is completed by applying PNoLe_ref with x6, x7.
Apply PNoLeLt_tra with x4, x6, x2, x5, x7, x3 leaving 5 subgoals.
The subproof is completed by applying L12.
The subproof is completed by applying H14.
The subproof is completed by applying H0.
The subproof is completed by applying H18.
Apply H6 with x6, x7 leaving 2 subgoals.
Apply H3 with x6, x7.
The subproof is completed by applying H17.
The subproof is completed by applying L19.
...
...
■