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

Metamath Proof Explorer

Theorem ofrfvalg

Description: Value of a relation applied to two functions. Originally part of ofrfval , this version assumes the functions are sets rather than their domains, avoiding ax-rep . (Contributed by SN, 5-Aug-2024)

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

Proof

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