Step | Hyp | Ref
| Expression |
1 | | uhgrspan.s |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ 𝑊) |
2 | | edgaval 25794 |
. . . . 5
⊢ (𝑆 ∈ 𝑊 → (Edg‘𝑆) = ran (iEdg‘𝑆)) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → (Edg‘𝑆) = ran (iEdg‘𝑆)) |
4 | 3 | eleq2d 2673 |
. . 3
⊢ (𝜑 → (𝑒 ∈ (Edg‘𝑆) ↔ 𝑒 ∈ ran (iEdg‘𝑆))) |
5 | | uhgrspan.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ UHGraph ) |
6 | | uhgrspan.e |
. . . . . . . . 9
⊢ 𝐸 = (iEdg‘𝐺) |
7 | 6 | uhgrfun 25732 |
. . . . . . . 8
⊢ (𝐺 ∈ UHGraph → Fun 𝐸) |
8 | 5, 7 | syl 17 |
. . . . . . 7
⊢ (𝜑 → Fun 𝐸) |
9 | | funres 5843 |
. . . . . . 7
⊢ (Fun
𝐸 → Fun (𝐸 ↾ 𝐴)) |
10 | 8, 9 | syl 17 |
. . . . . 6
⊢ (𝜑 → Fun (𝐸 ↾ 𝐴)) |
11 | | uhgrspan.r |
. . . . . . 7
⊢ (𝜑 → (iEdg‘𝑆) = (𝐸 ↾ 𝐴)) |
12 | 11 | funeqd 5825 |
. . . . . 6
⊢ (𝜑 → (Fun (iEdg‘𝑆) ↔ Fun (𝐸 ↾ 𝐴))) |
13 | 10, 12 | mpbird 246 |
. . . . 5
⊢ (𝜑 → Fun (iEdg‘𝑆)) |
14 | | elrnrexdmb 6272 |
. . . . 5
⊢ (Fun
(iEdg‘𝑆) →
(𝑒 ∈ ran
(iEdg‘𝑆) ↔
∃𝑖 ∈ dom
(iEdg‘𝑆)𝑒 = ((iEdg‘𝑆)‘𝑖))) |
15 | 13, 14 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑒 ∈ ran (iEdg‘𝑆) ↔ ∃𝑖 ∈ dom (iEdg‘𝑆)𝑒 = ((iEdg‘𝑆)‘𝑖))) |
16 | 11 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → (iEdg‘𝑆) = (𝐸 ↾ 𝐴)) |
17 | 16 | fveq1d 6105 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑖) = ((𝐸 ↾ 𝐴)‘𝑖)) |
18 | 11 | dmeqd 5248 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom (iEdg‘𝑆) = dom (𝐸 ↾ 𝐴)) |
19 | | dmres 5339 |
. . . . . . . . . . . . 13
⊢ dom
(𝐸 ↾ 𝐴) = (𝐴 ∩ dom 𝐸) |
20 | 18, 19 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom (iEdg‘𝑆) = (𝐴 ∩ dom 𝐸)) |
21 | 20 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑖 ∈ dom (iEdg‘𝑆) ↔ 𝑖 ∈ (𝐴 ∩ dom 𝐸))) |
22 | | elinel1 3761 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (𝐴 ∩ dom 𝐸) → 𝑖 ∈ 𝐴) |
23 | 21, 22 | syl6bi 242 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑖 ∈ dom (iEdg‘𝑆) → 𝑖 ∈ 𝐴)) |
24 | 23 | imp 444 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → 𝑖 ∈ 𝐴) |
25 | | fvres 6117 |
. . . . . . . . 9
⊢ (𝑖 ∈ 𝐴 → ((𝐸 ↾ 𝐴)‘𝑖) = (𝐸‘𝑖)) |
26 | 24, 25 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → ((𝐸 ↾ 𝐴)‘𝑖) = (𝐸‘𝑖)) |
27 | 17, 26 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑖) = (𝐸‘𝑖)) |
28 | 5 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → 𝐺 ∈ UHGraph ) |
29 | | elinel2 3762 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (𝐴 ∩ dom 𝐸) → 𝑖 ∈ dom 𝐸) |
30 | 21, 29 | syl6bi 242 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑖 ∈ dom (iEdg‘𝑆) → 𝑖 ∈ dom 𝐸)) |
31 | 30 | imp 444 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → 𝑖 ∈ dom 𝐸) |
32 | | uhgrspan.v |
. . . . . . . . . 10
⊢ 𝑉 = (Vtx‘𝐺) |
33 | 32, 6 | uhgrss 25730 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UHGraph ∧ 𝑖 ∈ dom 𝐸) → (𝐸‘𝑖) ⊆ 𝑉) |
34 | 28, 31, 33 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → (𝐸‘𝑖) ⊆ 𝑉) |
35 | | uhgrspan.q |
. . . . . . . . . . . 12
⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) |
36 | 35 | pweqd 4113 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝒫 (Vtx‘𝑆) = 𝒫 𝑉) |
37 | 36 | eleq2d 2673 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐸‘𝑖) ∈ 𝒫 (Vtx‘𝑆) ↔ (𝐸‘𝑖) ∈ 𝒫 𝑉)) |
38 | 37 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → ((𝐸‘𝑖) ∈ 𝒫 (Vtx‘𝑆) ↔ (𝐸‘𝑖) ∈ 𝒫 𝑉)) |
39 | | fvex 6113 |
. . . . . . . . . 10
⊢ (𝐸‘𝑖) ∈ V |
40 | 39 | elpw 4114 |
. . . . . . . . 9
⊢ ((𝐸‘𝑖) ∈ 𝒫 𝑉 ↔ (𝐸‘𝑖) ⊆ 𝑉) |
41 | 38, 40 | syl6bb 275 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → ((𝐸‘𝑖) ∈ 𝒫 (Vtx‘𝑆) ↔ (𝐸‘𝑖) ⊆ 𝑉)) |
42 | 34, 41 | mpbird 246 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → (𝐸‘𝑖) ∈ 𝒫 (Vtx‘𝑆)) |
43 | 27, 42 | eqeltrd 2688 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑖) ∈ 𝒫 (Vtx‘𝑆)) |
44 | | eleq1 2676 |
. . . . . 6
⊢ (𝑒 = ((iEdg‘𝑆)‘𝑖) → (𝑒 ∈ 𝒫 (Vtx‘𝑆) ↔ ((iEdg‘𝑆)‘𝑖) ∈ 𝒫 (Vtx‘𝑆))) |
45 | 43, 44 | syl5ibrcom 236 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ dom (iEdg‘𝑆)) → (𝑒 = ((iEdg‘𝑆)‘𝑖) → 𝑒 ∈ 𝒫 (Vtx‘𝑆))) |
46 | 45 | rexlimdva 3013 |
. . . 4
⊢ (𝜑 → (∃𝑖 ∈ dom (iEdg‘𝑆)𝑒 = ((iEdg‘𝑆)‘𝑖) → 𝑒 ∈ 𝒫 (Vtx‘𝑆))) |
47 | 15, 46 | sylbid 229 |
. . 3
⊢ (𝜑 → (𝑒 ∈ ran (iEdg‘𝑆) → 𝑒 ∈ 𝒫 (Vtx‘𝑆))) |
48 | 4, 47 | sylbid 229 |
. 2
⊢ (𝜑 → (𝑒 ∈ (Edg‘𝑆) → 𝑒 ∈ 𝒫 (Vtx‘𝑆))) |
49 | 48 | ssrdv 3574 |
1
⊢ (𝜑 → (Edg‘𝑆) ⊆ 𝒫
(Vtx‘𝑆)) |