Metamath Proof Explorer

Theorem nlim1

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

Ref Expression
Assertion nlim1 
|- -. Lim 1o

Proof

Step Hyp Ref Expression
1 1n0 
 |-  1o =/= (/)
2 0ex 
 |-  (/) e. _V
3 2 unisn 
 |-  U. { (/) } = (/)
4 1 3 neeqtrri 
 |-  1o =/= U. { (/) }
5 df1o2 
 |-  1o = { (/) }
6 5 unieqi 
 |-  U. 1o = U. { (/) }
7 4 6 neeqtrri 
 |-  1o =/= U. 1o
8 7 neii 
 |-  -. 1o = U. 1o
9 simp3 
 |-  ( ( Ord 1o /\ 1o =/= (/) /\ 1o = U. 1o ) -> 1o = U. 1o )
10 8 9 mto 
 |-  -. ( Ord 1o /\ 1o =/= (/) /\ 1o = U. 1o )
11 df-lim 
 |-  ( Lim 1o <-> ( Ord 1o /\ 1o =/= (/) /\ 1o = U. 1o ) )
12 10 11 mtbir 
 |-  -. Lim 1o