This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem catcco

Description: Composition in the category of categories. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses catcbas.c ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
catcbas.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
catcbas.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
catcco.o ⊢ · = ( comp ‘ 𝐶 )
catcco.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
catcco.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
catcco.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
catcco.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 Func 𝑌 ) )
catcco.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 Func 𝑍 ) )
Assertion catcco ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 𝐺 ∘func 𝐹 ) )

Proof

Step Hyp Ref Expression
1 catcbas.c ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2 catcbas.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 catcbas.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
4 catcco.o ⊢ · = ( comp ‘ 𝐶 )
5 catcco.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 catcco.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7 catcco.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
8 catcco.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 Func 𝑌 ) )
9 catcco.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 Func 𝑍 ) )
10 1 2 3 4 catccofval ⊢ ( 𝜑 → · = ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ) )
11 simprl ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ )
12 11 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 2nd ‘ 𝑣 ) = ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
13 op2ndg ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
14 5 6 13 syl2anc ⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
15 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
16 12 15 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 2nd ‘ 𝑣 ) = 𝑌 )
17 simprr ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → 𝑧 = 𝑍 )
18 16 17 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) = ( 𝑌 Func 𝑍 ) )
19 11 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( Func ‘ 𝑣 ) = ( Func ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
20 df-ov ⊢ ( 𝑋 Func 𝑌 ) = ( Func ‘ ⟨ 𝑋 , 𝑌 ⟩ )
21 19 20 eqtr4di ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( Func ‘ 𝑣 ) = ( 𝑋 Func 𝑌 ) )
22 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 𝑔 ∘func 𝑓 ) = ( 𝑔 ∘func 𝑓 ) )
23 18 21 22 mpoeq123dv ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) = ( 𝑔 ∈ ( 𝑌 Func 𝑍 ) , 𝑓 ∈ ( 𝑋 Func 𝑌 ) ↦ ( 𝑔 ∘func 𝑓 ) ) )
24 5 6 opelxpd ⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) )
25 ovex ⊢ ( 𝑌 Func 𝑍 ) ∈ V
26 ovex ⊢ ( 𝑋 Func 𝑌 ) ∈ V
27 25 26 mpoex ⊢ ( 𝑔 ∈ ( 𝑌 Func 𝑍 ) , 𝑓 ∈ ( 𝑋 Func 𝑌 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ∈ V
28 27 a1i ⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝑌 Func 𝑍 ) , 𝑓 ∈ ( 𝑋 Func 𝑌 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ∈ V )
29 10 23 24 7 28 ovmpod ⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) = ( 𝑔 ∈ ( 𝑌 Func 𝑍 ) , 𝑓 ∈ ( 𝑋 Func 𝑌 ) ↦ ( 𝑔 ∘func 𝑓 ) ) )
30 oveq12 ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) → ( 𝑔 ∘func 𝑓 ) = ( 𝐺 ∘func 𝐹 ) )
31 30 adantl ⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 𝑔 ∘func 𝑓 ) = ( 𝐺 ∘func 𝐹 ) )
32 ovexd ⊢ ( 𝜑 → ( 𝐺 ∘func 𝐹 ) ∈ V )
33 29 31 9 8 32 ovmpod ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 𝐺 ∘func 𝐹 ) )