Step |
Hyp |
Ref |
Expression |
1 |
|
nnlim |
|- ( A e. _om -> -. Lim A ) |
2 |
1
|
adantr |
|- ( ( A e. _om /\ A =/= (/) ) -> -. Lim A ) |
3 |
|
nnord |
|- ( A e. _om -> Ord A ) |
4 |
|
orduninsuc |
|- ( Ord A -> ( A = U. A <-> -. E. x e. On A = suc x ) ) |
5 |
4
|
adantr |
|- ( ( Ord A /\ A =/= (/) ) -> ( A = U. A <-> -. E. x e. On A = suc x ) ) |
6 |
|
df-lim |
|- ( Lim A <-> ( Ord A /\ A =/= (/) /\ A = U. A ) ) |
7 |
6
|
biimpri |
|- ( ( Ord A /\ A =/= (/) /\ A = U. A ) -> Lim A ) |
8 |
7
|
3expia |
|- ( ( Ord A /\ A =/= (/) ) -> ( A = U. A -> Lim A ) ) |
9 |
5 8
|
sylbird |
|- ( ( Ord A /\ A =/= (/) ) -> ( -. E. x e. On A = suc x -> Lim A ) ) |
10 |
3 9
|
sylan |
|- ( ( A e. _om /\ A =/= (/) ) -> ( -. E. x e. On A = suc x -> Lim A ) ) |
11 |
2 10
|
mt3d |
|- ( ( A e. _om /\ A =/= (/) ) -> E. x e. On A = suc x ) |
12 |
|
eleq1 |
|- ( A = suc x -> ( A e. _om <-> suc x e. _om ) ) |
13 |
12
|
biimpcd |
|- ( A e. _om -> ( A = suc x -> suc x e. _om ) ) |
14 |
|
peano2b |
|- ( x e. _om <-> suc x e. _om ) |
15 |
13 14
|
syl6ibr |
|- ( A e. _om -> ( A = suc x -> x e. _om ) ) |
16 |
15
|
ancrd |
|- ( A e. _om -> ( A = suc x -> ( x e. _om /\ A = suc x ) ) ) |
17 |
16
|
adantld |
|- ( A e. _om -> ( ( x e. On /\ A = suc x ) -> ( x e. _om /\ A = suc x ) ) ) |
18 |
17
|
reximdv2 |
|- ( A e. _om -> ( E. x e. On A = suc x -> E. x e. _om A = suc x ) ) |
19 |
18
|
adantr |
|- ( ( A e. _om /\ A =/= (/) ) -> ( E. x e. On A = suc x -> E. x e. _om A = suc x ) ) |
20 |
11 19
|
mpd |
|- ( ( A e. _om /\ A =/= (/) ) -> E. x e. _om A = suc x ) |