Metamath Proof Explorer


Definition df-cofu

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

Ref Expression
Assertion df-cofu func = ( 𝑔 ∈ V , 𝑓 ∈ V ↦ ⟨ ( ( 1st𝑔 ) ∘ ( 1st𝑓 ) ) , ( 𝑥 ∈ dom dom ( 2nd𝑓 ) , 𝑦 ∈ dom dom ( 2nd𝑓 ) ↦ ( ( ( ( 1st𝑓 ) ‘ 𝑥 ) ( 2nd𝑔 ) ( ( 1st𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ) ) ⟩ )

Detailed syntax breakdown

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