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 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 3ancomb | ⊢ ( ( Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅ ) ↔ ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴 ) ) | |
| 2 | df-3an | ⊢ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴 ) ↔ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) ∧ ¬ Lim 𝐴 ) ) | |
| 3 | df-ne | ⊢ ( 𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅ ) | |
| 4 | 3 | anbi2i | ⊢ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) ↔ ( Ord 𝐴 ∧ ¬ 𝐴 = ∅ ) ) |
| 5 | 4 | imbi1i | ⊢ ( ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ↔ ( ( Ord 𝐴 ∧ ¬ 𝐴 = ∅ ) → ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) |
| 6 | pm5.6 | ⊢ ( ( ( Ord 𝐴 ∧ ¬ 𝐴 = ∅ ) → ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ↔ ( Ord 𝐴 → ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) ) | |
| 7 | iman | ⊢ ( ( Ord 𝐴 → ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) ↔ ¬ ( Ord 𝐴 ∧ ¬ ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) ) | |
| 8 | 5 6 7 | 3bitrri | ⊢ ( ¬ ( Ord 𝐴 ∧ ¬ ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) ↔ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) |
| 9 | dflim3 | ⊢ ( Lim 𝐴 ↔ ( Ord 𝐴 ∧ ¬ ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) ) | |
| 10 | 8 9 | xchnxbir | ⊢ ( ¬ Lim 𝐴 ↔ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) |
| 11 | 10 | anbi2i | ⊢ ( ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) ∧ ¬ Lim 𝐴 ) ↔ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) ∧ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) ) |
| 12 | 1 2 11 | 3bitri | ⊢ ( ( Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅ ) ↔ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) ∧ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) ) |
| 13 | pm3.35 | ⊢ ( ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) ∧ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) → ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) | |
| 14 | 12 13 | sylbi | ⊢ ( ( Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) |