Metamath Proof Explorer


Theorem caovordig

Description: Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 31-Dec-2014)

Ref Expression
Hypothesis caovordig.1
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( x R y -> ( z F x ) R ( z F y ) ) )
Assertion caovordig
|- ( ( 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 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 ) ) )