Step | Hyp | Ref
| Expression |
1 | | edgval 27172 |
. . . 4
⊢
(Edg‘𝑆) = ran
(iEdg‘𝑆) |
2 | 1 | eleq2i 2831 |
. . 3
⊢ (𝑒 ∈ (Edg‘𝑆) ↔ 𝑒 ∈ ran (iEdg‘𝑆)) |
3 | | uhgrspan.g |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ UHGraph) |
4 | | uhgrspan.e |
. . . . . . . 8
⊢ 𝐸 = (iEdg‘𝐺) |
5 | 4 | uhgrfun 27189 |
. . . . . . 7
⊢ (𝐺 ∈ UHGraph → Fun 𝐸) |
6 | | funres 6443 |
. . . . . . 7
⊢ (Fun
𝐸 → Fun (𝐸 ↾ 𝐴)) |
7 | 3, 5, 6 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → Fun (𝐸 ↾ 𝐴)) |
8 | | uhgrspan.r |
. . . . . . 7
⊢ (𝜑 → (iEdg‘𝑆) = (𝐸 ↾ 𝐴)) |
9 | 8 | funeqd 6423 |
. . . . . 6
⊢ (𝜑 → (Fun (iEdg‘𝑆) ↔ Fun (𝐸 ↾ 𝐴))) |
10 | 7, 9 | mpbird 260 |
. . . . 5
⊢ (𝜑 → Fun (iEdg‘𝑆)) |
11 | | elrnrexdmb 6931 |
. . . . 5
⊢ (Fun
(iEdg‘𝑆) →
(𝑒 ∈ ran
(iEdg‘𝑆) ↔
∃𝑖 ∈ dom
(iEdg‘𝑆)𝑒 = ((iEdg‘𝑆)‘𝑖))) |
12 | 10, 11 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑒 ∈ ran (iEdg‘𝑆) ↔ ∃𝑖 ∈ dom (iEdg‘𝑆)𝑒 = ((iEdg‘𝑆)‘𝑖))) |
13 | 8 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → (iEdg‘𝑆) = (𝐸 ↾ 𝐴)) |
14 | 13 | fveq1d 6741 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑖) = ((𝐸 ↾ 𝐴)‘𝑖)) |
15 | 8 | dmeqd 5792 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom (iEdg‘𝑆) = dom (𝐸 ↾ 𝐴)) |
16 | | dmres 5891 |
. . . . . . . . . . . . 13
⊢ dom
(𝐸 ↾ 𝐴) = (𝐴 ∩ dom 𝐸) |
17 | 15, 16 | eqtrdi 2796 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom (iEdg‘𝑆) = (𝐴 ∩ dom 𝐸)) |
18 | 17 | eleq2d 2825 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑖 ∈ dom (iEdg‘𝑆) ↔ 𝑖 ∈ (𝐴 ∩ dom 𝐸))) |
19 | | elinel1 4126 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (𝐴 ∩ dom 𝐸) → 𝑖 ∈ 𝐴) |
20 | 18, 19 | syl6bi 256 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑖 ∈ dom (iEdg‘𝑆) → 𝑖 ∈ 𝐴)) |
21 | 20 | imp 410 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → 𝑖 ∈ 𝐴) |
22 | 21 | fvresd 6759 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → ((𝐸 ↾ 𝐴)‘𝑖) = (𝐸‘𝑖)) |
23 | 14, 22 | eqtrd 2779 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑖) = (𝐸‘𝑖)) |
24 | | elinel2 4127 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (𝐴 ∩ dom 𝐸) → 𝑖 ∈ dom 𝐸) |
25 | 18, 24 | syl6bi 256 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑖 ∈ dom (iEdg‘𝑆) → 𝑖 ∈ dom 𝐸)) |
26 | 25 | imp 410 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → 𝑖 ∈ dom 𝐸) |
27 | | uhgrspan.v |
. . . . . . . . . 10
⊢ 𝑉 = (Vtx‘𝐺) |
28 | 27, 4 | uhgrss 27187 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UHGraph ∧ 𝑖 ∈ dom 𝐸) → (𝐸‘𝑖) ⊆ 𝑉) |
29 | 3, 26, 28 | syl2an2r 685 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → (𝐸‘𝑖) ⊆ 𝑉) |
30 | | uhgrspan.q |
. . . . . . . . . . . 12
⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) |
31 | 30 | pweqd 4549 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝒫 (Vtx‘𝑆) = 𝒫 𝑉) |
32 | 31 | eleq2d 2825 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐸‘𝑖) ∈ 𝒫 (Vtx‘𝑆) ↔ (𝐸‘𝑖) ∈ 𝒫 𝑉)) |
33 | 32 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → ((𝐸‘𝑖) ∈ 𝒫 (Vtx‘𝑆) ↔ (𝐸‘𝑖) ∈ 𝒫 𝑉)) |
34 | | fvex 6752 |
. . . . . . . . . 10
⊢ (𝐸‘𝑖) ∈ V |
35 | 34 | elpw 4534 |
. . . . . . . . 9
⊢ ((𝐸‘𝑖) ∈ 𝒫 𝑉 ↔ (𝐸‘𝑖) ⊆ 𝑉) |
36 | 33, 35 | bitrdi 290 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → ((𝐸‘𝑖) ∈ 𝒫 (Vtx‘𝑆) ↔ (𝐸‘𝑖) ⊆ 𝑉)) |
37 | 29, 36 | mpbird 260 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → (𝐸‘𝑖) ∈ 𝒫 (Vtx‘𝑆)) |
38 | 23, 37 | eqeltrd 2840 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑖) ∈ 𝒫 (Vtx‘𝑆)) |
39 | | eleq1 2827 |
. . . . . 6
⊢ (𝑒 = ((iEdg‘𝑆)‘𝑖) → (𝑒 ∈ 𝒫 (Vtx‘𝑆) ↔ ((iEdg‘𝑆)‘𝑖) ∈ 𝒫 (Vtx‘𝑆))) |
40 | 38, 39 | syl5ibrcom 250 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → (𝑒 = ((iEdg‘𝑆)‘𝑖) → 𝑒 ∈ 𝒫 (Vtx‘𝑆))) |
41 | 40 | rexlimdva 3213 |
. . . 4
⊢ (𝜑 → (∃𝑖 ∈ dom (iEdg‘𝑆)𝑒 = ((iEdg‘𝑆)‘𝑖) → 𝑒 ∈ 𝒫 (Vtx‘𝑆))) |
42 | 12, 41 | sylbid 243 |
. . 3
⊢ (𝜑 → (𝑒 ∈ ran (iEdg‘𝑆) → 𝑒 ∈ 𝒫 (Vtx‘𝑆))) |
43 | 2, 42 | syl5bi 245 |
. 2
⊢ (𝜑 → (𝑒 ∈ (Edg‘𝑆) → 𝑒 ∈ 𝒫 (Vtx‘𝑆))) |
44 | 43 | ssrdv 3924 |
1
⊢ (𝜑 → (Edg‘𝑆) ⊆ 𝒫
(Vtx‘𝑆)) |