Metamath Proof Explorer

Theorem 1ellim

Description: A limit ordinal contains 1. (Contributed by BTernaryTau, 1-Dec-2024)

Ref Expression
Assertion 1ellim 
|- ( Lim A -> 1o e. A )

Proof

Step Hyp Ref Expression
1 nlim0 
 |-  -. Lim (/)
2 limeq 
 |-  ( A = (/) -> ( Lim A <-> Lim (/) ) )
3 1 2 mtbiri 
 |-  ( A = (/) -> -. Lim A )
4 3 necon2ai 
 |-  ( Lim A -> A =/= (/) )
5 nlim1 
 |-  -. Lim 1o
6 limeq 
 |-  ( A = 1o -> ( Lim A <-> Lim 1o ) )
7 5 6 mtbiri 
 |-  ( A = 1o -> -. Lim A )
8 7 necon2ai 
 |-  ( Lim A -> A =/= 1o )
9 limord 
 |-  ( Lim A -> Ord A )
10 ord1eln01 
 |-  ( Ord A -> ( 1o e. A <-> ( A =/= (/) /\ A =/= 1o ) ) )
11 9 10 syl 
 |-  ( Lim A -> ( 1o e. A <-> ( A =/= (/) /\ A =/= 1o ) ) )
12 4 8 11 mpbir2and 
 |-  ( Lim A -> 1o e. A )