Step |
Hyp |
Ref |
Expression |
1 |
|
df-ord |
|- ( Ord A <-> ( Tr A /\ _E We A ) ) |
2 |
|
zfregfr |
|- _E Fr A |
3 |
|
dfwe2 |
|- ( _E We A <-> ( _E Fr A /\ A. x e. A A. y e. A ( x _E y \/ x = y \/ y _E x ) ) ) |
4 |
2 3
|
mpbiran |
|- ( _E We A <-> A. x e. A A. y e. A ( x _E y \/ x = y \/ y _E x ) ) |
5 |
|
epel |
|- ( x _E y <-> x e. y ) |
6 |
|
biid |
|- ( x = y <-> x = y ) |
7 |
|
epel |
|- ( y _E x <-> y e. x ) |
8 |
5 6 7
|
3orbi123i |
|- ( ( x _E y \/ x = y \/ y _E x ) <-> ( x e. y \/ x = y \/ y e. x ) ) |
9 |
8
|
2ralbii |
|- ( A. x e. A A. y e. A ( x _E y \/ x = y \/ y _E x ) <-> A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) ) |
10 |
4 9
|
bitri |
|- ( _E We A <-> A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) ) |
11 |
10
|
anbi2i |
|- ( ( Tr A /\ _E We A ) <-> ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) ) ) |
12 |
1 11
|
bitri |
|- ( Ord A <-> ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) ) ) |