Proof of Theorem subumgredg2
Step | Hyp | Ref
| Expression |
1 | | subumgredg2.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝑆) |
2 | | subumgredg2.i |
. . . 4
⊢ 𝐼 = (iEdg‘𝑆) |
3 | | umgruhgr 25770 |
. . . . 5
⊢ (𝐺 ∈ UMGraph → 𝐺 ∈ UHGraph
) |
4 | 3 | 3ad2ant2 1076 |
. . . 4
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → 𝐺 ∈ UHGraph ) |
5 | | simp1 1054 |
. . . 4
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → 𝑆 SubGraph 𝐺) |
6 | | simp3 1056 |
. . . 4
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → 𝑋 ∈ dom 𝐼) |
7 | 1, 2, 4, 5, 6 | subgruhgredgd 40508 |
. . 3
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘𝑋) ∈ (𝒫 𝑉 ∖ {∅})) |
8 | | eqid 2610 |
. . . . . . . . 9
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
9 | 8 | uhgrfun 25732 |
. . . . . . . 8
⊢ (𝐺 ∈ UHGraph → Fun
(iEdg‘𝐺)) |
10 | 3, 9 | syl 17 |
. . . . . . 7
⊢ (𝐺 ∈ UMGraph → Fun
(iEdg‘𝐺)) |
11 | 10 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → Fun (iEdg‘𝐺)) |
12 | | eqid 2610 |
. . . . . . . . 9
⊢
(Vtx‘𝑆) =
(Vtx‘𝑆) |
13 | | eqid 2610 |
. . . . . . . . 9
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
14 | | eqid 2610 |
. . . . . . . . 9
⊢
(Edg‘𝑆) =
(Edg‘𝑆) |
15 | 12, 13, 2, 8, 14 | subgrprop2 40498 |
. . . . . . . 8
⊢ (𝑆 SubGraph 𝐺 → ((Vtx‘𝑆) ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 (Vtx‘𝑆))) |
16 | 15 | simp2d 1067 |
. . . . . . 7
⊢ (𝑆 SubGraph 𝐺 → 𝐼 ⊆ (iEdg‘𝐺)) |
17 | 16 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → 𝐼 ⊆ (iEdg‘𝐺)) |
18 | | funssfv 6119 |
. . . . . . 7
⊢ ((Fun
(iEdg‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ 𝑋 ∈ dom 𝐼) → ((iEdg‘𝐺)‘𝑋) = (𝐼‘𝑋)) |
19 | 18 | eqcomd 2616 |
. . . . . 6
⊢ ((Fun
(iEdg‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘𝑋) = ((iEdg‘𝐺)‘𝑋)) |
20 | 11, 17, 6, 19 | syl3anc 1318 |
. . . . 5
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘𝑋) = ((iEdg‘𝐺)‘𝑋)) |
21 | 20 | fveq2d 6107 |
. . . 4
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → (#‘(𝐼‘𝑋)) = (#‘((iEdg‘𝐺)‘𝑋))) |
22 | | simp2 1055 |
. . . . 5
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → 𝐺 ∈ UMGraph ) |
23 | 2 | dmeqi 5247 |
. . . . . . . . 9
⊢ dom 𝐼 = dom (iEdg‘𝑆) |
24 | 23 | eleq2i 2680 |
. . . . . . . 8
⊢ (𝑋 ∈ dom 𝐼 ↔ 𝑋 ∈ dom (iEdg‘𝑆)) |
25 | | subgreldmiedg 40507 |
. . . . . . . . 9
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝑋 ∈ dom (iEdg‘𝑆)) → 𝑋 ∈ dom (iEdg‘𝐺)) |
26 | 25 | ex 449 |
. . . . . . . 8
⊢ (𝑆 SubGraph 𝐺 → (𝑋 ∈ dom (iEdg‘𝑆) → 𝑋 ∈ dom (iEdg‘𝐺))) |
27 | 24, 26 | syl5bi 231 |
. . . . . . 7
⊢ (𝑆 SubGraph 𝐺 → (𝑋 ∈ dom 𝐼 → 𝑋 ∈ dom (iEdg‘𝐺))) |
28 | 27 | a1d 25 |
. . . . . 6
⊢ (𝑆 SubGraph 𝐺 → (𝐺 ∈ UMGraph → (𝑋 ∈ dom 𝐼 → 𝑋 ∈ dom (iEdg‘𝐺)))) |
29 | 28 | 3imp 1249 |
. . . . 5
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → 𝑋 ∈ dom (iEdg‘𝐺)) |
30 | 13, 8 | umgredg2 25766 |
. . . . 5
⊢ ((𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom (iEdg‘𝐺)) →
(#‘((iEdg‘𝐺)‘𝑋)) = 2) |
31 | 22, 29, 30 | syl2anc 691 |
. . . 4
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → (#‘((iEdg‘𝐺)‘𝑋)) = 2) |
32 | 21, 31 | eqtrd 2644 |
. . 3
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → (#‘(𝐼‘𝑋)) = 2) |
33 | | fveq2 6103 |
. . . . 5
⊢ (𝑒 = (𝐼‘𝑋) → (#‘𝑒) = (#‘(𝐼‘𝑋))) |
34 | 33 | eqeq1d 2612 |
. . . 4
⊢ (𝑒 = (𝐼‘𝑋) → ((#‘𝑒) = 2 ↔ (#‘(𝐼‘𝑋)) = 2)) |
35 | 34 | elrab 3331 |
. . 3
⊢ ((𝐼‘𝑋) ∈ {𝑒 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑒) = 2} ↔ ((𝐼‘𝑋) ∈ (𝒫 𝑉 ∖ {∅}) ∧ (#‘(𝐼‘𝑋)) = 2)) |
36 | 7, 32, 35 | sylanbrc 695 |
. 2
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘𝑋) ∈ {𝑒 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑒) = 2}) |
37 | | prprrab 13112 |
. 2
⊢ {𝑒 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(#‘𝑒) = 2} = {𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2} |
38 | 36, 37 | syl6eleq 2698 |
1
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘𝑋) ∈ {𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2}) |