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 ⊢ 𝐴 = ( Arrow ‘ 𝐶 )
arwval.h ⊢ 𝐻 = ( Homa ‘ 𝐶 )
Assertion arwval 𝐴 = ∪ ran 𝐻

Proof

Step Hyp Ref Expression
1 arwval.a ⊢ 𝐴 = ( Arrow ‘ 𝐶 )
2 arwval.h ⊢ 𝐻 = ( Homa ‘ 𝐶 )
3 fveq2 ⊢ ( 𝑐 = 𝐶 → ( Homa ‘ 𝑐 ) = ( Homa ‘ 𝐶 ) )
4 3 2 eqtr4di ⊢ ( 𝑐 = 𝐶 → ( Homa ‘ 𝑐 ) = 𝐻 )
5 4 rneqd ⊢ ( 𝑐 = 𝐶 → ran ( Homa ‘ 𝑐 ) = ran 𝐻 )
6 5 unieqd ⊢ ( 𝑐 = 𝐶 → ∪ ran ( Homa ‘ 𝑐 ) = ∪ ran 𝐻 )
7 df-arw ⊢ Arrow = ( 𝑐 ∈ Cat ↦ ∪ ran ( Homa ‘ 𝑐 ) )
8 2 fvexi ⊢ 𝐻 ∈ V
9 8 rnex ⊢ ran 𝐻 ∈ V
10 9 uniex ⊢ ∪ ran 𝐻 ∈ V
11 6 7 10 fvmpt ⊢ ( 𝐶 ∈ Cat → ( Arrow ‘ 𝐶 ) = ∪ ran 𝐻 )
12 7 fvmptndm ⊢ ( ¬ 𝐶 ∈ Cat → ( Arrow ‘ 𝐶 ) = ∅ )
13 df-homa ⊢ Homa = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) ) ↦ ( { 𝑥 } × ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ) ) )
14 13 fvmptndm ⊢ ( ¬ 𝐶 ∈ Cat → ( Homa ‘ 𝐶 ) = ∅ )
15 2 14 eqtrid ⊢ ( ¬ 𝐶 ∈ Cat → 𝐻 = ∅ )
16 15 rneqd ⊢ ( ¬ 𝐶 ∈ Cat → ran 𝐻 = ran ∅ )
17 rn0 ⊢ ran ∅ = ∅
18 16 17 eqtrdi ⊢ ( ¬ 𝐶 ∈ Cat → ran 𝐻 = ∅ )
19 18 unieqd ⊢ ( ¬ 𝐶 ∈ Cat → ∪ ran 𝐻 = ∪ ∅ )
20 uni0 ⊢ ∪ ∅ = ∅
21 19 20 eqtrdi ⊢ ( ¬ 𝐶 ∈ Cat → ∪ ran 𝐻 = ∅ )
22 12 21 eqtr4d ⊢ ( ¬ 𝐶 ∈ Cat → ( Arrow ‘ 𝐶 ) = ∪ ran 𝐻 )
23 11 22 pm2.61i ⊢ ( Arrow ‘ 𝐶 ) = ∪ ran 𝐻
24 1 23 eqtri ⊢ 𝐴 = ∪ ran 𝐻