Step | Hyp | Ref
| Expression |
1 | | arwval.a |
. 2
⊢ 𝐴 = (Arrow‘𝐶) |
2 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → (Homa‘𝑐) =
(Homa‘𝐶)) |
3 | | arwval.h |
. . . . . . 7
⊢ 𝐻 =
(Homa‘𝐶) |
4 | 2, 3 | syl6eqr 2662 |
. . . . . 6
⊢ (𝑐 = 𝐶 → (Homa‘𝑐) = 𝐻) |
5 | 4 | rneqd 5274 |
. . . . 5
⊢ (𝑐 = 𝐶 → ran
(Homa‘𝑐) = ran 𝐻) |
6 | 5 | unieqd 4382 |
. . . 4
⊢ (𝑐 = 𝐶 → ∪ ran
(Homa‘𝑐) = ∪ ran 𝐻) |
7 | | df-arw 16500 |
. . . 4
⊢ Arrow =
(𝑐 ∈ Cat ↦ ∪ ran (Homa‘𝑐)) |
8 | | fvex 6113 |
. . . . . . 7
⊢
(Homa‘𝐶) ∈ V |
9 | 3, 8 | eqeltri 2684 |
. . . . . 6
⊢ 𝐻 ∈ V |
10 | 9 | rnex 6992 |
. . . . 5
⊢ ran 𝐻 ∈ V |
11 | 10 | uniex 6851 |
. . . 4
⊢ ∪ ran 𝐻 ∈ V |
12 | 6, 7, 11 | fvmpt 6191 |
. . 3
⊢ (𝐶 ∈ Cat →
(Arrow‘𝐶) = ∪ ran 𝐻) |
13 | 7 | dmmptss 5548 |
. . . . . . 7
⊢ dom Arrow
⊆ Cat |
14 | 13 | sseli 3564 |
. . . . . 6
⊢ (𝐶 ∈ dom Arrow → 𝐶 ∈ Cat) |
15 | 14 | con3i 149 |
. . . . 5
⊢ (¬
𝐶 ∈ Cat → ¬
𝐶 ∈ dom
Arrow) |
16 | | ndmfv 6128 |
. . . . 5
⊢ (¬
𝐶 ∈ dom Arrow →
(Arrow‘𝐶) =
∅) |
17 | 15, 16 | syl 17 |
. . . 4
⊢ (¬
𝐶 ∈ Cat →
(Arrow‘𝐶) =
∅) |
18 | | df-homa 16499 |
. . . . . . . . . . . . 13
⊢
Homa = (𝑐 ∈ Cat ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)) ↦ ({𝑥} × ((Hom ‘𝑐)‘𝑥)))) |
19 | 18 | dmmptss 5548 |
. . . . . . . . . . . 12
⊢ dom
Homa ⊆ Cat |
20 | 19 | sseli 3564 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ dom
Homa → 𝐶 ∈ Cat) |
21 | 20 | con3i 149 |
. . . . . . . . . 10
⊢ (¬
𝐶 ∈ Cat → ¬
𝐶 ∈ dom
Homa) |
22 | | ndmfv 6128 |
. . . . . . . . . 10
⊢ (¬
𝐶 ∈ dom
Homa → (Homa‘𝐶) = ∅) |
23 | 21, 22 | syl 17 |
. . . . . . . . 9
⊢ (¬
𝐶 ∈ Cat →
(Homa‘𝐶) = ∅) |
24 | 3, 23 | syl5eq 2656 |
. . . . . . . 8
⊢ (¬
𝐶 ∈ Cat → 𝐻 = ∅) |
25 | 24 | rneqd 5274 |
. . . . . . 7
⊢ (¬
𝐶 ∈ Cat → ran
𝐻 = ran
∅) |
26 | | rn0 5298 |
. . . . . . 7
⊢ ran
∅ = ∅ |
27 | 25, 26 | syl6eq 2660 |
. . . . . 6
⊢ (¬
𝐶 ∈ Cat → ran
𝐻 =
∅) |
28 | 27 | unieqd 4382 |
. . . . 5
⊢ (¬
𝐶 ∈ Cat → ∪ ran 𝐻 = ∪
∅) |
29 | | uni0 4401 |
. . . . 5
⊢ ∪ ∅ = ∅ |
30 | 28, 29 | syl6eq 2660 |
. . . 4
⊢ (¬
𝐶 ∈ Cat → ∪ ran 𝐻 = ∅) |
31 | 17, 30 | eqtr4d 2647 |
. . 3
⊢ (¬
𝐶 ∈ Cat →
(Arrow‘𝐶) = ∪ ran 𝐻) |
32 | 12, 31 | pm2.61i 175 |
. 2
⊢
(Arrow‘𝐶) =
∪ ran 𝐻 |
33 | 1, 32 | eqtri 2632 |
1
⊢ 𝐴 = ∪
ran 𝐻 |