This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC CATEGORY THEORY Arrows (disjointified hom-sets) df-homa
Description: Definition of the hom-set extractor for arrows, which tags the morphisms
of the underlying hom-set with domain and codomain, which can then be
extracted using df-doma and df-coda . (Contributed by FL , 6-May-2007) (Revised by Mario Carneiro , 11-Jan-2017)
Ref
Expression
Assertion
df-homa ⊢ Homa 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) ) ↦ ( { 𝑥 } × ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ) ) )
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
choma ⊢ Homa
1
vc ⊢ 𝑐
2
ccat ⊢ Cat
3
vx ⊢ 𝑥
4
cbs ⊢ Base
5
1
cv ⊢ 𝑐
6
5 4
cfv ⊢ ( Base ‘ 𝑐 )
7
6 6
cxp ⊢ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) )
8
3
cv ⊢ 𝑥
9
8
csn ⊢ { 𝑥 }
10
chom ⊢ Hom
11
5 10
cfv ⊢ ( Hom ‘ 𝑐 )
12
8 11
cfv ⊢ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 )
13
9 12
cxp ⊢ ( { 𝑥 } × ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) )
14
3 7 13
cmpt ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) ) ↦ ( { 𝑥 } × ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ) )
15
1 2 14
cmpt ⊢ ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) ) ↦ ( { 𝑥 } × ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ) ) )
16
0 15
wceq ⊢ Homa 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) ) ↦ ( { 𝑥 } × ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ) ) )