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