Metamath Proof Explorer


Theorem nlim1

Description: 1 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024)

Ref Expression
Assertion nlim1 ¬ Lim 1 𝑜

Proof

Step Hyp Ref Expression
1 1n0 1 𝑜
2 0ex V
3 2 unisn =
4 1 3 neeqtrri 1 𝑜
5 df1o2 1 𝑜 =
6 5 unieqi 1 𝑜 =
7 4 6 neeqtrri 1 𝑜 1 𝑜
8 7 neii ¬ 1 𝑜 = 1 𝑜
9 simp3 Ord 1 𝑜 1 𝑜 1 𝑜 = 1 𝑜 1 𝑜 = 1 𝑜
10 8 9 mto ¬ Ord 1 𝑜 1 𝑜 1 𝑜 = 1 𝑜
11 df-lim Lim 1 𝑜 Ord 1 𝑜 1 𝑜 1 𝑜 = 1 𝑜
12 10 11 mtbir ¬ Lim 1 𝑜