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

Metamath Proof Explorer

Definition df-subc

Description: ( SubcatC ) is the set of all the subcategory specifications of the category C . Like df-subg , this is not actually a collection of categories (as in definition 4.1(a) of Adamek p. 48), but only sets which when given operations from the base category (using df-resc ) form a category. All the objects and all the morphisms of the subcategory belong to the supercategory. The identity of an object, the domain and the codomain of a morphism are the same in the subcategory and the supercategory. The composition of the subcategory is a restriction of the composition of the supercategory. (Contributed by FL, 17-Sep-2009) (Revised by Mario Carneiro, 4-Jan-2017)

Ref Expression
Assertion df-subc Subcat = ( 𝑐 ∈ Cat ↦ { ℎ ∣ ( ℎ ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom ℎ / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 ℎ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ℎ 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csubc ⊢ Subcat
1 vc ⊢ 𝑐
2 ccat ⊢ Cat
3 vh ⊢ ℎ
4 3 cv ⊢ ℎ
5 cssc ⊢ ⊆cat
6 chomf ⊢ Homf
7 1 cv ⊢ 𝑐
8 7 6 cfv ⊢ ( Homf ‘ 𝑐 )
9 4 8 5 wbr ⊢ ℎ ⊆cat ( Homf ‘ 𝑐 )
10 4 cdm ⊢ dom ℎ
11 10 cdm ⊢ dom dom ℎ
12 vs ⊢ 𝑠
13 vx ⊢ 𝑥
14 12 cv ⊢ 𝑠
15 ccid ⊢ Id
16 7 15 cfv ⊢ ( Id ‘ 𝑐 )
17 13 cv ⊢ 𝑥
18 17 16 cfv ⊢ ( ( Id ‘ 𝑐 ) ‘ 𝑥 )
19 17 17 4 co ⊢ ( 𝑥 ℎ 𝑥 )
20 18 19 wcel ⊢ ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 ℎ 𝑥 )
21 vy ⊢ 𝑦
22 vz ⊢ 𝑧
23 vf ⊢ 𝑓
24 21 cv ⊢ 𝑦
25 17 24 4 co ⊢ ( 𝑥 ℎ 𝑦 )
26 vg ⊢ 𝑔
27 22 cv ⊢ 𝑧
28 24 27 4 co ⊢ ( 𝑦 ℎ 𝑧 )
29 26 cv ⊢ 𝑔
30 17 24 cop ⊢ ⟨ 𝑥 , 𝑦 ⟩
31 cco ⊢ comp
32 7 31 cfv ⊢ ( comp ‘ 𝑐 )
33 30 27 32 co ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 )
34 23 cv ⊢ 𝑓
35 29 34 33 co ⊢ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 )
36 17 27 4 co ⊢ ( 𝑥 ℎ 𝑧 )
37 35 36 wcel ⊢ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 )
38 37 26 28 wral ⊢ ∀ 𝑔 ∈ ( 𝑦 ℎ 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 )
39 38 23 25 wral ⊢ ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ℎ 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 )
40 39 22 14 wral ⊢ ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ℎ 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 )
41 40 21 14 wral ⊢ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ℎ 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 )
42 20 41 wa ⊢ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 ℎ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ℎ 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 ) )
43 42 13 14 wral ⊢ ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 ℎ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ℎ 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 ) )
44 43 12 11 wsbc ⊢ [ dom dom ℎ / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 ℎ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ℎ 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 ) )
45 9 44 wa ⊢ ( ℎ ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom ℎ / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 ℎ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ℎ 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 ) ) )
46 45 3 cab ⊢ { ℎ ∣ ( ℎ ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom ℎ / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 ℎ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ℎ 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 ) ) ) }
47 1 2 46 cmpt ⊢ ( 𝑐 ∈ Cat ↦ { ℎ ∣ ( ℎ ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom ℎ / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 ℎ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ℎ 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 ) ) ) } )
48 0 47 wceq ⊢ Subcat = ( 𝑐 ∈ Cat ↦ { ℎ ∣ ( ℎ ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom ℎ / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 ℎ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ℎ 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 ) ) ) } )