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

Metamath Proof Explorer

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 ) , ℎ ⟩ ) )