Metamath Proof Explorer

Theorem rescofuf

Description: The restriction of functor composition is a function from product functor space to functor space. (Contributed by Zhi Wang, 25-Sep-2025)

		Ref	Expression
	Assertion	rescofuf	$⊢ ({\circ_{func} ↾}_{((D Func E) \times (C Func D))}) : (D Func E) \times (C Func D) ⟶ C Func E$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ g \in V$
2		vex	$⊢ f \in V$
3		opex	$⊢ ⟨1^{st} (g) \circ 1^{st} (f), (x \in dom dom 2^{nd} (f), y \in dom dom 2^{nd} (f) ⟼ (1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y)) \circ (x 2^{nd} (f) y))⟩ \in V$
4		df-cofu	$⊢ \circ_{func} = (g \in V, f \in V ⟼ ⟨1^{st} (g) \circ 1^{st} (f), (x \in dom dom 2^{nd} (f), y \in dom dom 2^{nd} (f) ⟼ (1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y)) \circ (x 2^{nd} (f) y))⟩)$
5	4	ovmpt4g	$⊢ (g \in V \land f \in V \land ⟨1^{st} (g) \circ 1^{st} (f), (x \in dom dom 2^{nd} (f), y \in dom dom 2^{nd} (f) ⟼ (1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y)) \circ (x 2^{nd} (f) y))⟩ \in V) \to g \circ_{func} f = ⟨1^{st} (g) \circ 1^{st} (f), (x \in dom dom 2^{nd} (f), y \in dom dom 2^{nd} (f) ⟼ (1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y)) \circ (x 2^{nd} (f) y))⟩$
6	1 2 3 5	mp3an	$⊢ g \circ_{func} f = ⟨1^{st} (g) \circ 1^{st} (f), (x \in dom dom 2^{nd} (f), y \in dom dom 2^{nd} (f) ⟼ (1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y)) \circ (x 2^{nd} (f) y))⟩$
7		simpr	$⊢ (g \in (D Func E) \land f \in (C Func D)) \to f \in (C Func D)$
8		simpl	$⊢ (g \in (D Func E) \land f \in (C Func D)) \to g \in (D Func E)$
9	7 8	cofucl	$⊢ (g \in (D Func E) \land f \in (C Func D)) \to g \circ_{func} f \in (C Func E)$
10	6 9	eqeltrrid	$⊢ (g \in (D Func E) \land f \in (C Func D)) \to ⟨1^{st} (g) \circ 1^{st} (f), (x \in dom dom 2^{nd} (f), y \in dom dom 2^{nd} (f) ⟼ (1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y)) \circ (x 2^{nd} (f) y))⟩ \in (C Func E)$
11	10	rgen2	$⊢ \forall g \in (D Func E) \forall f \in (C Func D) ⟨1^{st} (g) \circ 1^{st} (f), (x \in dom dom 2^{nd} (f), y \in dom dom 2^{nd} (f) ⟼ (1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y)) \circ (x 2^{nd} (f) y))⟩ \in (C Func E)$
12	4	reseq1i	$⊢ {\circ_{func} ↾}_{((D Func E) \times (C Func D))} = {(g \in V, f \in V ⟼ ⟨1^{st} (g) \circ 1^{st} (f), (x \in dom dom 2^{nd} (f), y \in dom dom 2^{nd} (f) ⟼ (1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y)) \circ (x 2^{nd} (f) y))⟩) ↾}_{((D Func E) \times (C Func D))}$
13		ssv	$⊢ D Func E \subseteq V$
14		ssv	$⊢ C Func D \subseteq V$
15		resmpo	$⊢ (D Func E \subseteq V \land C Func D \subseteq V) \to {(g \in V, f \in V ⟼ ⟨1^{st} (g) \circ 1^{st} (f), (x \in dom dom 2^{nd} (f), y \in dom dom 2^{nd} (f) ⟼ (1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y)) \circ (x 2^{nd} (f) y))⟩) ↾}_{((D Func E) \times (C Func D))} = (g \in (D Func E), f \in (C Func D) ⟼ ⟨1^{st} (g) \circ 1^{st} (f), (x \in dom dom 2^{nd} (f), y \in dom dom 2^{nd} (f) ⟼ (1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y)) \circ (x 2^{nd} (f) y))⟩)$
16	13 14 15	mp2an	$⊢ {(g \in V, f \in V ⟼ ⟨1^{st} (g) \circ 1^{st} (f), (x \in dom dom 2^{nd} (f), y \in dom dom 2^{nd} (f) ⟼ (1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y)) \circ (x 2^{nd} (f) y))⟩) ↾}_{((D Func E) \times (C Func D))} = (g \in (D Func E), f \in (C Func D) ⟼ ⟨1^{st} (g) \circ 1^{st} (f), (x \in dom dom 2^{nd} (f), y \in dom dom 2^{nd} (f) ⟼ (1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y)) \circ (x 2^{nd} (f) y))⟩)$
17	12 16	eqtri	$⊢ {\circ_{func} ↾}_{((D Func E) \times (C Func D))} = (g \in (D Func E), f \in (C Func D) ⟼ ⟨1^{st} (g) \circ 1^{st} (f), (x \in dom dom 2^{nd} (f), y \in dom dom 2^{nd} (f) ⟼ (1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y)) \circ (x 2^{nd} (f) y))⟩)$
18	17	fmpo	$⊢ \forall g \in (D Func E) \forall f \in (C Func D) ⟨1^{st} (g) \circ 1^{st} (f), (x \in dom dom 2^{nd} (f), y \in dom dom 2^{nd} (f) ⟼ (1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y)) \circ (x 2^{nd} (f) y))⟩ \in (C Func E) \leftrightarrow ({\circ_{func} ↾}_{((D Func E) \times (C Func D))}) : (D Func E) \times (C Func D) ⟶ C Func E$
19	11 18	mpbi	$⊢ ({\circ_{func} ↾}_{((D Func E) \times (C Func D))}) : (D Func E) \times (C Func D) ⟶ C Func E$