Theorem nlim2

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

	Ref	Expression
Assertion	nlim2	⊢ ¬ Lim 2o

Proof

Step	Hyp	Ref	Expression
1		1oelpr	⊢ 1o ∈ { ∅ , 1o }
2		df2o3	⊢ 2o = { ∅ , 1o }
3	1 2	eleqtrri	⊢ 1o ∈ 2o
4		1on	⊢ 1o ∈ On
5	4	onirri	⊢ ¬ 1o ∈ 1o
6		eleq2	⊢ ( 2o = 1o → ( 1o ∈ 2o ↔ 1o ∈ 1o ) )
7	5 6	mtbiri	⊢ ( 2o = 1o → ¬ 1o ∈ 2o )
8	3 7	mt2	⊢ ¬ 2o = 1o
9	8	neir	⊢ 2o ≠ 1o
10	2	unieqi	⊢ ∪ 2o = ∪ { ∅ , 1o }
11		0ex	⊢ ∅ ∈ V
12		1oex	⊢ 1o ∈ V
13	11 12	unipr	⊢ ∪ { ∅ , 1o } = ( ∅ ∪ 1o )
14		0un	⊢ ( ∅ ∪ 1o ) = 1o
15	10 13 14	3eqtri	⊢ ∪ 2o = 1o
16	9 15	neeqtrri	⊢ 2o ≠ ∪ 2o
17	16	neii	⊢ ¬ 2o = ∪ 2o
18		simp3	⊢ ( ( Ord 2o ∧ 2o ≠ ∅ ∧ 2o = ∪ 2o ) → 2o = ∪ 2o )
19	17 18	mto	⊢ ¬ ( Ord 2o ∧ 2o ≠ ∅ ∧ 2o = ∪ 2o )
20		df-lim	⊢ ( Lim 2o ↔ ( Ord 2o ∧ 2o ≠ ∅ ∧ 2o = ∪ 2o ) )
21	19 20	mtbir	⊢ ¬ Lim 2o