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 =/= (/) ) -> E. x e. 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 =/= (/) ) -> E. x e. On A = suc x ) <-> ( ( Ord A /\ -. A = (/) ) -> E. x e. On A = suc x ) )
6 pm5.6 
 |-  ( ( ( Ord A /\ -. A = (/) ) -> E. x e. On A = suc x ) <-> ( Ord A -> ( A = (/) \/ E. x e. On A = suc x ) ) )
7 iman 
 |-  ( ( Ord A -> ( A = (/) \/ E. x e. On A = suc x ) ) <-> -. ( Ord A /\ -. ( A = (/) \/ E. x e. On A = suc x ) ) )
8 5 6 7 3bitrri 
 |-  ( -. ( Ord A /\ -. ( A = (/) \/ E. x e. On A = suc x ) ) <-> ( ( Ord A /\ A =/= (/) ) -> E. x e. On A = suc x ) )
9 dflim3 
 |-  ( Lim A <-> ( Ord A /\ -. ( A = (/) \/ E. x e. On A = suc x ) ) )
10 8 9 xchnxbir 
 |-  ( -. Lim A <-> ( ( Ord A /\ A =/= (/) ) -> E. x e. On A = suc x ) )
11 10 anbi2i 
 |-  ( ( ( Ord A /\ A =/= (/) ) /\ -. Lim A ) <-> ( ( Ord A /\ A =/= (/) ) /\ ( ( Ord A /\ A =/= (/) ) -> E. x e. On A = suc x ) ) )
12 1 2 11 3bitri 
 |-  ( ( Ord A /\ -. Lim A /\ A =/= (/) ) <-> ( ( Ord A /\ A =/= (/) ) /\ ( ( Ord A /\ A =/= (/) ) -> E. x e. On A = suc x ) ) )
13 pm3.35 
 |-  ( ( ( Ord A /\ A =/= (/) ) /\ ( ( Ord A /\ A =/= (/) ) -> E. x e. On A = suc x ) ) -> E. x e. On A = suc x )
14 12 13 sylbi 
 |-  ( ( Ord A /\ -. Lim A /\ A =/= (/) ) -> E. x e. On A = suc x )