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 e. { (/) , 1o }
2		df2o3	|- 2o = { (/) , 1o }
3	1 2	eleqtrri	|- 1o e. 2o
4		1on	|- 1o e. On
5	4	onirri	|- -. 1o e. 1o
6		eleq2	|- ( 2o = 1o -> ( 1o e. 2o <-> 1o e. 1o ) )
7	5 6	mtbiri	|- ( 2o = 1o -> -. 1o e. 2o )
8	3 7	mt2	|- -. 2o = 1o
9	8	neir	|- 2o =/= 1o
10	2	unieqi	|- U. 2o = U. { (/) , 1o }
11		0ex	|- (/) e. _V
12		1oex	|- 1o e. _V
13	11 12	unipr	|- U. { (/) , 1o } = ( (/) u. 1o )
14		0un	|- ( (/) u. 1o ) = 1o
15	10 13 14	3eqtri	|- U. 2o = 1o
16	9 15	neeqtrri	|- 2o =/= U. 2o
17	16	neii	|- -. 2o = U. 2o
18		simp3	|- ( ( Ord 2o /\ 2o =/= (/) /\ 2o = U. 2o ) -> 2o = U. 2o )
19	17 18	mto	|- -. ( Ord 2o /\ 2o =/= (/) /\ 2o = U. 2o )
20		df-lim	|- ( Lim 2o <-> ( Ord 2o /\ 2o =/= (/) /\ 2o = U. 2o ) )
21	19 20	mtbir	|- -. Lim 2o