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 e. _V
2	1	prid2	|- 1o e. { (/) , 1o }
3		df2o3	|- 2o = { (/) , 1o }
4	2 3	eleqtrri	|- 1o e. 2o
5		1on	|- 1o e. On
6	5	onirri	|- -. 1o e. 1o
7		eleq2	|- ( 2o = 1o -> ( 1o e. 2o <-> 1o e. 1o ) )
8	6 7	mtbiri	|- ( 2o = 1o -> -. 1o e. 2o )
9	4 8	mt2	|- -. 2o = 1o
10	9	neir	|- 2o =/= 1o
11	3	unieqi	|- U. 2o = U. { (/) , 1o }
12		0ex	|- (/) e. _V
13	12 1	unipr	|- U. { (/) , 1o } = ( (/) u. 1o )
14		0un	|- ( (/) u. 1o ) = 1o
15	11 13 14	3eqtri	|- U. 2o = 1o
16	10 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