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 ) )