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	$⊢ φ \to F Fn A$
	ofrfvalg.2	$⊢ φ \to G Fn B$
	ofrfvalg.3	$⊢ φ \to F \in V$
	ofrfvalg.4	$⊢ φ \to G \in W$
	ofrfvalg.5	$⊢ A \cap B = S$
	ofrfvalg.6	$⊢ (φ \land x \in A) \to F (x) = C$
	ofrfvalg.7	$⊢ (φ \land x \in B) \to G (x) = D$
Assertion	ofrfvalg	$⊢ φ \to (F R_{f} G \leftrightarrow \forall x \in S C R D)$

Proof

Step	Hyp	Ref	Expression
1		ofrfvalg.1	$⊢ φ \to F Fn A$
2		ofrfvalg.2	$⊢ φ \to G Fn B$
3		ofrfvalg.3	$⊢ φ \to F \in V$
4		ofrfvalg.4	$⊢ φ \to G \in W$
5		ofrfvalg.5	$⊢ A \cap B = S$
6		ofrfvalg.6	$⊢ (φ \land x \in A) \to F (x) = C$
7		ofrfvalg.7	$⊢ (φ \land x \in B) \to G (x) = D$
8		dmeq	$⊢ f = F \to dom f = dom F$
9		dmeq	$⊢ g = G \to dom g = dom G$
10	8 9	ineqan12d	$⊢ (f = F \land g = G) \to dom f \cap dom g = dom F \cap dom G$
11		fveq1	$⊢ f = F \to f (x) = F (x)$
12		fveq1	$⊢ g = G \to g (x) = G (x)$
13	11 12	breqan12d	$⊢ (f = F \land g = G) \to (f (x) R g (x) \leftrightarrow F (x) R G (x))$
14	10 13	raleqbidv	$⊢ (f = F \land g = G) \to (\forall x \in (dom f \cap dom g) f (x) R g (x) \leftrightarrow \forall x \in (dom F \cap dom G) F (x) R G (x))$
15		df-ofr	$⊢ \circ_{r} R = \{⟨f, g⟩ \| \forall x \in (dom f \cap dom g) f (x) R g (x)\}$
16	14 15	brabga	$⊢ (F \in V \land G \in W) \to (F R_{f} G \leftrightarrow \forall x \in (dom F \cap dom G) F (x) R G (x))$
17	3 4 16	syl2anc	$⊢ φ \to (F R_{f} G \leftrightarrow \forall x \in (dom F \cap dom G) F (x) R G (x))$
18	1	fndmd	$⊢ φ \to dom F = A$
19	2	fndmd	$⊢ φ \to dom G = B$
20	18 19	ineq12d	$⊢ φ \to dom F \cap dom G = A \cap B$
21	20 5	eqtrdi	$⊢ φ \to dom F \cap dom G = S$
22	21	raleqdv	$⊢ φ \to (\forall x \in (dom F \cap dom G) F (x) R G (x) \leftrightarrow \forall x \in S F (x) R G (x))$
23		inss1	$⊢ A \cap B \subseteq A$
24	5 23	eqsstrri	$⊢ S \subseteq A$
25	24	sseli	$⊢ x \in S \to x \in A$
26	25 6	sylan2	$⊢ (φ \land x \in S) \to F (x) = C$
27		inss2	$⊢ A \cap B \subseteq B$
28	5 27	eqsstrri	$⊢ S \subseteq B$
29	28	sseli	$⊢ x \in S \to x \in B$
30	29 7	sylan2	$⊢ (φ \land x \in S) \to G (x) = D$
31	26 30	breq12d	$⊢ (φ \land x \in S) \to (F (x) R G (x) \leftrightarrow C R D)$
32	31	ralbidva	$⊢ φ \to (\forall x \in S F (x) R G (x) \leftrightarrow \forall x \in S C R D)$
33	17 22 32	3bitrd	$⊢ φ \to (F R_{f} G \leftrightarrow \forall x \in S C R D)$

Metamath Proof Explorer

Theorem ofrfvalg

Proof