Theorem arwval 15245

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

Hypotheses

Ref	Expression
arwval.a	|- A = (Nat ` C )
arwval.h	|- H = (Homa ` C )

Assertion

Ref	Expression
arwval	|- A = U. ran H

Proof of Theorem arwval

Dummy variables x c are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		arwval.a	. 2 |- A = (Nat ` C )
2		fveq2 5872	. . . . . . 7 |- ( c = C -> (Homa ` c ) = (Homa ` C ) )
3		arwval.h	. . . . . . 7 |- H = (Homa ` C )
4	2, 3	syl6eqr 2526	. . . . . 6 |- ( c = C -> (Homa ` c ) = H )
5	4	rneqd 5236	. . . . 5 |- ( c = C -> ran (Homa ` c ) = ran H )
6	5	unieqd 4261	. . . 4 |- ( c = C -> U. ran (Homa ` c ) = U. ran H )
7		df-arw 15229	. . . 4 |- Nat = ( c e. Cat |-> U. ran (Homa ` c ) )
8		fvex 5882	. . . . . . 7 |- (Homa ` C ) e. _V
9	3, 8	eqeltri 2551	. . . . . 6 |- H e. _V
10	9	rnex 6729	. . . . 5 |- ran H e. _V
11	10	uniex 6591	. . . 4 |- U. ran H e. _V
12	6, 7, 11	fvmpt 5957	. . 3 |- ( C e. Cat -> (Nat ` C ) = U. ran H )
13	7	dmmptss 5509	. . . . . . 7 |- dom Nat C_ Cat
14	13	sseli 3505	. . . . . 6 |- ( C e. dom Nat -> C e. Cat )
15	14	con3i 135	. . . . 5 |- ( -. C e. Cat -> -. C e. dom Nat )
16		ndmfv 5896	. . . . 5 |- ( -. C e. dom Nat -> (Nat ` C ) = (/) )
17	15, 16	syl 16	. . . 4 |- ( -. C e. Cat -> (Nat ` C ) = (/) )
18		df-homa 15228	. . . . . . . . . . . . 13 |- Homa = ( c e. Cat |-> ( x e. ( ( Base ` c ) X. ( Base ` c ) ) |-> ( { x } X. ( ( Hom ` c ) ` x ) ) ) )
19	18	dmmptss 5509	. . . . . . . . . . . 12 |- dom Homa C_ Cat
20	19	sseli 3505	. . . . . . . . . . 11 |- ( C e. dom Homa -> C e. Cat )
21	20	con3i 135	. . . . . . . . . 10 |- ( -. C e. Cat -> -. C e. dom Homa )
22		ndmfv 5896	. . . . . . . . . 10 |- ( -. C e. dom Homa -> (Homa ` C ) = (/) )
23	21, 22	syl 16	. . . . . . . . 9 |- ( -. C e. Cat -> (Homa ` C ) = (/) )
24	3, 23	syl5eq 2520	. . . . . . . 8 |- ( -. C e. Cat -> H = (/) )
25	24	rneqd 5236	. . . . . . 7 |- ( -. C e. Cat -> ran H = ran (/) )
26		rn0 5260	. . . . . . 7 |- ran (/) = (/)
27	25, 26	syl6eq 2524	. . . . . 6 |- ( -. C e. Cat -> ran H = (/) )
28	27	unieqd 4261	. . . . 5 |- ( -. C e. Cat -> U. ran H = U. (/) )
29		uni0 4278	. . . . 5 |- U. (/) = (/)
30	28, 29	syl6eq 2524	. . . 4 |- ( -. C e. Cat -> U. ran H = (/) )
31	17, 30	eqtr4d 2511	. . 3 |- ( -. C e. Cat -> (Nat ` C ) = U. ran H )
32	12, 31	pm2.61i 164	. 2 |- (Nat ` C ) = U. ran H
33	1, 32	eqtri 2496	1 |- A = U. ran H

Syntax hints:   -. wn 3   = wceq 1379   e. wcel 1767   _Vcvv 3118   (/)c0 3790   {csn 4033   U.cuni 4251   |-> cmpt 4511   X. cxp 5003   dom cdm 5005   ran crn 5006   ` cfv 5594   Basecbs 14507   Hom chom 14583   Catccat 14936  Natcarw 15224  Hom_achoma 15225

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-sbc 3337  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-br 4454  df-opab 4512  df-mpt 4513  df-id 4801  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fv 5602  df-homa 15228  df-arw 15229

This theorem is referenced by:  arwhoma  15247  homarw  15248