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	|- A = ( Arrow ` C )
	arwval.h	|- H = ( HomA ` C )
Assertion	arwval	|- A = U. ran H

Proof

Step	Hyp	Ref	Expression
1		arwval.a	|- A = ( Arrow ` C )
2		arwval.h	|- H = ( HomA ` C )
3		fveq2	|- ( c = C -> ( HomA ` c ) = ( HomA ` C ) )
4	3 2	eqtr4di	|- ( c = C -> ( HomA ` c ) = H )
5	4	rneqd	|- ( c = C -> ran ( HomA ` c ) = ran H )
6	5	unieqd	|- ( c = C -> U. ran ( HomA ` c ) = U. ran H )
7		df-arw	|- Arrow = ( c e. Cat |-> U. ran ( HomA ` c ) )
8	2	fvexi	|- H e. _V
9	8	rnex	|- ran H e. _V
10	9	uniex	|- U. ran H e. _V
11	6 7 10	fvmpt	|- ( C e. Cat -> ( Arrow ` C ) = U. ran H )
12	7	fvmptndm	|- ( -. C e. Cat -> ( Arrow ` C ) = (/) )
13		df-homa	|- HomA = ( c e. Cat |-> ( x e. ( ( Base ` c ) X. ( Base ` c ) ) |-> ( { x } X. ( ( Hom ` c ) ` x ) ) ) )
14	13	fvmptndm	|- ( -. C e. Cat -> ( HomA ` C ) = (/) )
15	2 14	syl5eq	|- ( -. C e. Cat -> H = (/) )
16	15	rneqd	|- ( -. C e. Cat -> ran H = ran (/) )
17		rn0	|- ran (/) = (/)
18	16 17	eqtrdi	|- ( -. C e. Cat -> ran H = (/) )
19	18	unieqd	|- ( -. C e. Cat -> U. ran H = U. (/) )
20		uni0	|- U. (/) = (/)
21	19 20	eqtrdi	|- ( -. C e. Cat -> U. ran H = (/) )
22	12 21	eqtr4d	|- ( -. C e. Cat -> ( Arrow ` C ) = U. ran H )
23	11 22	pm2.61i	|- ( Arrow ` C ) = U. ran H
24	1 23	eqtri	|- A = U. ran H