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 𝑅 𝐺 ↔ ∀ 𝑥 ∈ 𝑆 𝐶 𝑅 𝐷 ) )

Metamath Proof Explorer

Theorem ofrfvalg

Proof