Definition 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 ‘ 𝑐 ) ‘ 𝑥 ) ) ) )