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 ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 ) ) ) } )