df-cofu

Description: Define the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017)

		Ref	Expression
	Assertion	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 ‘ 𝑓 ) 𝑦 ) ) ) ⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccofu	⊢ ∘_func
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		vf	⊢ 𝑓
4		c1st	⊢ 1^st
5	1	cv	⊢ 𝑔
6	5 4	cfv	⊢ ( 1^st ‘ 𝑔 )
7	3	cv	⊢ 𝑓
8	7 4	cfv	⊢ ( 1^st ‘ 𝑓 )
9	6 8	ccom	⊢ ( ( 1^st ‘ 𝑔 ) ∘ ( 1^st ‘ 𝑓 ) )
10		vx	⊢ 𝑥
11		c2nd	⊢ 2^nd
12	7 11	cfv	⊢ ( 2^nd ‘ 𝑓 )
13	12	cdm	⊢ dom ( 2^nd ‘ 𝑓 )
14	13	cdm	⊢ dom dom ( 2^nd ‘ 𝑓 )
15		vy	⊢ 𝑦
16	10	cv	⊢ 𝑥
17	16 8	cfv	⊢ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 )
18	5 11	cfv	⊢ ( 2^nd ‘ 𝑔 )
19	15	cv	⊢ 𝑦
20	19 8	cfv	⊢ ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 )
21	17 20 18	co	⊢ ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) )
22	16 19 12	co	⊢ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 )
23	21 22	ccom	⊢ ( ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) )
24	10 15 14 14 23	cmpo	⊢ ( 𝑥 ∈ dom dom ( 2^nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2^nd ‘ 𝑓 ) ↦ ( ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ) )
25	9 24	cop	⊢ ⟨ ( ( 1^st ‘ 𝑔 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( 𝑥 ∈ dom dom ( 2^nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2^nd ‘ 𝑓 ) ↦ ( ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ) ) ⟩
26	1 3 2 2 25	cmpo	⊢ ( 𝑔 ∈ V , 𝑓 ∈ V ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( 𝑥 ∈ dom dom ( 2^nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2^nd ‘ 𝑓 ) ↦ ( ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ) ) ⟩ )
27	0 26	wceq	⊢ ∘_func = ( 𝑔 ∈ V , 𝑓 ∈ V ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( 𝑥 ∈ dom dom ( 2^nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2^nd ‘ 𝑓 ) ↦ ( ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ) ) ⟩ )

Metamath Proof Explorer

Definition df-cofu

Detailed syntax breakdown