Step |
Hyp |
Ref |
Expression |
1 |
|
poinxp |
|- ( R Po A <-> ( R i^i ( A X. A ) ) Po A ) |
2 |
|
brinxp |
|- ( ( x e. A /\ y e. A ) -> ( x R y <-> x ( R i^i ( A X. A ) ) y ) ) |
3 |
|
biidd |
|- ( ( x e. A /\ y e. A ) -> ( x = y <-> x = y ) ) |
4 |
|
brinxp |
|- ( ( y e. A /\ x e. A ) -> ( y R x <-> y ( R i^i ( A X. A ) ) x ) ) |
5 |
4
|
ancoms |
|- ( ( x e. A /\ y e. A ) -> ( y R x <-> y ( R i^i ( A X. A ) ) x ) ) |
6 |
2 3 5
|
3orbi123d |
|- ( ( x e. A /\ y e. A ) -> ( ( x R y \/ x = y \/ y R x ) <-> ( x ( R i^i ( A X. A ) ) y \/ x = y \/ y ( R i^i ( A X. A ) ) x ) ) ) |
7 |
6
|
ralbidva |
|- ( x e. A -> ( A. y e. A ( x R y \/ x = y \/ y R x ) <-> A. y e. A ( x ( R i^i ( A X. A ) ) y \/ x = y \/ y ( R i^i ( A X. A ) ) x ) ) ) |
8 |
7
|
ralbiia |
|- ( A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) <-> A. x e. A A. y e. A ( x ( R i^i ( A X. A ) ) y \/ x = y \/ y ( R i^i ( A X. A ) ) x ) ) |
9 |
1 8
|
anbi12i |
|- ( ( R Po A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) <-> ( ( R i^i ( A X. A ) ) Po A /\ A. x e. A A. y e. A ( x ( R i^i ( A X. A ) ) y \/ x = y \/ y ( R i^i ( A X. A ) ) x ) ) ) |
10 |
|
df-so |
|- ( R Or A <-> ( R Po A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) ) |
11 |
|
df-so |
|- ( ( R i^i ( A X. A ) ) Or A <-> ( ( R i^i ( A X. A ) ) Po A /\ A. x e. A A. y e. A ( x ( R i^i ( A X. A ) ) y \/ x = y \/ y ( R i^i ( A X. A ) ) x ) ) ) |
12 |
9 10 11
|
3bitr4i |
|- ( R Or A <-> ( R i^i ( A X. A ) ) Or A ) |