Metamath Proof Explorer

Theorem caovordg

Description: Convert an operation ordering law to class notation. (Contributed by NM, 19-Feb-1996) (Revised by Mario Carneiro, 30-Dec-2014)

Ref Expression
Hypothesis caovordg.1 
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( x R y <-> ( z F x ) R ( z F y ) ) )
Assertion caovordg 
|- ( ( ph /\ ( A e. S /\ B e. S /\ C e. S ) ) -> ( A R B <-> ( C F A ) R ( C F B ) ) )

Proof

Step Hyp Ref Expression
1 caovordg.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 bibi12d 
 |-  ( 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 bibi12d 
 |-  ( 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 bibi2d 
 |-  ( 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 ) ) )