Proof of Theorem subgruhgredgd
Step | Hyp | Ref
| Expression |
1 | | subgruhgredgd.s |
. . 3
⊢ (𝜑 → 𝑆 SubGraph 𝐺) |
2 | | subgruhgredgd.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝑆) |
3 | | eqid 2752 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
4 | | subgruhgredgd.i |
. . . 4
⊢ 𝐼 = (iEdg‘𝑆) |
5 | | eqid 2752 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
6 | | eqid 2752 |
. . . 4
⊢
(Edg‘𝑆) =
(Edg‘𝑆) |
7 | 2, 3, 4, 5, 6 | subgrprop2 26357 |
. . 3
⊢ (𝑆 SubGraph 𝐺 → (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) |
8 | 1, 7 | syl 17 |
. 2
⊢ (𝜑 → (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) |
9 | | simpr3 1235 |
. . . 4
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → (Edg‘𝑆) ⊆ 𝒫 𝑉) |
10 | | subgruhgredgd.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ UHGraph) |
11 | | subgruhgrfun 26365 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺) → Fun (iEdg‘𝑆)) |
12 | 10, 1, 11 | syl2anc 696 |
. . . . . . . 8
⊢ (𝜑 → Fun (iEdg‘𝑆)) |
13 | | subgruhgredgd.x |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ dom 𝐼) |
14 | 4 | dmeqi 5472 |
. . . . . . . . 9
⊢ dom 𝐼 = dom (iEdg‘𝑆) |
15 | 13, 14 | syl6eleq 2841 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ dom (iEdg‘𝑆)) |
16 | 12, 15 | jca 555 |
. . . . . . 7
⊢ (𝜑 → (Fun (iEdg‘𝑆) ∧ 𝑋 ∈ dom (iEdg‘𝑆))) |
17 | 16 | adantr 472 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → (Fun (iEdg‘𝑆) ∧ 𝑋 ∈ dom (iEdg‘𝑆))) |
18 | 4 | fveq1i 6345 |
. . . . . . 7
⊢ (𝐼‘𝑋) = ((iEdg‘𝑆)‘𝑋) |
19 | | fvelrn 6507 |
. . . . . . 7
⊢ ((Fun
(iEdg‘𝑆) ∧ 𝑋 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑋) ∈ ran (iEdg‘𝑆)) |
20 | 18, 19 | syl5eqel 2835 |
. . . . . 6
⊢ ((Fun
(iEdg‘𝑆) ∧ 𝑋 ∈ dom (iEdg‘𝑆)) → (𝐼‘𝑋) ∈ ran (iEdg‘𝑆)) |
21 | 17, 20 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → (𝐼‘𝑋) ∈ ran (iEdg‘𝑆)) |
22 | | edgval 26132 |
. . . . 5
⊢
(Edg‘𝑆) = ran
(iEdg‘𝑆) |
23 | 21, 22 | syl6eleqr 2842 |
. . . 4
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → (𝐼‘𝑋) ∈ (Edg‘𝑆)) |
24 | 9, 23 | sseldd 3737 |
. . 3
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → (𝐼‘𝑋) ∈ 𝒫 𝑉) |
25 | 5 | uhgrfun 26152 |
. . . . . . 7
⊢ (𝐺 ∈ UHGraph → Fun
(iEdg‘𝐺)) |
26 | 10, 25 | syl 17 |
. . . . . 6
⊢ (𝜑 → Fun (iEdg‘𝐺)) |
27 | 26 | adantr 472 |
. . . . 5
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → Fun (iEdg‘𝐺)) |
28 | | simpr2 1233 |
. . . . 5
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → 𝐼 ⊆ (iEdg‘𝐺)) |
29 | 13 | adantr 472 |
. . . . 5
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → 𝑋 ∈ dom 𝐼) |
30 | | funssfv 6362 |
. . . . . 6
⊢ ((Fun
(iEdg‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ 𝑋 ∈ dom 𝐼) → ((iEdg‘𝐺)‘𝑋) = (𝐼‘𝑋)) |
31 | 30 | eqcomd 2758 |
. . . . 5
⊢ ((Fun
(iEdg‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘𝑋) = ((iEdg‘𝐺)‘𝑋)) |
32 | 27, 28, 29, 31 | syl3anc 1473 |
. . . 4
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → (𝐼‘𝑋) = ((iEdg‘𝐺)‘𝑋)) |
33 | 10 | adantr 472 |
. . . . 5
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → 𝐺 ∈ UHGraph) |
34 | | funfn 6071 |
. . . . . . 7
⊢ (Fun
(iEdg‘𝐺) ↔
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
35 | 26, 34 | sylib 208 |
. . . . . 6
⊢ (𝜑 → (iEdg‘𝐺) Fn dom (iEdg‘𝐺)) |
36 | 35 | adantr 472 |
. . . . 5
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → (iEdg‘𝐺) Fn dom (iEdg‘𝐺)) |
37 | | subgreldmiedg 26366 |
. . . . . . 7
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝑋 ∈ dom (iEdg‘𝑆)) → 𝑋 ∈ dom (iEdg‘𝐺)) |
38 | 1, 15, 37 | syl2anc 696 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ dom (iEdg‘𝐺)) |
39 | 38 | adantr 472 |
. . . . 5
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → 𝑋 ∈ dom (iEdg‘𝐺)) |
40 | 5 | uhgrn0 26153 |
. . . . 5
⊢ ((𝐺 ∈ UHGraph ∧
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺) ∧ 𝑋 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑋) ≠ ∅) |
41 | 33, 36, 39, 40 | syl3anc 1473 |
. . . 4
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → ((iEdg‘𝐺)‘𝑋) ≠ ∅) |
42 | 32, 41 | eqnetrd 2991 |
. . 3
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → (𝐼‘𝑋) ≠ ∅) |
43 | | eldifsn 4454 |
. . 3
⊢ ((𝐼‘𝑋) ∈ (𝒫 𝑉 ∖ {∅}) ↔ ((𝐼‘𝑋) ∈ 𝒫 𝑉 ∧ (𝐼‘𝑋) ≠ ∅)) |
44 | 24, 42, 43 | sylanbrc 701 |
. 2
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → (𝐼‘𝑋) ∈ (𝒫 𝑉 ∖ {∅})) |
45 | 8, 44 | mpdan 705 |
1
⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝒫 𝑉 ∖ {∅})) |