Step |
Hyp |
Ref |
Expression |
1 |
|
dflim4 |
|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A. x e. A suc x e. A ) ) |
2 |
|
suceq |
|- ( x = B -> suc x = suc B ) |
3 |
2
|
eleq1d |
|- ( x = B -> ( suc x e. A <-> suc B e. A ) ) |
4 |
3
|
rspccv |
|- ( A. x e. A suc x e. A -> ( B e. A -> suc B e. A ) ) |
5 |
4
|
3ad2ant3 |
|- ( ( Ord A /\ (/) e. A /\ A. x e. A suc x e. A ) -> ( B e. A -> suc B e. A ) ) |
6 |
1 5
|
sylbi |
|- ( Lim A -> ( B e. A -> suc B e. A ) ) |
7 |
|
limord |
|- ( Lim A -> Ord A ) |
8 |
|
ordtr |
|- ( Ord A -> Tr A ) |
9 |
|
trsuc |
|- ( ( Tr A /\ suc B e. A ) -> B e. A ) |
10 |
9
|
ex |
|- ( Tr A -> ( suc B e. A -> B e. A ) ) |
11 |
7 8 10
|
3syl |
|- ( Lim A -> ( suc B e. A -> B e. A ) ) |
12 |
6 11
|
impbid |
|- ( Lim A -> ( B e. A <-> suc B e. A ) ) |