Step |
Hyp |
Ref |
Expression |
1 |
|
elex |
|- ( A e. On -> A e. _V ) |
2 |
|
eloni |
|- ( A e. On -> Ord A ) |
3 |
|
ordzsl |
|- ( Ord A <-> ( A = (/) \/ E. x e. On A = suc x \/ Lim A ) ) |
4 |
|
3mix1 |
|- ( A = (/) -> ( A = (/) \/ E. x e. On A = suc x \/ ( A e. _V /\ Lim A ) ) ) |
5 |
4
|
adantl |
|- ( ( A e. _V /\ A = (/) ) -> ( A = (/) \/ E. x e. On A = suc x \/ ( A e. _V /\ Lim A ) ) ) |
6 |
|
3mix2 |
|- ( E. x e. On A = suc x -> ( A = (/) \/ E. x e. On A = suc x \/ ( A e. _V /\ Lim A ) ) ) |
7 |
6
|
adantl |
|- ( ( A e. _V /\ E. x e. On A = suc x ) -> ( A = (/) \/ E. x e. On A = suc x \/ ( A e. _V /\ Lim A ) ) ) |
8 |
|
3mix3 |
|- ( ( A e. _V /\ Lim A ) -> ( A = (/) \/ E. x e. On A = suc x \/ ( A e. _V /\ Lim A ) ) ) |
9 |
5 7 8
|
3jaodan |
|- ( ( A e. _V /\ ( A = (/) \/ E. x e. On A = suc x \/ Lim A ) ) -> ( A = (/) \/ E. x e. On A = suc x \/ ( A e. _V /\ Lim A ) ) ) |
10 |
3 9
|
sylan2b |
|- ( ( A e. _V /\ Ord A ) -> ( A = (/) \/ E. x e. On A = suc x \/ ( A e. _V /\ Lim A ) ) ) |
11 |
1 2 10
|
syl2anc |
|- ( A e. On -> ( A = (/) \/ E. x e. On A = suc x \/ ( A e. _V /\ Lim A ) ) ) |
12 |
|
0elon |
|- (/) e. On |
13 |
|
eleq1 |
|- ( A = (/) -> ( A e. On <-> (/) e. On ) ) |
14 |
12 13
|
mpbiri |
|- ( A = (/) -> A e. On ) |
15 |
|
suceloni |
|- ( x e. On -> suc x e. On ) |
16 |
|
eleq1 |
|- ( A = suc x -> ( A e. On <-> suc x e. On ) ) |
17 |
15 16
|
syl5ibrcom |
|- ( x e. On -> ( A = suc x -> A e. On ) ) |
18 |
17
|
rexlimiv |
|- ( E. x e. On A = suc x -> A e. On ) |
19 |
|
limelon |
|- ( ( A e. _V /\ Lim A ) -> A e. On ) |
20 |
14 18 19
|
3jaoi |
|- ( ( A = (/) \/ E. x e. On A = suc x \/ ( A e. _V /\ Lim A ) ) -> A e. On ) |
21 |
11 20
|
impbii |
|- ( A e. On <-> ( A = (/) \/ E. x e. On A = suc x \/ ( A e. _V /\ Lim A ) ) ) |