Proof of Theorem 0uhgrsubgr
Step | Hyp | Ref
| Expression |
1 | | 3simpa 1051 |
. 2
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ UHGraph ∧ (Vtx‘𝑆) = ∅) → (𝐺 ∈ 𝑊 ∧ 𝑆 ∈ UHGraph )) |
2 | | 0ss 3924 |
. . . 4
⊢ ∅
⊆ (Vtx‘𝐺) |
3 | | sseq1 3589 |
. . . 4
⊢
((Vtx‘𝑆) =
∅ → ((Vtx‘𝑆) ⊆ (Vtx‘𝐺) ↔ ∅ ⊆ (Vtx‘𝐺))) |
4 | 2, 3 | mpbiri 247 |
. . 3
⊢
((Vtx‘𝑆) =
∅ → (Vtx‘𝑆) ⊆ (Vtx‘𝐺)) |
5 | 4 | 3ad2ant3 1077 |
. 2
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ UHGraph ∧ (Vtx‘𝑆) = ∅) →
(Vtx‘𝑆) ⊆
(Vtx‘𝐺)) |
6 | | eqid 2610 |
. . . 4
⊢
(iEdg‘𝑆) =
(iEdg‘𝑆) |
7 | 6 | uhgrfun 25732 |
. . 3
⊢ (𝑆 ∈ UHGraph → Fun
(iEdg‘𝑆)) |
8 | 7 | 3ad2ant2 1076 |
. 2
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ UHGraph ∧ (Vtx‘𝑆) = ∅) → Fun
(iEdg‘𝑆)) |
9 | | edgaval 25794 |
. . . 4
⊢ (𝑆 ∈ UHGraph →
(Edg‘𝑆) = ran
(iEdg‘𝑆)) |
10 | 9 | 3ad2ant2 1076 |
. . 3
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ UHGraph ∧ (Vtx‘𝑆) = ∅) →
(Edg‘𝑆) = ran
(iEdg‘𝑆)) |
11 | | uhgr0vb 25738 |
. . . . . . . 8
⊢ ((𝑆 ∈ UHGraph ∧
(Vtx‘𝑆) = ∅)
→ (𝑆 ∈ UHGraph
↔ (iEdg‘𝑆) =
∅)) |
12 | | rneq 5272 |
. . . . . . . . 9
⊢
((iEdg‘𝑆) =
∅ → ran (iEdg‘𝑆) = ran ∅) |
13 | | rn0 5298 |
. . . . . . . . 9
⊢ ran
∅ = ∅ |
14 | 12, 13 | syl6eq 2660 |
. . . . . . . 8
⊢
((iEdg‘𝑆) =
∅ → ran (iEdg‘𝑆) = ∅) |
15 | 11, 14 | syl6bi 242 |
. . . . . . 7
⊢ ((𝑆 ∈ UHGraph ∧
(Vtx‘𝑆) = ∅)
→ (𝑆 ∈ UHGraph
→ ran (iEdg‘𝑆) =
∅)) |
16 | 15 | ex 449 |
. . . . . 6
⊢ (𝑆 ∈ UHGraph →
((Vtx‘𝑆) = ∅
→ (𝑆 ∈ UHGraph
→ ran (iEdg‘𝑆) =
∅))) |
17 | 16 | pm2.43a 52 |
. . . . 5
⊢ (𝑆 ∈ UHGraph →
((Vtx‘𝑆) = ∅
→ ran (iEdg‘𝑆) =
∅)) |
18 | 17 | a1i 11 |
. . . 4
⊢ (𝐺 ∈ 𝑊 → (𝑆 ∈ UHGraph → ((Vtx‘𝑆) = ∅ → ran
(iEdg‘𝑆) =
∅))) |
19 | 18 | 3imp 1249 |
. . 3
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ UHGraph ∧ (Vtx‘𝑆) = ∅) → ran
(iEdg‘𝑆) =
∅) |
20 | 10, 19 | eqtrd 2644 |
. 2
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ UHGraph ∧ (Vtx‘𝑆) = ∅) →
(Edg‘𝑆) =
∅) |
21 | | egrsubgr 40501 |
. 2
⊢ (((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ UHGraph ) ∧ (Vtx‘𝑆) ⊆ (Vtx‘𝐺) ∧ (Fun (iEdg‘𝑆) ∧ (Edg‘𝑆) = ∅)) → 𝑆 SubGraph 𝐺) |
22 | 1, 5, 8, 20, 21 | syl112anc 1322 |
1
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ UHGraph ∧ (Vtx‘𝑆) = ∅) → 𝑆 SubGraph 𝐺) |