Proof of Theorem subumgredg2
Step | Hyp | Ref
| Expression |
1 | | fveqeq2 6776 |
. . 3
⊢ (𝑒 = (𝐼‘𝑋) → ((♯‘𝑒) = 2 ↔ (♯‘(𝐼‘𝑋)) = 2)) |
2 | | subumgredg2.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝑆) |
3 | | subumgredg2.i |
. . . 4
⊢ 𝐼 = (iEdg‘𝑆) |
4 | | umgruhgr 27462 |
. . . . 5
⊢ (𝐺 ∈ UMGraph → 𝐺 ∈
UHGraph) |
5 | 4 | 3ad2ant2 1133 |
. . . 4
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → 𝐺 ∈ UHGraph) |
6 | | simp1 1135 |
. . . 4
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → 𝑆 SubGraph 𝐺) |
7 | | simp3 1137 |
. . . 4
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → 𝑋 ∈ dom 𝐼) |
8 | 2, 3, 5, 6, 7 | subgruhgredgd 27639 |
. . 3
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘𝑋) ∈ (𝒫 𝑉 ∖ {∅})) |
9 | | eqid 2738 |
. . . . . . . . 9
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
10 | 9 | uhgrfun 27424 |
. . . . . . . 8
⊢ (𝐺 ∈ UHGraph → Fun
(iEdg‘𝐺)) |
11 | 4, 10 | syl 17 |
. . . . . . 7
⊢ (𝐺 ∈ UMGraph → Fun
(iEdg‘𝐺)) |
12 | 11 | 3ad2ant2 1133 |
. . . . . 6
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → Fun (iEdg‘𝐺)) |
13 | | eqid 2738 |
. . . . . . . . 9
⊢
(Vtx‘𝑆) =
(Vtx‘𝑆) |
14 | | eqid 2738 |
. . . . . . . . 9
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
15 | | eqid 2738 |
. . . . . . . . 9
⊢
(Edg‘𝑆) =
(Edg‘𝑆) |
16 | 13, 14, 3, 9, 15 | subgrprop2 27629 |
. . . . . . . 8
⊢ (𝑆 SubGraph 𝐺 → ((Vtx‘𝑆) ⊆ (Vtx‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 (Vtx‘𝑆))) |
17 | 16 | simp2d 1142 |
. . . . . . 7
⊢ (𝑆 SubGraph 𝐺 → 𝐼 ⊆ (iEdg‘𝐺)) |
18 | 17 | 3ad2ant1 1132 |
. . . . . 6
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → 𝐼 ⊆ (iEdg‘𝐺)) |
19 | | funssfv 6788 |
. . . . . . 7
⊢ ((Fun
(iEdg‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ 𝑋 ∈ dom 𝐼) → ((iEdg‘𝐺)‘𝑋) = (𝐼‘𝑋)) |
20 | 19 | eqcomd 2744 |
. . . . . 6
⊢ ((Fun
(iEdg‘𝐺) ∧ 𝐼 ⊆ (iEdg‘𝐺) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘𝑋) = ((iEdg‘𝐺)‘𝑋)) |
21 | 12, 18, 7, 20 | syl3anc 1370 |
. . . . 5
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘𝑋) = ((iEdg‘𝐺)‘𝑋)) |
22 | 21 | fveq2d 6771 |
. . . 4
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → (♯‘(𝐼‘𝑋)) = (♯‘((iEdg‘𝐺)‘𝑋))) |
23 | | simp2 1136 |
. . . . 5
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → 𝐺 ∈ UMGraph) |
24 | 3 | dmeqi 5807 |
. . . . . . . . 9
⊢ dom 𝐼 = dom (iEdg‘𝑆) |
25 | 24 | eleq2i 2830 |
. . . . . . . 8
⊢ (𝑋 ∈ dom 𝐼 ↔ 𝑋 ∈ dom (iEdg‘𝑆)) |
26 | | subgreldmiedg 27638 |
. . . . . . . . 9
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝑋 ∈ dom (iEdg‘𝑆)) → 𝑋 ∈ dom (iEdg‘𝐺)) |
27 | 26 | ex 413 |
. . . . . . . 8
⊢ (𝑆 SubGraph 𝐺 → (𝑋 ∈ dom (iEdg‘𝑆) → 𝑋 ∈ dom (iEdg‘𝐺))) |
28 | 25, 27 | syl5bi 241 |
. . . . . . 7
⊢ (𝑆 SubGraph 𝐺 → (𝑋 ∈ dom 𝐼 → 𝑋 ∈ dom (iEdg‘𝐺))) |
29 | 28 | a1d 25 |
. . . . . 6
⊢ (𝑆 SubGraph 𝐺 → (𝐺 ∈ UMGraph → (𝑋 ∈ dom 𝐼 → 𝑋 ∈ dom (iEdg‘𝐺)))) |
30 | 29 | 3imp 1110 |
. . . . 5
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → 𝑋 ∈ dom (iEdg‘𝐺)) |
31 | 14, 9 | umgredg2 27458 |
. . . . 5
⊢ ((𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom (iEdg‘𝐺)) →
(♯‘((iEdg‘𝐺)‘𝑋)) = 2) |
32 | 23, 30, 31 | syl2anc 584 |
. . . 4
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → (♯‘((iEdg‘𝐺)‘𝑋)) = 2) |
33 | 22, 32 | eqtrd 2778 |
. . 3
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → (♯‘(𝐼‘𝑋)) = 2) |
34 | 1, 8, 33 | elrabd 3626 |
. 2
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘𝑋) ∈ {𝑒 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑒) =
2}) |
35 | | prprrab 14175 |
. 2
⊢ {𝑒 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑒) = 2} =
{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2} |
36 | 34, 35 | eleqtrdi 2849 |
1
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘𝑋) ∈ {𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}) |