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 φ F Fn A
ofrfvalg.2 φ G Fn B
ofrfvalg.3 φ F V
ofrfvalg.4 φ G W
ofrfvalg.5 A B = S
ofrfvalg.6 φ x A F x = C
ofrfvalg.7 φ x B G x = D
Assertion ofrfvalg φ F R f G x S C R D

Proof

Step Hyp Ref Expression
1 ofrfvalg.1 φ F Fn A
2 ofrfvalg.2 φ G Fn B
3 ofrfvalg.3 φ F V
4 ofrfvalg.4 φ G W
5 ofrfvalg.5 A B = S
6 ofrfvalg.6 φ x A F x = C
7 ofrfvalg.7 φ x 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 dom g = dom F 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 x dom f dom g f x R g x x dom F dom G F x R G x
15 df-ofr r R = f g | x dom f dom g f x R g x
16 14 15 brabga F V G W F R f G x dom F dom G F x R G x
17 3 4 16 syl2anc φ F R f G x dom F dom G F x R G x
18 1 fndmd φ dom F = A
19 2 fndmd φ dom G = B
20 18 19 ineq12d φ dom F dom G = A B
21 20 5 eqtrdi φ dom F dom G = S
22 21 raleqdv φ x dom F dom G F x R G x x S F x R G x
23 inss1 A B A
24 5 23 eqsstrri S A
25 24 sseli x S x A
26 25 6 sylan2 φ x S F x = C
27 inss2 A B B
28 5 27 eqsstrri S B
29 28 sseli x S x B
30 29 7 sylan2 φ x S G x = D
31 26 30 breq12d φ x S F x R G x C R D
32 31 ralbidva φ x S F x R G x x S C R D
33 17 22 32 3bitrd φ F R f G x S C R D