Metamath Proof Explorer

Theorem oprssov

Description: The value of a member of the domain of a subclass of an operation. (Contributed by NM, 23-Aug-2007)

Ref Expression
Assertion oprssov 
|- ( ( ( Fun F /\ G Fn ( C X. D ) /\ G C_ F ) /\ ( A e. C /\ B e. D ) ) -> ( A F B ) = ( A G B ) )

Proof

Step Hyp Ref Expression
1 ovres 
 |-  ( ( A e. C /\ B e. D ) -> ( A ( F |` ( C X. D ) ) B ) = ( A F B ) )
2 1 adantl 
 |-  ( ( ( Fun F /\ G Fn ( C X. D ) /\ G C_ F ) /\ ( A e. C /\ B e. D ) ) -> ( A ( F |` ( C X. D ) ) B ) = ( A F B ) )
3 fndm 
 |-  ( G Fn ( C X. D ) -> dom G = ( C X. D ) )
4 3 reseq2d 
 |-  ( G Fn ( C X. D ) -> ( F |` dom G ) = ( F |` ( C X. D ) ) )
5 4 3ad2ant2 
 |-  ( ( Fun F /\ G Fn ( C X. D ) /\ G C_ F ) -> ( F |` dom G ) = ( F |` ( C X. D ) ) )
6 funssres 
 |-  ( ( Fun F /\ G C_ F ) -> ( F |` dom G ) = G )
7 6 3adant2 
 |-  ( ( Fun F /\ G Fn ( C X. D ) /\ G C_ F ) -> ( F |` dom G ) = G )
8 5 7 eqtr3d 
 |-  ( ( Fun F /\ G Fn ( C X. D ) /\ G C_ F ) -> ( F |` ( C X. D ) ) = G )
9 8 oveqd 
 |-  ( ( Fun F /\ G Fn ( C X. D ) /\ G C_ F ) -> ( A ( F |` ( C X. D ) ) B ) = ( A G B ) )
10 9 adantr 
 |-  ( ( ( Fun F /\ G Fn ( C X. D ) /\ G C_ F ) /\ ( A e. C /\ B e. D ) ) -> ( A ( F |` ( C X. D ) ) B ) = ( A G B ) )
11 2 10 eqtr3d 
 |-  ( ( ( Fun F /\ G Fn ( C X. D ) /\ G C_ F ) /\ ( A e. C /\ B e. D ) ) -> ( A F B ) = ( A G B ) )