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 )