Step |
Hyp |
Ref |
Expression |
1 |
|
df-lim |
|- ( Lim A <-> ( Ord A /\ A =/= (/) /\ A = U. A ) ) |
2 |
|
3anass |
|- ( ( Ord A /\ A =/= (/) /\ A = U. A ) <-> ( Ord A /\ ( A =/= (/) /\ A = U. A ) ) ) |
3 |
|
df-ne |
|- ( A =/= (/) <-> -. A = (/) ) |
4 |
3
|
a1i |
|- ( Ord A -> ( A =/= (/) <-> -. A = (/) ) ) |
5 |
|
orduninsuc |
|- ( Ord A -> ( A = U. A <-> -. E. x e. On A = suc x ) ) |
6 |
4 5
|
anbi12d |
|- ( Ord A -> ( ( A =/= (/) /\ A = U. A ) <-> ( -. A = (/) /\ -. E. x e. On A = suc x ) ) ) |
7 |
|
ioran |
|- ( -. ( A = (/) \/ E. x e. On A = suc x ) <-> ( -. A = (/) /\ -. E. x e. On A = suc x ) ) |
8 |
6 7
|
bitr4di |
|- ( Ord A -> ( ( A =/= (/) /\ A = U. A ) <-> -. ( A = (/) \/ E. x e. On A = suc x ) ) ) |
9 |
8
|
pm5.32i |
|- ( ( Ord A /\ ( A =/= (/) /\ A = U. A ) ) <-> ( Ord A /\ -. ( A = (/) \/ E. x e. On A = suc x ) ) ) |
10 |
1 2 9
|
3bitri |
|- ( Lim A <-> ( Ord A /\ -. ( A = (/) \/ E. x e. On A = suc x ) ) ) |