Metamath Proof Explorer

Theorem 2ellim

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

Ref Expression
Assertion 2ellim 
|- ( Lim A -> 2o 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 nlim2 
 |-  -. Lim 2o
10 limeq 
 |-  ( A = 2o -> ( Lim A <-> Lim 2o ) )
11 9 10 mtbiri 
 |-  ( A = 2o -> -. Lim A )
12 11 necon2ai 
 |-  ( Lim A -> A =/= 2o )
13 limord 
 |-  ( Lim A -> Ord A )
14 ord2eln012 
 |-  ( Ord A -> ( 2o e. A <-> ( A =/= (/) /\ A =/= 1o /\ A =/= 2o ) ) )
15 13 14 syl 
 |-  ( Lim A -> ( 2o e. A <-> ( A =/= (/) /\ A =/= 1o /\ A =/= 2o ) ) )
16 4 8 12 15 mpbir3and 
 |-  ( Lim A -> 2o e. A )