| pf |
|---|
Apply nat_p_omega with 0.
The subproof is completed by applying nat_0.
The subproof is completed by applying SNo_0.
Apply minus_SNo_0 with λ x0 x1 . not (SNo (minus_SNo omega) ⟶ add_SNo x1 (minus_SNo (minus_SNo omega)) ∈ int).
Apply minus_SNo_invol with omega, λ x0 x1 . not (SNo (minus_SNo omega) ⟶ add_SNo 0 x1 ∈ int) leaving 2 subgoals.
The subproof is completed by applying SNo_omega.
Apply add_SNo_0L with omega, λ x0 x1 . not (SNo (minus_SNo omega) ⟶ x1 ∈ int) leaving 2 subgoals.
The subproof is completed by applying SNo_omega.
Claim L4: ∀ x0 . x0 ∈ int ⟶ x0 = omega ⟶ ∀ x1 : ο . x1Apply int_SNo_cases with λ x0 . x0 = omega ⟶ ∀ x1 : ο . x1 leaving 2 subgoals.
Let x0 of type ι be given.
Apply In_irref with x0.
Apply H5 with λ x1 x2 . x0 ∈ x2.
The subproof is completed by applying H4.
Let x0 of type ι be given.
Apply SNoLt_irref with 0.
Apply SNoLtLe_tra with 0, omega, 0 leaving 5 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying SNo_omega.
The subproof is completed by applying SNo_0.
Apply ordinal_In_SNoLt with omega, 0 leaving 2 subgoals.
The subproof is completed by applying omega_ordinal.
Apply nat_p_omega with 0.
The subproof is completed by applying nat_0.
Apply H5 with λ x1 x2 . SNoLe x1 0.
Apply minus_SNo_0 with λ x1 x2 . SNoLe (minus_SNo x0) x1.
Apply minus_SNo_Le_contra with 0, x0 leaving 3 subgoals.
The subproof is completed by applying SNo_0.
Apply omega_SNo with x0.
The subproof is completed by applying H4.
Apply ordinal_Subq_SNoLe with 0, x0 leaving 3 subgoals.
The subproof is completed by applying ordinal_Empty.
Apply nat_p_ordinal with x0.
Apply omega_nat_p with x0.
The subproof is completed by applying H4.
The subproof is completed by applying Subq_Empty with x0.
Apply L4 with omega leaving 2 subgoals.
Apply H3.
Apply SNo_minus_SNo with omega.
The subproof is completed by applying SNo_omega.
Let x0 of type ι → ι → ο be given.
The subproof is completed by applying H5.
Apply L3.
Apply H0 with 0, minus_SNo omega leaving 2 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
■ |
|