off

Description: The function operation produces a function. (Contributed by Mario Carneiro, 20-Jul-2014)

	Ref	Expression
Hypotheses	off.1	$⊢ (φ \land (x \in S \land y \in T)) \to x R y \in U$
	off.2	$⊢ φ \to F : A ⟶ S$
	off.3	$⊢ φ \to G : B ⟶ T$
	off.4	$⊢ φ \to A \in V$
	off.5	$⊢ φ \to B \in W$
	off.6	$⊢ A \cap B = C$
Assertion	off	$⊢ φ \to (F R_{f} G) : C ⟶ U$

Step	Hyp	Ref	Expression
1		off.1	$⊢ (φ \land (x \in S \land y \in T)) \to x R y \in U$
2		off.2	$⊢ φ \to F : A ⟶ S$
3		off.3	$⊢ φ \to G : B ⟶ T$
4		off.4	$⊢ φ \to A \in V$
5		off.5	$⊢ φ \to B \in W$
6		off.6	$⊢ A \cap B = C$
7	2	ffnd	$⊢ φ \to F Fn A$
8	3	ffnd	$⊢ φ \to G Fn B$
9		eqidd	$⊢ (φ \land z \in A) \to F (z) = F (z)$
10		eqidd	$⊢ (φ \land z \in B) \to G (z) = G (z)$
11	7 8 4 5 6 9 10	offval	$⊢ φ \to F R_{f} G = (z \in C ⟼ F (z) R G (z))$
12		inss1	$⊢ A \cap B \subseteq A$
13	6 12	eqsstrri	$⊢ C \subseteq A$
14	13	sseli	$⊢ z \in C \to z \in A$
15		ffvelcdm	$⊢ (F : A ⟶ S \land z \in A) \to F (z) \in S$
16	2 14 15	syl2an	$⊢ (φ \land z \in C) \to F (z) \in S$
17		inss2	$⊢ A \cap B \subseteq B$
18	6 17	eqsstrri	$⊢ C \subseteq B$
19	18	sseli	$⊢ z \in C \to z \in B$
20		ffvelcdm	$⊢ (G : B ⟶ T \land z \in B) \to G (z) \in T$
21	3 19 20	syl2an	$⊢ (φ \land z \in C) \to G (z) \in T$
22	1	ralrimivva	$⊢ φ \to \forall x \in S \forall y \in T x R y \in U$
23	22	adantr	$⊢ (φ \land z \in C) \to \forall x \in S \forall y \in T x R y \in U$
24		ovrspc2v	$⊢ ((F (z) \in S \land G (z) \in T) \land \forall x \in S \forall y \in T x R y \in U) \to F (z) R G (z) \in U$
25	16 21 23 24	syl21anc	$⊢ (φ \land z \in C) \to F (z) R G (z) \in U$
26	11 25	fmpt3d	$⊢ φ \to (F R_{f} G) : C ⟶ U$

Metamath Proof Explorer