Step |
Hyp |
Ref |
Expression |
1 |
|
caovordig.1 |
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( x R y -> ( z F x ) R ( z F y ) ) ) |
2 |
1
|
ralrimivvva |
|- ( ph -> A. x e. S A. y e. S A. z e. S ( x R y -> ( z F x ) R ( z F y ) ) ) |
3 |
|
breq1 |
|- ( x = A -> ( x R y <-> A R y ) ) |
4 |
|
oveq2 |
|- ( x = A -> ( z F x ) = ( z F A ) ) |
5 |
4
|
breq1d |
|- ( x = A -> ( ( z F x ) R ( z F y ) <-> ( z F A ) R ( z F y ) ) ) |
6 |
3 5
|
imbi12d |
|- ( x = A -> ( ( x R y -> ( z F x ) R ( z F y ) ) <-> ( A R y -> ( z F A ) R ( z F y ) ) ) ) |
7 |
|
breq2 |
|- ( y = B -> ( A R y <-> A R B ) ) |
8 |
|
oveq2 |
|- ( y = B -> ( z F y ) = ( z F B ) ) |
9 |
8
|
breq2d |
|- ( y = B -> ( ( z F A ) R ( z F y ) <-> ( z F A ) R ( z F B ) ) ) |
10 |
7 9
|
imbi12d |
|- ( y = B -> ( ( A R y -> ( z F A ) R ( z F y ) ) <-> ( A R B -> ( z F A ) R ( z F B ) ) ) ) |
11 |
|
oveq1 |
|- ( z = C -> ( z F A ) = ( C F A ) ) |
12 |
|
oveq1 |
|- ( z = C -> ( z F B ) = ( C F B ) ) |
13 |
11 12
|
breq12d |
|- ( z = C -> ( ( z F A ) R ( z F B ) <-> ( C F A ) R ( C F B ) ) ) |
14 |
13
|
imbi2d |
|- ( z = C -> ( ( A R B -> ( z F A ) R ( z F B ) ) <-> ( A R B -> ( C F A ) R ( C F B ) ) ) ) |
15 |
6 10 14
|
rspc3v |
|- ( ( A e. S /\ B e. S /\ C e. S ) -> ( A. x e. S A. y e. S A. z e. S ( x R y -> ( z F x ) R ( z F y ) ) -> ( A R B -> ( C F A ) R ( C F B ) ) ) ) |
16 |
2 15
|
mpan9 |
|- ( ( ph /\ ( A e. S /\ B e. S /\ C e. S ) ) -> ( A R B -> ( C F A ) R ( C F B ) ) ) |