This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem caovord

Description: Convert an operation ordering law to class notation. (Contributed by NM, 19-Feb-1996)

Ref Expression
Hypotheses caovord.1 
|- A e. _V
caovord.2 
|- B e. _V
caovord.3 
|- ( z e. S -> ( x R y <-> ( z F x ) R ( z F y ) ) )
Assertion caovord 
|- ( C e. S -> ( A R B <-> ( C F A ) R ( C F B ) ) )

Proof

Step Hyp Ref Expression
1 caovord.1 
 |-  A e. _V
2 caovord.2 
 |-  B e. _V
3 caovord.3 
 |-  ( z e. S -> ( x R y <-> ( z F x ) R ( z F y ) ) )
4 oveq1 
 |-  ( z = C -> ( z F A ) = ( C F A ) )
5 oveq1 
 |-  ( z = C -> ( z F B ) = ( C F B ) )
6 4 5 breq12d 
 |-  ( z = C -> ( ( z F A ) R ( z F B ) <-> ( C F A ) R ( C F B ) ) )
7 6 bibi2d 
 |-  ( z = C -> ( ( A R B <-> ( z F A ) R ( z F B ) ) <-> ( A R B <-> ( C F A ) R ( C F B ) ) ) )
8 breq1 
 |-  ( x = A -> ( x R y <-> A R y ) )
9 oveq2 
 |-  ( x = A -> ( z F x ) = ( z F A ) )
10 9 breq1d 
 |-  ( x = A -> ( ( z F x ) R ( z F y ) <-> ( z F A ) R ( z F y ) ) )
11 8 10 bibi12d 
 |-  ( x = A -> ( ( x R y <-> ( z F x ) R ( z F y ) ) <-> ( A R y <-> ( z F A ) R ( z F y ) ) ) )
12 breq2 
 |-  ( y = B -> ( A R y <-> A R B ) )
13 oveq2 
 |-  ( y = B -> ( z F y ) = ( z F B ) )
14 13 breq2d 
 |-  ( y = B -> ( ( z F A ) R ( z F y ) <-> ( z F A ) R ( z F B ) ) )
15 12 14 bibi12d 
 |-  ( y = B -> ( ( A R y <-> ( z F A ) R ( z F y ) ) <-> ( A R B <-> ( z F A ) R ( z F B ) ) ) )
16 11 15 sylan9bb 
 |-  ( ( x = A /\ y = B ) -> ( ( x R y <-> ( z F x ) R ( z F y ) ) <-> ( A R B <-> ( z F A ) R ( z F B ) ) ) )
17 16 imbi2d 
 |-  ( ( x = A /\ y = B ) -> ( ( z e. S -> ( x R y <-> ( z F x ) R ( z F y ) ) ) <-> ( z e. S -> ( A R B <-> ( z F A ) R ( z F B ) ) ) ) )
18 1 2 17 3 vtocl2 
 |-  ( z e. S -> ( A R B <-> ( z F A ) R ( z F B ) ) )
19 7 18 vtoclga 
 |-  ( C e. S -> ( A R B <-> ( C F A ) R ( C F B ) ) )