Theorem arwval

Description: The set of arrows is the union of all the disjointified hom-sets. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	arwval.a	⊢ 𝐴 = ( Arrow ‘ 𝐶 )
	arwval.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
Assertion	arwval	⊢ 𝐴 = ∪ ran 𝐻

Proof

Step	Hyp	Ref	Expression
1		arwval.a	⊢ 𝐴 = ( Arrow ‘ 𝐶 )
2		arwval.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
3		fveq2	⊢ ( 𝑐 = 𝐶 → ( Homa ‘ 𝑐 ) = ( Homa ‘ 𝐶 ) )
4	3 2	eqtr4di	⊢ ( 𝑐 = 𝐶 → ( Homa ‘ 𝑐 ) = 𝐻 )
5	4	rneqd	⊢ ( 𝑐 = 𝐶 → ran ( Homa ‘ 𝑐 ) = ran 𝐻 )
6	5	unieqd	⊢ ( 𝑐 = 𝐶 → ∪ ran ( Homa ‘ 𝑐 ) = ∪ ran 𝐻 )
7		df-arw	⊢ Arrow = ( 𝑐 ∈ Cat ↦ ∪ ran ( Homa ‘ 𝑐 ) )
8	2	fvexi	⊢ 𝐻 ∈ V
9	8	rnex	⊢ ran 𝐻 ∈ V
10	9	uniex	⊢ ∪ ran 𝐻 ∈ V
11	6 7 10	fvmpt	⊢ ( 𝐶 ∈ Cat → ( Arrow ‘ 𝐶 ) = ∪ ran 𝐻 )
12	7	fvmptndm	⊢ ( ¬ 𝐶 ∈ Cat → ( Arrow ‘ 𝐶 ) = ∅ )
13		df-homa	⊢ Homa = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) ) ↦ ( { 𝑥 } × ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ) ) )
14	13	fvmptndm	⊢ ( ¬ 𝐶 ∈ Cat → ( Homa ‘ 𝐶 ) = ∅ )
15	2 14	syl5eq	⊢ ( ¬ 𝐶 ∈ Cat → 𝐻 = ∅ )
16	15	rneqd	⊢ ( ¬ 𝐶 ∈ Cat → ran 𝐻 = ran ∅ )
17		rn0	⊢ ran ∅ = ∅
18	16 17	eqtrdi	⊢ ( ¬ 𝐶 ∈ Cat → ran 𝐻 = ∅ )
19	18	unieqd	⊢ ( ¬ 𝐶 ∈ Cat → ∪ ran 𝐻 = ∪ ∅ )
20		uni0	⊢ ∪ ∅ = ∅
21	19 20	eqtrdi	⊢ ( ¬ 𝐶 ∈ Cat → ∪ ran 𝐻 = ∅ )
22	12 21	eqtr4d	⊢ ( ¬ 𝐶 ∈ Cat → ( Arrow ‘ 𝐶 ) = ∪ ran 𝐻 )
23	11 22	pm2.61i	⊢ ( Arrow ‘ 𝐶 ) = ∪ ran 𝐻
24	1 23	eqtri	⊢ 𝐴 = ∪ ran 𝐻