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