| 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 |