Step |
Hyp |
Ref |
Expression |
1 |
|
infcl.1 |
|- ( ph -> R Or A ) |
2 |
|
infcl.2 |
|- ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) ) |
3 |
|
vex |
|- x e. _V |
4 |
|
vex |
|- y e. _V |
5 |
3 4
|
brcnv |
|- ( x `' R y <-> y R x ) |
6 |
5
|
bicomi |
|- ( y R x <-> x `' R y ) |
7 |
6
|
notbii |
|- ( -. y R x <-> -. x `' R y ) |
8 |
7
|
ralbii |
|- ( A. y e. B -. y R x <-> A. y e. B -. x `' R y ) |
9 |
4 3
|
brcnv |
|- ( y `' R x <-> x R y ) |
10 |
9
|
bicomi |
|- ( x R y <-> y `' R x ) |
11 |
|
vex |
|- z e. _V |
12 |
4 11
|
brcnv |
|- ( y `' R z <-> z R y ) |
13 |
12
|
bicomi |
|- ( z R y <-> y `' R z ) |
14 |
13
|
rexbii |
|- ( E. z e. B z R y <-> E. z e. B y `' R z ) |
15 |
10 14
|
imbi12i |
|- ( ( x R y -> E. z e. B z R y ) <-> ( y `' R x -> E. z e. B y `' R z ) ) |
16 |
15
|
ralbii |
|- ( A. y e. A ( x R y -> E. z e. B z R y ) <-> A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) |
17 |
8 16
|
anbi12i |
|- ( ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) <-> ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) ) |
18 |
17
|
rexbii |
|- ( E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) <-> E. x e. A ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) ) |
19 |
2 18
|
sylib |
|- ( ph -> E. x e. A ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) ) |