Step |
Hyp |
Ref |
Expression |
1 |
|
df-lim |
|- ( Lim A <-> ( Ord A /\ A =/= (/) /\ A = U. A ) ) |
2 |
|
ord0eln0 |
|- ( Ord A -> ( (/) e. A <-> A =/= (/) ) ) |
3 |
2
|
anbi1d |
|- ( Ord A -> ( ( (/) e. A /\ A = U. A ) <-> ( A =/= (/) /\ A = U. A ) ) ) |
4 |
3
|
pm5.32i |
|- ( ( Ord A /\ ( (/) e. A /\ A = U. A ) ) <-> ( Ord A /\ ( A =/= (/) /\ A = U. A ) ) ) |
5 |
|
3anass |
|- ( ( Ord A /\ (/) e. A /\ A = U. A ) <-> ( Ord A /\ ( (/) e. A /\ A = U. A ) ) ) |
6 |
|
3anass |
|- ( ( Ord A /\ A =/= (/) /\ A = U. A ) <-> ( Ord A /\ ( A =/= (/) /\ A = U. A ) ) ) |
7 |
4 5 6
|
3bitr4i |
|- ( ( Ord A /\ (/) e. A /\ A = U. A ) <-> ( Ord A /\ A =/= (/) /\ A = U. A ) ) |
8 |
1 7
|
bitr4i |
|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U. A ) ) |