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	⊢ ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) : ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ⟶ ( 𝐶 Func 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑔 ∈ V
2		vex	⊢ 𝑓 ∈ V
3		opex	⊢ ⟨ ( ( 1^st ‘ 𝑔 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( 𝑥 ∈ dom dom ( 2^nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2^nd ‘ 𝑓 ) ↦ ( ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ) ) ⟩ ∈ V
4		df-cofu	⊢ ∘_func = ( 𝑔 ∈ V , 𝑓 ∈ V ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( 𝑥 ∈ dom dom ( 2^nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2^nd ‘ 𝑓 ) ↦ ( ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ) ) ⟩ )
5	4	ovmpt4g	⊢ ( ( 𝑔 ∈ V ∧ 𝑓 ∈ V ∧ ⟨ ( ( 1^st ‘ 𝑔 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( 𝑥 ∈ dom dom ( 2^nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2^nd ‘ 𝑓 ) ↦ ( ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ) ) ⟩ ∈ V ) → ( 𝑔 ∘_func 𝑓 ) = ⟨ ( ( 1^st ‘ 𝑔 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( 𝑥 ∈ dom dom ( 2^nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2^nd ‘ 𝑓 ) ↦ ( ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ) ) ⟩ )
6	1 2 3 5	mp3an	⊢ ( 𝑔 ∘_func 𝑓 ) = ⟨ ( ( 1^st ‘ 𝑔 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( 𝑥 ∈ dom dom ( 2^nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2^nd ‘ 𝑓 ) ↦ ( ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ) ) ⟩
7		simpr	⊢ ( ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) → 𝑓 ∈ ( 𝐶 Func 𝐷 ) )
8		simpl	⊢ ( ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) → 𝑔 ∈ ( 𝐷 Func 𝐸 ) )
9	7 8	cofucl	⊢ ( ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) → ( 𝑔 ∘_func 𝑓 ) ∈ ( 𝐶 Func 𝐸 ) )
10	6 9	eqeltrrid	⊢ ( ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) → ⟨ ( ( 1^st ‘ 𝑔 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( 𝑥 ∈ dom dom ( 2^nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2^nd ‘ 𝑓 ) ↦ ( ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ) ) ⟩ ∈ ( 𝐶 Func 𝐸 ) )
11	10	rgen2	⊢ ∀ 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∀ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ⟨ ( ( 1^st ‘ 𝑔 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( 𝑥 ∈ dom dom ( 2^nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2^nd ‘ 𝑓 ) ↦ ( ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ) ) ⟩ ∈ ( 𝐶 Func 𝐸 )
12	4	reseq1i	⊢ ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) = ( ( 𝑔 ∈ V , 𝑓 ∈ V ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( 𝑥 ∈ dom dom ( 2^nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2^nd ‘ 𝑓 ) ↦ ( ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ) ) ⟩ ) ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
13		ssv	⊢ ( 𝐷 Func 𝐸 ) ⊆ V
14		ssv	⊢ ( 𝐶 Func 𝐷 ) ⊆ V
15		resmpo	⊢ ( ( ( 𝐷 Func 𝐸 ) ⊆ V ∧ ( 𝐶 Func 𝐷 ) ⊆ V ) → ( ( 𝑔 ∈ V , 𝑓 ∈ V ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( 𝑥 ∈ dom dom ( 2^nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2^nd ‘ 𝑓 ) ↦ ( ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ) ) ⟩ ) ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) = ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) , 𝑓 ∈ ( 𝐶 Func 𝐷 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( 𝑥 ∈ dom dom ( 2^nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2^nd ‘ 𝑓 ) ↦ ( ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ) ) ⟩ ) )
16	13 14 15	mp2an	⊢ ( ( 𝑔 ∈ V , 𝑓 ∈ V ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( 𝑥 ∈ dom dom ( 2^nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2^nd ‘ 𝑓 ) ↦ ( ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ) ) ⟩ ) ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) = ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) , 𝑓 ∈ ( 𝐶 Func 𝐷 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( 𝑥 ∈ dom dom ( 2^nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2^nd ‘ 𝑓 ) ↦ ( ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ) ) ⟩ )
17	12 16	eqtri	⊢ ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) = ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) , 𝑓 ∈ ( 𝐶 Func 𝐷 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( 𝑥 ∈ dom dom ( 2^nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2^nd ‘ 𝑓 ) ↦ ( ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ) ) ⟩ )
18	17	fmpo	⊢ ( ∀ 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∀ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ⟨ ( ( 1^st ‘ 𝑔 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( 𝑥 ∈ dom dom ( 2^nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2^nd ‘ 𝑓 ) ↦ ( ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ) ) ⟩ ∈ ( 𝐶 Func 𝐸 ) ↔ ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) : ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ⟶ ( 𝐶 Func 𝐸 ) )
19	11 18	mpbi	⊢ ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) : ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ⟶ ( 𝐶 Func 𝐸 )