Description: 1 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | nlim1 | |- -. Lim 1o |
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 |