ofrval

Description: Exhibit a function relation at a point. (Contributed by Mario Carneiro, 28-Jul-2014)

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		ofval.6	$⊢ (φ \land X \in A) \to F (X) = C$
7		ofval.7	$⊢ (φ \land X \in B) \to G (X) = D$
8		eqidd	$⊢ (φ \land x \in A) \to F (x) = F (x)$
9		eqidd	$⊢ (φ \land x \in B) \to G (x) = G (x)$
10	1 2 3 4 5 8 9	ofrfval	$⊢ φ \to (F R_{f} G \leftrightarrow \forall x \in S F (x) R G (x))$
11	10	biimpa	$⊢ (φ \land F R_{f} G) \to \forall x \in S F (x) R G (x)$
12		fveq2	$⊢ x = X \to F (x) = F (X)$
13		fveq2	$⊢ x = X \to G (x) = G (X)$
14	12 13	breq12d	$⊢ x = X \to (F (x) R G (x) \leftrightarrow F (X) R G (X))$
15	14	rspccv	$⊢ \forall x \in S F (x) R G (x) \to (X \in S \to F (X) R G (X))$
16	11 15	syl	$⊢ (φ \land F R_{f} G) \to (X \in S \to F (X) R G (X))$
17	16	3impia	$⊢ (φ \land F R_{f} G \land X \in S) \to F (X) R G (X)$
18		simp1	$⊢ (φ \land F R_{f} G \land X \in S) \to φ$
19		inss1	$⊢ A \cap B \subseteq A$
20	5 19	eqsstrri	$⊢ S \subseteq A$
21		simp3	$⊢ (φ \land F R_{f} G \land X \in S) \to X \in S$
22	20 21	sseldi	$⊢ (φ \land F R_{f} G \land X \in S) \to X \in A$
23	18 22 6	syl2anc	$⊢ (φ \land F R_{f} G \land X \in S) \to F (X) = C$
24		inss2	$⊢ A \cap B \subseteq B$
25	5 24	eqsstrri	$⊢ S \subseteq B$
26	25 21	sseldi	$⊢ (φ \land F R_{f} G \land X \in S) \to X \in B$
27	18 26 7	syl2anc	$⊢ (φ \land F R_{f} G \land X \in S) \to G (X) = D$
28	17 23 27	3brtr3d	$⊢ (φ \land F R_{f} G \land X \in S) \to C R D$

Metamath Proof Explorer