Metamath Proof Explorer

Theorem faosnf0.11b

Description: B is called a non-limit ordinal if it is not a limit ordinal. (Contributed by RP, 27-Sep-2023)

Alling, Norman L. "Fundamentals of Analysis Over Surreal Numbers Fields." The Rocky Mountain Journal of Mathematics 19, no. 3 (1989): 565-73. http://www.jstor.org/stable/44237243.

Ref Expression
Assertion faosnf0.11b ⊢ Ord ⁡ A ∧ ¬ Lim ⁡ A ∧ A ≠ ∅ → ∃ x ∈ On A = suc ⁡ x

Proof

Step Hyp Ref Expression
1 3ancomb ⊢ Ord ⁡ A ∧ ¬ Lim ⁡ A ∧ A ≠ ∅ ↔ Ord ⁡ A ∧ A ≠ ∅ ∧ ¬ Lim ⁡ A
2 df-3an ⊢ Ord ⁡ A ∧ A ≠ ∅ ∧ ¬ Lim ⁡ A ↔ Ord ⁡ A ∧ A ≠ ∅ ∧ ¬ Lim ⁡ A
3 df-ne ⊢ A ≠ ∅ ↔ ¬ A = ∅
4 3 anbi2i ⊢ Ord ⁡ A ∧ A ≠ ∅ ↔ Ord ⁡ A ∧ ¬ A = ∅
5 4 imbi1i ⊢ Ord ⁡ A ∧ A ≠ ∅ → ∃ x ∈ On A = suc ⁡ x ↔ Ord ⁡ A ∧ ¬ A = ∅ → ∃ x ∈ On A = suc ⁡ x
6 pm5.6 ⊢ Ord ⁡ A ∧ ¬ A = ∅ → ∃ x ∈ On A = suc ⁡ x ↔ Ord ⁡ A → A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x
7 iman ⊢ Ord ⁡ A → A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x ↔ ¬ Ord ⁡ A ∧ ¬ A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x
8 5 6 7 3bitrri ⊢ ¬ Ord ⁡ A ∧ ¬ A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x ↔ Ord ⁡ A ∧ A ≠ ∅ → ∃ x ∈ On A = suc ⁡ x
9 dflim3 ⊢ Lim ⁡ A ↔ Ord ⁡ A ∧ ¬ A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x
10 8 9 xchnxbir ⊢ ¬ Lim ⁡ A ↔ Ord ⁡ A ∧ A ≠ ∅ → ∃ x ∈ On A = suc ⁡ x
11 10 anbi2i ⊢ Ord ⁡ A ∧ A ≠ ∅ ∧ ¬ Lim ⁡ A ↔ Ord ⁡ A ∧ A ≠ ∅ ∧ Ord ⁡ A ∧ A ≠ ∅ → ∃ x ∈ On A = suc ⁡ x
12 1 2 11 3bitri ⊢ Ord ⁡ A ∧ ¬ Lim ⁡ A ∧ A ≠ ∅ ↔ Ord ⁡ A ∧ A ≠ ∅ ∧ Ord ⁡ A ∧ A ≠ ∅ → ∃ x ∈ On A = suc ⁡ x
13 pm3.35 ⊢ Ord ⁡ A ∧ A ≠ ∅ ∧ Ord ⁡ A ∧ A ≠ ∅ → ∃ x ∈ On A = suc ⁡ x → ∃ x ∈ On A = suc ⁡ x
14 12 13 sylbi ⊢ Ord ⁡ A ∧ ¬ Lim ⁡ A ∧ A ≠ ∅ → ∃ x ∈ On A = suc ⁡ x