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		1oex	⊢ 1o ∈ V
2	1	prid2	⊢ 1o ∈ { ∅ , 1o }
3		df2o3	⊢ 2o = { ∅ , 1o }
4	2 3	eleqtrri	⊢ 1o ∈ 2o
5		1on	⊢ 1o ∈ On
6	5	onirri	⊢ ¬ 1o ∈ 1o
7		eleq2	⊢ ( 2o = 1o → ( 1o ∈ 2o ↔ 1o ∈ 1o ) )
8	6 7	mtbiri	⊢ ( 2o = 1o → ¬ 1o ∈ 2o )
9	4 8	mt2	⊢ ¬ 2o = 1o
10	9	neir	⊢ 2o ≠ 1o
11	3	unieqi	⊢ ∪ 2o = ∪ { ∅ , 1o }
12		0ex	⊢ ∅ ∈ V
13	12 1	unipr	⊢ ∪ { ∅ , 1o } = ( ∅ ∪ 1o )
14		0un	⊢ ( ∅ ∪ 1o ) = 1o
15	11 13 14	3eqtri	⊢ ∪ 2o = 1o
16	10 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