Definition df-resc

Description: Define the restriction of a category to a given set of arrows. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Assertion	df-resc	⊢ ↾cat = ( 𝑐 ∈ V , ℎ ∈ V ↦ ( ( 𝑐 ↾s dom dom ℎ ) sSet ⟨ ( Hom ‘ ndx ) , ℎ ⟩ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cresc	⊢ ↾cat
1		vc	⊢ 𝑐
2		cvv	⊢ V
3		vh	⊢ ℎ
4	1	cv	⊢ 𝑐
5		cress	⊢ ↾s
6	3	cv	⊢ ℎ
7	6	cdm	⊢ dom ℎ
8	7	cdm	⊢ dom dom ℎ
9	4 8 5	co	⊢ ( 𝑐 ↾s dom dom ℎ )
10		csts	⊢ sSet
11		chom	⊢ Hom
12		cnx	⊢ ndx
13	12 11	cfv	⊢ ( Hom ‘ ndx )
14	13 6	cop	⊢ ⟨ ( Hom ‘ ndx ) , ℎ ⟩
15	9 14 10	co	⊢ ( ( 𝑐 ↾s dom dom ℎ ) sSet ⟨ ( Hom ‘ ndx ) , ℎ ⟩ )
16	1 3 2 2 15	cmpo	⊢ ( 𝑐 ∈ V , ℎ ∈ V ↦ ( ( 𝑐 ↾s dom dom ℎ ) sSet ⟨ ( Hom ‘ ndx ) , ℎ ⟩ ) )
17	0 16	wceq	⊢ ↾cat = ( 𝑐 ∈ V , ℎ ∈ V ↦ ( ( 𝑐 ↾s dom dom ℎ ) sSet ⟨ ( Hom ‘ ndx ) , ℎ ⟩ ) )