Step |
Hyp |
Ref |
Expression |
1 |
|
nlim0 |
|- -. Lim (/) |
2 |
|
limeq |
|- ( A = (/) -> ( Lim A <-> Lim (/) ) ) |
3 |
1 2
|
mtbiri |
|- ( A = (/) -> -. Lim A ) |
4 |
3
|
necon2ai |
|- ( Lim A -> A =/= (/) ) |
5 |
|
nlim1 |
|- -. Lim 1o |
6 |
|
limeq |
|- ( A = 1o -> ( Lim A <-> Lim 1o ) ) |
7 |
5 6
|
mtbiri |
|- ( A = 1o -> -. Lim A ) |
8 |
7
|
necon2ai |
|- ( Lim A -> A =/= 1o ) |
9 |
|
nlim2 |
|- -. Lim 2o |
10 |
|
limeq |
|- ( A = 2o -> ( Lim A <-> Lim 2o ) ) |
11 |
9 10
|
mtbiri |
|- ( A = 2o -> -. Lim A ) |
12 |
11
|
necon2ai |
|- ( Lim A -> A =/= 2o ) |
13 |
|
limord |
|- ( Lim A -> Ord A ) |
14 |
|
ord2eln012 |
|- ( Ord A -> ( 2o e. A <-> ( A =/= (/) /\ A =/= 1o /\ A =/= 2o ) ) ) |
15 |
13 14
|
syl |
|- ( Lim A -> ( 2o e. A <-> ( A =/= (/) /\ A =/= 1o /\ A =/= 2o ) ) ) |
16 |
4 8 12 15
|
mpbir3and |
|- ( Lim A -> 2o e. A ) |