Proof of Theorem subgruhgredgd
Step | Hyp | Ref
| Expression |
1 | | subgruhgredgd.s |
. . 3
⊢ (𝜑 → 𝑆 SubGraph 𝐺) |
2 | | subgruhgredgd.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝑆) |
3 | | eqid 2610 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
4 | | subgruhgredgd.i |
. . . 4
⊢ 𝐼 = (iEdg‘𝑆) |
5 | | eqid 2610 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
6 | | eqid 2610 |
. . . 4
⊢
(Edg‘𝑆) =
(Edg‘𝑆) |
7 | 2, 3, 4, 5, 6 | subgrprop2 40498 |
. . 3
⊢ (𝑆 SubGraph 𝐺 → (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) |
8 | 1, 7 | syl 17 |
. 2
⊢ (𝜑 → (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) |
9 | | simpr3 1062 |
. . . 4
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → (Edg‘𝑆) ⊆ 𝒫 𝑉) |
10 | | subgruhgredgd.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ UHGraph ) |
11 | | subgruhgrfun 40506 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺) → Fun (iEdg‘𝑆)) |
12 | 10, 1, 11 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → Fun (iEdg‘𝑆)) |
13 | | subgruhgredgd.x |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ dom 𝐼) |
14 | 4 | dmeqi 5247 |
. . . . . . . . 9
⊢ dom 𝐼 = dom (iEdg‘𝑆) |
15 | 13, 14 | syl6eleq 2698 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ dom (iEdg‘𝑆)) |
16 | 12, 15 | jca 553 |
. . . . . . 7
⊢ (𝜑 → (Fun (iEdg‘𝑆) ∧ 𝑋 ∈ dom (iEdg‘𝑆))) |
17 | 16 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → (Fun (iEdg‘𝑆) ∧ 𝑋 ∈ dom (iEdg‘𝑆))) |
18 | 4 | fveq1i 6104 |
. . . . . . 7
⊢ (𝐼‘𝑋) = ((iEdg‘𝑆)‘𝑋) |
19 | | fvelrn 6260 |
. . . . . . 7
⊢ ((Fun
(iEdg‘𝑆) ∧ 𝑋 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑋) ∈ ran (iEdg‘𝑆)) |
20 | 18, 19 | syl5eqel 2692 |
. . . . . 6
⊢ ((Fun
(iEdg‘𝑆) ∧ 𝑋 ∈ dom (iEdg‘𝑆)) → (𝐼‘𝑋) ∈ ran (iEdg‘𝑆)) |
21 | 17, 20 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → (𝐼‘𝑋) ∈ ran (iEdg‘𝑆)) |
22 | | subgrv 40494 |
. . . . . . . . 9
⊢ (𝑆 SubGraph 𝐺 → (𝑆 ∈ V ∧ 𝐺 ∈ V)) |
23 | 22 | simpld 474 |
. . . . . . . 8
⊢ (𝑆 SubGraph 𝐺 → 𝑆 ∈ V) |
24 | 1, 23 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ V) |
25 | | edgaval 25794 |
. . . . . . 7
⊢ (𝑆 ∈ V →
(Edg‘𝑆) = ran
(iEdg‘𝑆)) |
26 | 24, 25 | syl 17 |
. . . . . 6
⊢ (𝜑 → (Edg‘𝑆) = ran (iEdg‘𝑆)) |
27 | 26 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → (Edg‘𝑆) = ran (iEdg‘𝑆)) |
28 | 21, 27 | eleqtrrd 2691 |
. . . 4
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → (𝐼‘𝑋) ∈ (Edg‘𝑆)) |
29 | 9, 28 | sseldd 3569 |
. . 3
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → (𝐼‘𝑋) ∈ 𝒫 𝑉) |
30 | 5 | uhgrfun 25732 |
. . . . . . 7
⊢ (𝐺 ∈ UHGraph → Fun
(iEdg‘𝐺)) |
31 | 10, 30 | syl 17 |
. . . . . 6
⊢ (𝜑 → Fun (iEdg‘𝐺)) |
32 | 31 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → Fun (iEdg‘𝐺)) |
33 | | simpr2 1061 |
. . . . 5
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → 𝐼 ⊆ (iEdg‘𝐺)) |
34 | 13 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → 𝑋 ∈ dom 𝐼) |
35 | | funssfv 6119 |
. . . . . 6
⊢ ((Fun
(iEdg‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ 𝑋 ∈ dom 𝐼) → ((iEdg‘𝐺)‘𝑋) = (𝐼‘𝑋)) |
36 | 35 | eqcomd 2616 |
. . . . 5
⊢ ((Fun
(iEdg‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘𝑋) = ((iEdg‘𝐺)‘𝑋)) |
37 | 32, 33, 34, 36 | syl3anc 1318 |
. . . 4
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → (𝐼‘𝑋) = ((iEdg‘𝐺)‘𝑋)) |
38 | 10 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → 𝐺 ∈ UHGraph ) |
39 | | funfn 5833 |
. . . . . . 7
⊢ (Fun
(iEdg‘𝐺) ↔
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
40 | 31, 39 | sylib 207 |
. . . . . 6
⊢ (𝜑 → (iEdg‘𝐺) Fn dom (iEdg‘𝐺)) |
41 | 40 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → (iEdg‘𝐺) Fn dom (iEdg‘𝐺)) |
42 | | subgreldmiedg 40507 |
. . . . . . 7
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝑋 ∈ dom (iEdg‘𝑆)) → 𝑋 ∈ dom (iEdg‘𝐺)) |
43 | 1, 15, 42 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ dom (iEdg‘𝐺)) |
44 | 43 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → 𝑋 ∈ dom (iEdg‘𝐺)) |
45 | 5 | uhgrn0 25733 |
. . . . 5
⊢ ((𝐺 ∈ UHGraph ∧
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺) ∧ 𝑋 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑋) ≠ ∅) |
46 | 38, 41, 44, 45 | syl3anc 1318 |
. . . 4
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → ((iEdg‘𝐺)‘𝑋) ≠ ∅) |
47 | 37, 46 | eqnetrd 2849 |
. . 3
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → (𝐼‘𝑋) ≠ ∅) |
48 | | eldifsn 4260 |
. . 3
⊢ ((𝐼‘𝑋) ∈ (𝒫 𝑉 ∖ {∅}) ↔ ((𝐼‘𝑋) ∈ 𝒫 𝑉 ∧ (𝐼‘𝑋) ≠ ∅)) |
49 | 29, 47, 48 | sylanbrc 695 |
. 2
⊢ ((𝜑 ∧ (𝑉 ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) → (𝐼‘𝑋) ∈ (𝒫 𝑉 ∖ {∅})) |
50 | 8, 49 | mpdan 699 |
1
⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝒫 𝑉 ∖ {∅})) |