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=⋃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→⋃ran⁡Homa⁡c=⋃ran⁡H
7 df-arw ⊢Arrow=c∈Cat⟼⋃ran⁡Homa⁡c
8 2 fvexi ⊢H∈V
9 8 rnex ⊢ran⁡H∈V
10 9 uniex ⊢⋃ran⁡H∈V
11 6 7 10 fvmpt ⊢C∈Cat→Arrow⁡C=⋃ran⁡H
12 7 fvmptndm ⊢¬C∈Cat→Arrow⁡C=∅
13 df-homa ⊢Homa=c∈Cat⟼x∈Basec×Basec⟼x×Hom⁡c⁡x
14 13 fvmptndm ⊢¬C∈Cat→Homa⁡C=∅
15 2 14 eqtrid ⊢¬C∈Cat→H=∅
16 15 rneqd ⊢¬C∈Cat→ran⁡H=ran⁡∅
17 rn0 ⊢ran⁡∅=∅
18 16 17 eqtrdi ⊢¬C∈Cat→ran⁡H=∅
19 18 unieqd ⊢¬C∈Cat→⋃ran⁡H=⋃∅
20 uni0 ⊢⋃∅=∅
21 19 20 eqtrdi ⊢¬C∈Cat→⋃ran⁡H=∅
22 12 21 eqtr4d ⊢¬C∈Cat→Arrow⁡C=⋃ran⁡H
23 11 22 pm2.61i ⊢Arrow⁡C=⋃ran⁡H
24 1 23 eqtri ⊢A=⋃ran⁡H