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

Metamath Proof Explorer

Theorem setcco

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

Ref Expression
Hypotheses setcbas.c ⊢ 𝐶 = ( SetCat ‘ 𝑈 )
setcbas.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
setcco.o ⊢ · = ( comp ‘ 𝐶 )
setcco.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
setcco.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
setcco.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
setcco.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑌 )
setcco.g ⊢ ( 𝜑 → 𝐺 : 𝑌 ⟶ 𝑍 )
Assertion setcco ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 𝐺 ∘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 setcbas.c ⊢ 𝐶 = ( SetCat ‘ 𝑈 )
2 setcbas.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3 setcco.o ⊢ · = ( comp ‘ 𝐶 )
4 setcco.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
5 setcco.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
6 setcco.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
7 setcco.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑌 )
8 setcco.g ⊢ ( 𝜑 → 𝐺 : 𝑌 ⟶ 𝑍 )
9 1 2 3 setccofval ⊢ ( 𝜑 → · = ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) )
10 simprr ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → 𝑧 = 𝑍 )
11 simprl ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ )
12 11 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 2nd ‘ 𝑣 ) = ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
13 op2ndg ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
14 4 5 13 syl2anc ⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
15 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
16 12 15 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 2nd ‘ 𝑣 ) = 𝑌 )
17 10 16 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) = ( 𝑍 ↑m 𝑌 ) )
18 11 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 1st ‘ 𝑣 ) = ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
19 op1stg ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
20 4 5 19 syl2anc ⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
21 20 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
22 18 21 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 1st ‘ 𝑣 ) = 𝑋 )
23 16 22 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) = ( 𝑌 ↑m 𝑋 ) )
24 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 𝑔 ∘ 𝑓 ) = ( 𝑔 ∘ 𝑓 ) )
25 17 23 24 mpoeq123dv ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) = ( 𝑔 ∈ ( 𝑍 ↑m 𝑌 ) , 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ↦ ( 𝑔 ∘ 𝑓 ) ) )
26 4 5 opelxpd ⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝑈 × 𝑈 ) )
27 ovex ⊢ ( 𝑍 ↑m 𝑌 ) ∈ V
28 ovex ⊢ ( 𝑌 ↑m 𝑋 ) ∈ V
29 27 28 mpoex ⊢ ( 𝑔 ∈ ( 𝑍 ↑m 𝑌 ) , 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ↦ ( 𝑔 ∘ 𝑓 ) ) ∈ V
30 29 a1i ⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝑍 ↑m 𝑌 ) , 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ↦ ( 𝑔 ∘ 𝑓 ) ) ∈ V )
31 9 25 26 6 30 ovmpod ⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) = ( 𝑔 ∈ ( 𝑍 ↑m 𝑌 ) , 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ↦ ( 𝑔 ∘ 𝑓 ) ) )
32 simprl ⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → 𝑔 = 𝐺 )
33 simprr ⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → 𝑓 = 𝐹 )
34 32 33 coeq12d ⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 𝑔 ∘ 𝑓 ) = ( 𝐺 ∘ 𝐹 ) )
35 6 5 elmapd ⊢ ( 𝜑 → ( 𝐺 ∈ ( 𝑍 ↑m 𝑌 ) ↔ 𝐺 : 𝑌 ⟶ 𝑍 ) )
36 8 35 mpbird ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑍 ↑m 𝑌 ) )
37 5 4 elmapd ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑌 ↑m 𝑋 ) ↔ 𝐹 : 𝑋 ⟶ 𝑌 ) )
38 7 37 mpbird ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑌 ↑m 𝑋 ) )
39 coexg ⊢ ( ( 𝐺 ∈ ( 𝑍 ↑m 𝑌 ) ∧ 𝐹 ∈ ( 𝑌 ↑m 𝑋 ) ) → ( 𝐺 ∘ 𝐹 ) ∈ V )
40 36 38 39 syl2anc ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) ∈ V )
41 31 34 36 38 40 ovmpod ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 𝐺 ∘ 𝐹 ) )