Metamath Proof Explorer

Theorem subccocl

Description: A subcategory is closed under composition. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses subcidcl.j ⊢ ( 𝜑 → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
subcidcl.2 ⊢ ( 𝜑 → 𝐽 Fn ( 𝑆 × 𝑆 ) )
subcidcl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
subccocl.o ⊢ · = ( comp ‘ 𝐶 )
subccocl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
subccocl.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑆 )
subccocl.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐽 𝑌 ) )
subccocl.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐽 𝑍 ) )
Assertion subccocl ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐽 𝑍 ) )

Proof

Step Hyp Ref Expression
1 subcidcl.j ⊢ ( 𝜑 → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
2 subcidcl.2 ⊢ ( 𝜑 → 𝐽 Fn ( 𝑆 × 𝑆 ) )
3 subcidcl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
4 subccocl.o ⊢ · = ( comp ‘ 𝐶 )
5 subccocl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
6 subccocl.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑆 )
7 subccocl.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐽 𝑌 ) )
8 subccocl.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐽 𝑍 ) )
9 eqid ⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
10 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
11 subcrcl ⊢ ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → 𝐶 ∈ Cat )
12 1 11 syl ⊢ ( 𝜑 → 𝐶 ∈ Cat )
13 9 10 4 12 2 issubc2 ⊢ ( 𝜑 → ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) ↔ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ∀ 𝑥 ∈ 𝑆 ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) )
14 1 13 mpbid ⊢ ( 𝜑 → ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ∀ 𝑥 ∈ 𝑆 ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) )
15 14 simprd ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) )
16 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑌 ∈ 𝑆 )
17 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → 𝑍 ∈ 𝑆 )
18 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → 𝐹 ∈ ( 𝑋 𝐽 𝑌 ) )
19 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → 𝑥 = 𝑋 )
20 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → 𝑦 = 𝑌 )
21 19 20 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → ( 𝑥 𝐽 𝑦 ) = ( 𝑋 𝐽 𝑌 ) )
22 18 21 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → 𝐹 ∈ ( 𝑥 𝐽 𝑦 ) )
23 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) → 𝐺 ∈ ( 𝑌 𝐽 𝑍 ) )
24 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) → 𝑦 = 𝑌 )
25 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) → 𝑧 = 𝑍 )
26 24 25 oveq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) → ( 𝑦 𝐽 𝑧 ) = ( 𝑌 𝐽 𝑍 ) )
27 23 26 eleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) → 𝐺 ∈ ( 𝑦 𝐽 𝑧 ) )
28 simp-5r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → 𝑥 = 𝑋 )
29 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → 𝑦 = 𝑌 )
30 28 29 opeq12d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑋 , 𝑌 ⟩ )
31 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → 𝑧 = 𝑍 )
32 30 31 oveq12d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) = ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) )
33 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
34 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → 𝑓 = 𝐹 )
35 32 33 34 oveq123d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) )
36 28 31 oveq12d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑥 𝐽 𝑧 ) = ( 𝑋 𝐽 𝑍 ) )
37 35 36 eleq12d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ↔ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐽 𝑍 ) ) )
38 27 37 rspcdv ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) ∧ 𝑓 = 𝐹 ) → ( ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐽 𝑍 ) ) )
39 22 38 rspcimdv ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → ( ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐽 𝑍 ) ) )
40 17 39 rspcimdv ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → ( ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐽 𝑍 ) ) )
41 16 40 rspcimdv ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐽 𝑍 ) ) )
42 41 adantld ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐽 𝑍 ) ) )
43 3 42 rspcimdv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑆 ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐽 𝑍 ) ) )
44 15 43 mpd ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐽 𝑍 ) )