Metamath Proof Explorer


Theorem 1ellim

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

Ref Expression
Assertion 1ellim Lim A 1 𝑜 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 limord Lim A Ord A
10 ord1eln01 Ord A 1 𝑜 A A A 1 𝑜
11 9 10 syl Lim A 1 𝑜 A A A 1 𝑜
12 4 8 11 mpbir2and Lim A 1 𝑜 A