off2

Description: The function operation produces a function - alternative form with all antecedents as deduction. (Contributed by Thierry Arnoux, 17-Feb-2017)

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

Proof

Step	Hyp	Ref	Expression
1		off2.1	$⊢ (φ \land (x \in S \land y \in T)) \to x R y \in U$
2		off2.2	$⊢ φ \to F : A ⟶ S$
3		off2.3	$⊢ φ \to G : B ⟶ T$
4		off2.4	$⊢ φ \to A \in V$
5		off2.5	$⊢ φ \to B \in W$
6		off2.6	$⊢ φ \to A \cap B = C$
7	2	ffnd	$⊢ φ \to F Fn A$
8	3	ffnd	$⊢ φ \to G Fn B$
9		eqid	$⊢ A \cap B = A \cap B$
10		eqidd	$⊢ (φ \land z \in A) \to F (z) = F (z)$
11		eqidd	$⊢ (φ \land z \in B) \to G (z) = G (z)$
12	7 8 4 5 9 10 11	offval	$⊢ φ \to F R_{f} G = (z \in (A \cap B) ⟼ F (z) R G (z))$
13	6	mpteq1d	$⊢ φ \to (z \in (A \cap B) ⟼ F (z) R G (z)) = (z \in C ⟼ F (z) R G (z))$
14	12 13	eqtrd	$⊢ φ \to F R_{f} G = (z \in C ⟼ F (z) R G (z))$
15	2	adantr	$⊢ (φ \land z \in C) \to F : A ⟶ S$
16		inss1	$⊢ A \cap B \subseteq A$
17	6 16	eqsstrrdi	$⊢ φ \to C \subseteq A$
18	17	sselda	$⊢ (φ \land z \in C) \to z \in A$
19	15 18	ffvelrnd	$⊢ (φ \land z \in C) \to F (z) \in S$
20	3	adantr	$⊢ (φ \land z \in C) \to G : B ⟶ T$
21		inss2	$⊢ A \cap B \subseteq B$
22	6 21	eqsstrrdi	$⊢ φ \to C \subseteq B$
23	22	sselda	$⊢ (φ \land z \in C) \to z \in B$
24	20 23	ffvelrnd	$⊢ (φ \land z \in C) \to G (z) \in T$
25	1	ralrimivva	$⊢ φ \to \forall x \in S \forall y \in T x R y \in U$
26	25	adantr	$⊢ (φ \land z \in C) \to \forall x \in S \forall y \in T x R y \in U$
27		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$
28	19 24 26 27	syl21anc	$⊢ (φ \land z \in C) \to F (z) R G (z) \in U$
29	14 28	fmpt3d	$⊢ φ \to (F R_{f} G) : C ⟶ U$

Metamath Proof Explorer

Theorem off2

Proof