Step |
Hyp |
Ref |
Expression |
1 |
|
3simpa |
⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ UHGraph ∧ ( Vtx ‘ 𝑆 ) = ∅ ) → ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ UHGraph ) ) |
2 |
|
0ss |
⊢ ∅ ⊆ ( Vtx ‘ 𝐺 ) |
3 |
|
sseq1 |
⊢ ( ( Vtx ‘ 𝑆 ) = ∅ → ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ↔ ∅ ⊆ ( Vtx ‘ 𝐺 ) ) ) |
4 |
2 3
|
mpbiri |
⊢ ( ( Vtx ‘ 𝑆 ) = ∅ → ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ) |
5 |
4
|
3ad2ant3 |
⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ UHGraph ∧ ( Vtx ‘ 𝑆 ) = ∅ ) → ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ) |
6 |
|
eqid |
⊢ ( iEdg ‘ 𝑆 ) = ( iEdg ‘ 𝑆 ) |
7 |
6
|
uhgrfun |
⊢ ( 𝑆 ∈ UHGraph → Fun ( iEdg ‘ 𝑆 ) ) |
8 |
7
|
3ad2ant2 |
⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ UHGraph ∧ ( Vtx ‘ 𝑆 ) = ∅ ) → Fun ( iEdg ‘ 𝑆 ) ) |
9 |
|
edgval |
⊢ ( Edg ‘ 𝑆 ) = ran ( iEdg ‘ 𝑆 ) |
10 |
|
uhgr0vb |
⊢ ( ( 𝑆 ∈ UHGraph ∧ ( Vtx ‘ 𝑆 ) = ∅ ) → ( 𝑆 ∈ UHGraph ↔ ( iEdg ‘ 𝑆 ) = ∅ ) ) |
11 |
|
rneq |
⊢ ( ( iEdg ‘ 𝑆 ) = ∅ → ran ( iEdg ‘ 𝑆 ) = ran ∅ ) |
12 |
|
rn0 |
⊢ ran ∅ = ∅ |
13 |
11 12
|
eqtrdi |
⊢ ( ( iEdg ‘ 𝑆 ) = ∅ → ran ( iEdg ‘ 𝑆 ) = ∅ ) |
14 |
10 13
|
syl6bi |
⊢ ( ( 𝑆 ∈ UHGraph ∧ ( Vtx ‘ 𝑆 ) = ∅ ) → ( 𝑆 ∈ UHGraph → ran ( iEdg ‘ 𝑆 ) = ∅ ) ) |
15 |
14
|
ex |
⊢ ( 𝑆 ∈ UHGraph → ( ( Vtx ‘ 𝑆 ) = ∅ → ( 𝑆 ∈ UHGraph → ran ( iEdg ‘ 𝑆 ) = ∅ ) ) ) |
16 |
15
|
pm2.43a |
⊢ ( 𝑆 ∈ UHGraph → ( ( Vtx ‘ 𝑆 ) = ∅ → ran ( iEdg ‘ 𝑆 ) = ∅ ) ) |
17 |
16
|
a1i |
⊢ ( 𝐺 ∈ 𝑊 → ( 𝑆 ∈ UHGraph → ( ( Vtx ‘ 𝑆 ) = ∅ → ran ( iEdg ‘ 𝑆 ) = ∅ ) ) ) |
18 |
17
|
3imp |
⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ UHGraph ∧ ( Vtx ‘ 𝑆 ) = ∅ ) → ran ( iEdg ‘ 𝑆 ) = ∅ ) |
19 |
9 18
|
syl5eq |
⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ UHGraph ∧ ( Vtx ‘ 𝑆 ) = ∅ ) → ( Edg ‘ 𝑆 ) = ∅ ) |
20 |
|
egrsubgr |
⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ UHGraph ) ∧ ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( Fun ( iEdg ‘ 𝑆 ) ∧ ( Edg ‘ 𝑆 ) = ∅ ) ) → 𝑆 SubGraph 𝐺 ) |
21 |
1 5 8 19 20
|
syl112anc |
⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ UHGraph ∧ ( Vtx ‘ 𝑆 ) = ∅ ) → 𝑆 SubGraph 𝐺 ) |