Step |
Hyp |
Ref |
Expression |
1 |
|
df-ne |
|- ( A =/= (/) <-> -. A = (/) ) |
2 |
|
df-lim |
|- ( Lim A <-> ( Ord A /\ A =/= (/) /\ A = U. A ) ) |
3 |
2
|
biimpri |
|- ( ( Ord A /\ A =/= (/) /\ A = U. A ) -> Lim A ) |
4 |
3
|
3exp |
|- ( Ord A -> ( A =/= (/) -> ( A = U. A -> Lim A ) ) ) |
5 |
1 4
|
syl5bir |
|- ( Ord A -> ( -. A = (/) -> ( A = U. A -> Lim A ) ) ) |
6 |
5
|
com23 |
|- ( Ord A -> ( A = U. A -> ( -. A = (/) -> Lim A ) ) ) |
7 |
6
|
imp |
|- ( ( Ord A /\ A = U. A ) -> ( -. A = (/) -> Lim A ) ) |
8 |
7
|
orrd |
|- ( ( Ord A /\ A = U. A ) -> ( A = (/) \/ Lim A ) ) |
9 |
8
|
ex |
|- ( Ord A -> ( A = U. A -> ( A = (/) \/ Lim A ) ) ) |
10 |
|
uni0 |
|- U. (/) = (/) |
11 |
10
|
eqcomi |
|- (/) = U. (/) |
12 |
|
id |
|- ( A = (/) -> A = (/) ) |
13 |
|
unieq |
|- ( A = (/) -> U. A = U. (/) ) |
14 |
11 12 13
|
3eqtr4a |
|- ( A = (/) -> A = U. A ) |
15 |
|
limuni |
|- ( Lim A -> A = U. A ) |
16 |
14 15
|
jaoi |
|- ( ( A = (/) \/ Lim A ) -> A = U. A ) |
17 |
9 16
|
impbid1 |
|- ( Ord A -> ( A = U. A <-> ( A = (/) \/ Lim A ) ) ) |