Metamath Proof Explorer

Theorem ofrfval

Description: Value of a relation applied to two functions. (Contributed by Mario Carneiro, 28-Jul-2014)

Ref Expression
Hypotheses offval.1 
|- ( ph -> F Fn A )
offval.2 
|- ( ph -> G Fn B )
offval.3 
|- ( ph -> A e. V )
offval.4 
|- ( ph -> B e. W )
offval.5 
|- ( A i^i B ) = S
offval.6 
|- ( ( ph /\ x e. A ) -> ( F ` x ) = C )
offval.7 
|- ( ( ph /\ x e. B ) -> ( G ` x ) = D )
Assertion ofrfval 
|- ( ph -> ( F oR R G <-> A. x e. S C R D ) )

Proof

Step Hyp Ref Expression
1 offval.1 
 |-  ( ph -> F Fn A )
2 offval.2 
 |-  ( ph -> G Fn B )
3 offval.3 
 |-  ( ph -> A e. V )
4 offval.4 
 |-  ( ph -> B e. W )
5 offval.5 
 |-  ( A i^i B ) = S
6 offval.6 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) = C )
7 offval.7 
 |-  ( ( ph /\ x e. B ) -> ( G ` x ) = D )
8 fnex 
 |-  ( ( F Fn A /\ A e. V ) -> F e. _V )
9 1 3 8 syl2anc 
 |-  ( ph -> F e. _V )
10 fnex 
 |-  ( ( G Fn B /\ B e. W ) -> G e. _V )
11 2 4 10 syl2anc 
 |-  ( ph -> G e. _V )
12 dmeq 
 |-  ( f = F -> dom f = dom F )
13 dmeq 
 |-  ( g = G -> dom g = dom G )
14 12 13 ineqan12d 
 |-  ( ( f = F /\ g = G ) -> ( dom f i^i dom g ) = ( dom F i^i dom G ) )
15 fveq1 
 |-  ( f = F -> ( f ` x ) = ( F ` x ) )
16 fveq1 
 |-  ( g = G -> ( g ` x ) = ( G ` x ) )
17 15 16 breqan12d 
 |-  ( ( f = F /\ g = G ) -> ( ( f ` x ) R ( g ` x ) <-> ( F ` x ) R ( G ` x ) ) )
18 14 17 raleqbidv 
 |-  ( ( f = F /\ g = G ) -> ( A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) <-> A. x e. ( dom F i^i dom G ) ( F ` x ) R ( G ` x ) ) )
19 df-ofr 
 |-  oR R = { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) }
20 18 19 brabga 
 |-  ( ( F e. _V /\ G e. _V ) -> ( F oR R G <-> A. x e. ( dom F i^i dom G ) ( F ` x ) R ( G ` x ) ) )
21 9 11 20 syl2anc 
 |-  ( ph -> ( F oR R G <-> A. x e. ( dom F i^i dom G ) ( F ` x ) R ( G ` x ) ) )
22 1 fndmd 
 |-  ( ph -> dom F = A )
23 2 fndmd 
 |-  ( ph -> dom G = B )
24 22 23 ineq12d 
 |-  ( ph -> ( dom F i^i dom G ) = ( A i^i B ) )
25 24 5 syl6eq 
 |-  ( ph -> ( dom F i^i dom G ) = S )
26 25 raleqdv 
 |-  ( ph -> ( A. x e. ( dom F i^i dom G ) ( F ` x ) R ( G ` x ) <-> A. x e. S ( F ` x ) R ( G ` x ) ) )
27 inss1 
 |-  ( A i^i B ) C_ A
28 5 27 eqsstrri 
 |-  S C_ A
29 28 sseli 
 |-  ( x e. S -> x e. A )
30 29 6 sylan2 
 |-  ( ( ph /\ x e. S ) -> ( F ` x ) = C )
31 inss2 
 |-  ( A i^i B ) C_ B
32 5 31 eqsstrri 
 |-  S C_ B
33 32 sseli 
 |-  ( x e. S -> x e. B )
34 33 7 sylan2 
 |-  ( ( ph /\ x e. S ) -> ( G ` x ) = D )
35 30 34 breq12d 
 |-  ( ( ph /\ x e. S ) -> ( ( F ` x ) R ( G ` x ) <-> C R D ) )
36 35 ralbidva 
 |-  ( ph -> ( A. x e. S ( F ` x ) R ( G ` x ) <-> A. x e. S C R D ) )
37 21 26 36 3bitrd 
 |-  ( ph -> ( F oR R G <-> A. x e. S C R D ) )