Metamath Proof Explorer


Theorem 2ellim

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

Ref Expression
Assertion 2ellim Lim A 2 𝑜 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 1 𝑜
6 limeq A = 1 𝑜 Lim A Lim 1 𝑜
7 5 6 mtbiri A = 1 𝑜 ¬ Lim A
8 7 necon2ai Lim A A 1 𝑜
9 nlim2 ¬ Lim 2 𝑜
10 limeq A = 2 𝑜 Lim A Lim 2 𝑜
11 9 10 mtbiri A = 2 𝑜 ¬ Lim A
12 11 necon2ai Lim A A 2 𝑜
13 limord Lim A Ord A
14 ord2eln012 Ord A 2 𝑜 A A A 1 𝑜 A 2 𝑜
15 13 14 syl Lim A 2 𝑜 A A A 1 𝑜 A 2 𝑜
16 4 8 12 15 mpbir3and Lim A 2 𝑜 A