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