Metamath Proof Explorer

Theorem offval3

Description: General value of ( F oF R G ) with no assumptions on functionality of F and G . (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Assertion offval3 
|- ( ( F e. V /\ G e. W ) -> ( F oF R G ) = ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( F e. V -> F e. _V )
2 1 adantr 
 |-  ( ( F e. V /\ G e. W ) -> F e. _V )
3 elex 
 |-  ( G e. W -> G e. _V )
4 3 adantl 
 |-  ( ( F e. V /\ G e. W ) -> G e. _V )
5 dmexg 
 |-  ( F e. V -> dom F e. _V )
6 inex1g 
 |-  ( dom F e. _V -> ( dom F i^i dom G ) e. _V )
7 mptexg 
 |-  ( ( dom F i^i dom G ) e. _V -> ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) e. _V )
8 5 6 7 3syl 
 |-  ( F e. V -> ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) e. _V )
9 8 adantr 
 |-  ( ( F e. V /\ G e. W ) -> ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) e. _V )
10 dmeq 
 |-  ( a = F -> dom a = dom F )
11 dmeq 
 |-  ( b = G -> dom b = dom G )
12 10 11 ineqan12d 
 |-  ( ( a = F /\ b = G ) -> ( dom a i^i dom b ) = ( dom F i^i dom G ) )
13 fveq1 
 |-  ( a = F -> ( a ` x ) = ( F ` x ) )
14 fveq1 
 |-  ( b = G -> ( b ` x ) = ( G ` x ) )
15 13 14 oveqan12d 
 |-  ( ( a = F /\ b = G ) -> ( ( a ` x ) R ( b ` x ) ) = ( ( F ` x ) R ( G ` x ) ) )
16 12 15 mpteq12dv 
 |-  ( ( a = F /\ b = G ) -> ( x e. ( dom a i^i dom b ) |-> ( ( a ` x ) R ( b ` x ) ) ) = ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) )
17 df-of 
 |-  oF R = ( a e. _V , b e. _V |-> ( x e. ( dom a i^i dom b ) |-> ( ( a ` x ) R ( b ` x ) ) ) )
18 16 17 ovmpoga 
 |-  ( ( F e. _V /\ G e. _V /\ ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) e. _V ) -> ( F oF R G ) = ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) )
19 2 4 9 18 syl3anc 
 |-  ( ( F e. V /\ G e. W ) -> ( F oF R G ) = ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) )