This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid 
 |-  ( -. 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