Theorem arwval 16016

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 5879	. . . . . . 7 |- ( c = C -> (Homa ` c ) = (Homa ` C ) )
3		arwval.h	. . . . . . 7 |- H = (Homa ` C )
4	2, 3	syl6eqr 2523	. . . . . 6 |- ( c = C -> (Homa ` c ) = H )
5	4	rneqd 5068	. . . . 5 |- ( c = C -> ran (Homa ` c ) = ran H )
6	5	unieqd 4200	. . . 4 |- ( c = C -> U. ran (Homa ` c ) = U. ran H )
7		df-arw 16000	. . . 4 |- Nat = ( c e. Cat |-> U. ran (Homa ` c ) )
8		fvex 5889	. . . . . . 7 |- (Homa ` C ) e. _V
9	3, 8	eqeltri 2545	. . . . . 6 |- H e. _V
10	9	rnex 6746	. . . . 5 |- ran H e. _V
11	10	uniex 6606	. . . 4 |- U. ran H e. _V
12	6, 7, 11	fvmpt 5963	. . 3 |- ( C e. Cat -> (Nat ` C ) = U. ran H )
13	7	dmmptss 5338	. . . . . . 7 |- dom Nat C_ Cat
14	13	sseli 3414	. . . . . 6 |- ( C e. dom Nat -> C e. Cat )
15	14	con3i 142	. . . . 5 |- ( -. C e. Cat -> -. C e. dom Nat )
16		ndmfv 5903	. . . . 5 |- ( -. C e. dom Nat -> (Nat ` C ) = (/) )
17	15, 16	syl 17	. . . 4 |- ( -. C e. Cat -> (Nat ` C ) = (/) )
18		df-homa 15999	. . . . . . . . . . . . 13 |- Homa = ( c e. Cat |-> ( x e. ( ( Base ` c ) X. ( Base ` c ) ) |-> ( { x } X. ( ( Hom ` c ) ` x ) ) ) )
19	18	dmmptss 5338	. . . . . . . . . . . 12 |- dom Homa C_ Cat
20	19	sseli 3414	. . . . . . . . . . 11 |- ( C e. dom Homa -> C e. Cat )
21	20	con3i 142	. . . . . . . . . 10 |- ( -. C e. Cat -> -. C e. dom Homa )
22		ndmfv 5903	. . . . . . . . . 10 |- ( -. C e. dom Homa -> (Homa ` C ) = (/) )
23	21, 22	syl 17	. . . . . . . . 9 |- ( -. C e. Cat -> (Homa ` C ) = (/) )
24	3, 23	syl5eq 2517	. . . . . . . 8 |- ( -. C e. Cat -> H = (/) )
25	24	rneqd 5068	. . . . . . 7 |- ( -. C e. Cat -> ran H = ran (/) )
26		rn0 5092	. . . . . . 7 |- ran (/) = (/)
27	25, 26	syl6eq 2521	. . . . . 6 |- ( -. C e. Cat -> ran H = (/) )
28	27	unieqd 4200	. . . . 5 |- ( -. C e. Cat -> U. ran H = U. (/) )
29		uni0 4217	. . . . 5 |- U. (/) = (/)
30	28, 29	syl6eq 2521	. . . 4 |- ( -. C e. Cat -> U. ran H = (/) )
31	17, 30	eqtr4d 2508	. . 3 |- ( -. C e. Cat -> (Nat ` C ) = U. ran H )
32	12, 31	pm2.61i 169	. 2 |- (Nat ` C ) = U. ran H
33	1, 32	eqtri 2493	1 |- A = U. ran H

Syntax hints:   -. wn 3   = wceq 1452   e. wcel 1904   _Vcvv 3031   (/)c0 3722   {csn 3959   U.cuni 4190   |-> cmpt 4454   X. cxp 4837   dom cdm 4839   ran crn 4840   ` cfv 5589   Basecbs 15199   Hom chom 15279   Catccat 15648  Natcarw 15995  Hom_achoma 15996

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-iota 5553  df-fun 5591  df-fv 5597  df-homa 15999  df-arw 16000

This theorem is referenced by:  arwhoma  16018  homarw  16019