ofrfval

Description: Value of a relation applied to two functions. (Contributed by Mario Carneiro, 28-Jul-2014)

	Ref	Expression
Hypotheses	offval.1	$⊢ φ \to F Fn A$
	offval.2	$⊢ φ \to G Fn B$
	offval.3	$⊢ φ \to A \in V$
	offval.4	$⊢ φ \to B \in W$
	offval.5	$⊢ A \cap B = S$
	offval.6	$⊢ (φ \land x \in A) \to F (x) = C$
	offval.7	$⊢ (φ \land x \in B) \to G (x) = D$
Assertion	ofrfval	$⊢ φ \to (F R_{f} G \leftrightarrow \forall x \in S C R D)$

Proof

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

Metamath Proof Explorer

Theorem ofrfval

Proof