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 (PNo_pred (PNoCutL x0 x1) (PNoCutR x0 x1)).
Assume H1: TransSet x0.
Assume H2: ∀ x2 . x2 ∈ x0 ⟶ TransSet x2.
Claim L3: ...
...
Apply PNo_bd_pred with PNoCutL x0 x1, PNoCutR x0 x1, x0, PNoEq_ x0 x1 (PNo_pred (PNoCutL x0 x1) (PNoCutR x0 x1)) leaving 5 subgoals.
Apply PNoCut_pwise with x0, x1.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
The subproof is completed by applying PNoCutL_lenbdd with x0, x1.
The subproof is completed by applying PNoCutR_lenbdd with x0, x1.
Claim L4: ...
...
Apply L4 with λ x2 x3 . and (ordinal x3) (PNo_strict_imv (PNoCutL x0 x1) (PNoCutR x0 x1) x3 (PNo_pred (PNoCutL x0 x1) (PNoCutR x0 x1))) ⟶ (∀ x4 . x4 ∈ x3 ⟶ ∀ x5 : ι → ο . not (PNo_strict_imv (PNoCutL x0 x1) (PNoCutR x0 x1) x4 x5)) ⟶ PNoEq_ x0 x1 (PNo_pred (PNoCutL x0 x1) (PNoCutR x0 x1)).
Assume H5: and (ordinal x0) (PNo_strict_imv (PNoCutL x0 x1) (PNoCutR x0 x1) x0 (PNo_pred (PNoCutL x0 x1) (PNoCutR x0 x1))).
Apply H5 with (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 : ι → ο . not (PNo_strict_imv (PNoCutL x0 x1) (PNoCutR x0 x1) x2 x3)) ⟶ PNoEq_ x0 x1 (PNo_pred (PNoCutL x0 x1) (PNoCutR x0 x1)).
Assume H6: ordinal x0.
Assume H7: PNo_strict_imv (PNoCutL x0 x1) (PNoCutR x0 x1) x0 (PNo_pred (PNoCutL x0 x1) (PNoCutR x0 x1)).
Assume H8: ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 : ι → ο . not (PNo_strict_imv (PNoCutL x0 x1) (PNoCutR x0 x1) x2 x3).
Apply H7 with PNoEq_ x0 x1 (PNo_pred (PNoCutL x0 x1) (PNoCutR x0 x1)).
Assume H9: PNo_strict_upperbd (PNoCutL x0 x1) x0 (PNo_pred (PNoCutL x0 x1) (PNoCutR x0 x1)).
Assume H10: PNo_strict_lowerbd (PNoCutR x0 x1) x0 (PNo_pred (PNoCutL x0 x1) (PNoCutR x0 x1)).
Claim L11: ∀ x2 . ordinal x2 ⟶ x2 ∈ x0 ⟶ iff (x1 x2) (PNo_pred (PNoCutL x0 x1) (PNoCutR x0 x1) x2)
Apply ordinal_ind with λ x2 . x2 ∈ x0 ⟶ iff (x1 x2) (PNo_pred (PNoCutL x0 x1) (PNoCutR x0 x1) x2).
Let x2 of type ι be given.
Assume H11: ordinal x2.
Assume H12: ∀ x3 . ... ⟶ ... ⟶ iff (x1 x3) (PNo_pred (PNoCutL x0 x1) (PNoCutR x0 ...) ...).
...
Let x2 of type ι be given.
Assume H12: 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.
■