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 ( 𝜑𝐹 Fn 𝐴 )
ofrfvalg.2 ( 𝜑𝐺 Fn 𝐵 )
ofrfvalg.3 ( 𝜑𝐹𝑉 )
ofrfvalg.4 ( 𝜑𝐺𝑊 )
ofrfvalg.5 ( 𝐴𝐵 ) = 𝑆
ofrfvalg.6 ( ( 𝜑𝑥𝐴 ) → ( 𝐹𝑥 ) = 𝐶 )
ofrfvalg.7 ( ( 𝜑𝑥𝐵 ) → ( 𝐺𝑥 ) = 𝐷 )
Assertion ofrfvalg ( 𝜑 → ( 𝐹r 𝑅 𝐺 ↔ ∀ 𝑥𝑆 𝐶 𝑅 𝐷 ) )

Proof

Step Hyp Ref Expression
1 ofrfvalg.1 ( 𝜑𝐹 Fn 𝐴 )
2 ofrfvalg.2 ( 𝜑𝐺 Fn 𝐵 )
3 ofrfvalg.3 ( 𝜑𝐹𝑉 )
4 ofrfvalg.4 ( 𝜑𝐺𝑊 )
5 ofrfvalg.5 ( 𝐴𝐵 ) = 𝑆
6 ofrfvalg.6 ( ( 𝜑𝑥𝐴 ) → ( 𝐹𝑥 ) = 𝐶 )
7 ofrfvalg.7 ( ( 𝜑𝑥𝐵 ) → ( 𝐺𝑥 ) = 𝐷 )
8 dmeq ( 𝑓 = 𝐹 → dom 𝑓 = dom 𝐹 )
9 dmeq ( 𝑔 = 𝐺 → dom 𝑔 = dom 𝐺 )
10 8 9 ineqan12d ( ( 𝑓 = 𝐹𝑔 = 𝐺 ) → ( dom 𝑓 ∩ dom 𝑔 ) = ( dom 𝐹 ∩ dom 𝐺 ) )
11 fveq1 ( 𝑓 = 𝐹 → ( 𝑓𝑥 ) = ( 𝐹𝑥 ) )
12 fveq1 ( 𝑔 = 𝐺 → ( 𝑔𝑥 ) = ( 𝐺𝑥 ) )
13 11 12 breqan12d ( ( 𝑓 = 𝐹𝑔 = 𝐺 ) → ( ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) ↔ ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) ) )
14 10 13 raleqbidv ( ( 𝑓 = 𝐹𝑔 = 𝐺 ) → ( ∀ 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) ↔ ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) ) )
15 df-ofr r 𝑅 = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ∀ 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) }
16 14 15 brabga ( ( 𝐹𝑉𝐺𝑊 ) → ( 𝐹r 𝑅 𝐺 ↔ ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) ) )
17 3 4 16 syl2anc ( 𝜑 → ( 𝐹r 𝑅 𝐺 ↔ ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) ) )
18 1 fndmd ( 𝜑 → dom 𝐹 = 𝐴 )
19 2 fndmd ( 𝜑 → dom 𝐺 = 𝐵 )
20 18 19 ineq12d ( 𝜑 → ( dom 𝐹 ∩ dom 𝐺 ) = ( 𝐴𝐵 ) )
21 20 5 eqtrdi ( 𝜑 → ( dom 𝐹 ∩ dom 𝐺 ) = 𝑆 )
22 21 raleqdv ( 𝜑 → ( ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) ↔ ∀ 𝑥𝑆 ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) ) )
23 inss1 ( 𝐴𝐵 ) ⊆ 𝐴
24 5 23 eqsstrri 𝑆𝐴
25 24 sseli ( 𝑥𝑆𝑥𝐴 )
26 25 6 sylan2 ( ( 𝜑𝑥𝑆 ) → ( 𝐹𝑥 ) = 𝐶 )
27 inss2 ( 𝐴𝐵 ) ⊆ 𝐵
28 5 27 eqsstrri 𝑆𝐵
29 28 sseli ( 𝑥𝑆𝑥𝐵 )
30 29 7 sylan2 ( ( 𝜑𝑥𝑆 ) → ( 𝐺𝑥 ) = 𝐷 )
31 26 30 breq12d ( ( 𝜑𝑥𝑆 ) → ( ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) ↔ 𝐶 𝑅 𝐷 ) )
32 31 ralbidva ( 𝜑 → ( ∀ 𝑥𝑆 ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) ↔ ∀ 𝑥𝑆 𝐶 𝑅 𝐷 ) )
33 17 22 32 3bitrd ( 𝜑 → ( 𝐹r 𝑅 𝐺 ↔ ∀ 𝑥𝑆 𝐶 𝑅 𝐷 ) )