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 = Hom a ⁡ C
Assertion arwval ⊢ A = ⋃ ran ⁡ H

Proof

Step Hyp Ref Expression
1 arwval.a ⊢ A = Arrow ⁡ C
2 arwval.h ⊢ H = Hom a ⁡ C
3 fveq2 ⊢ c = C → Hom a ⁡ c = Hom a ⁡ C
4 3 2 eqtr4di ⊢ c = C → Hom a ⁡ c = H
5 4 rneqd ⊢ c = C → ran ⁡ Hom a ⁡ c = ran ⁡ H
6 5 unieqd ⊢ c = C → ⋃ ran ⁡ Hom a ⁡ c = ⋃ ran ⁡ H
7 df-arw ⊢ Arrow = c ∈ Cat ⟼ ⋃ ran ⁡ Hom a ⁡ 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 ⊢ Hom a = c ∈ Cat ⟼ x ∈ Base c × Base c ⟼ x × Hom ⁡ c ⁡ x
14 13 fvmptndm ⊢ ¬ C ∈ Cat → Hom a ⁡ 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