| Step |
Hyp |
Ref |
Expression |
| 1 |
|
3simpa |
|- ( ( G e. W /\ S e. UHGraph /\ ( Vtx ` S ) = (/) ) -> ( G e. W /\ S e. UHGraph ) ) |
| 2 |
|
0ss |
|- (/) C_ ( Vtx ` G ) |
| 3 |
|
sseq1 |
|- ( ( Vtx ` S ) = (/) -> ( ( Vtx ` S ) C_ ( Vtx ` G ) <-> (/) C_ ( Vtx ` G ) ) ) |
| 4 |
2 3
|
mpbiri |
|- ( ( Vtx ` S ) = (/) -> ( Vtx ` S ) C_ ( Vtx ` G ) ) |
| 5 |
4
|
3ad2ant3 |
|- ( ( G e. W /\ S e. UHGraph /\ ( Vtx ` S ) = (/) ) -> ( Vtx ` S ) C_ ( Vtx ` G ) ) |
| 6 |
|
eqid |
|- ( iEdg ` S ) = ( iEdg ` S ) |
| 7 |
6
|
uhgrfun |
|- ( S e. UHGraph -> Fun ( iEdg ` S ) ) |
| 8 |
7
|
3ad2ant2 |
|- ( ( G e. W /\ S e. UHGraph /\ ( Vtx ` S ) = (/) ) -> Fun ( iEdg ` S ) ) |
| 9 |
|
edgval |
|- ( Edg ` S ) = ran ( iEdg ` S ) |
| 10 |
|
uhgr0vb |
|- ( ( S e. UHGraph /\ ( Vtx ` S ) = (/) ) -> ( S e. UHGraph <-> ( iEdg ` S ) = (/) ) ) |
| 11 |
|
rneq |
|- ( ( iEdg ` S ) = (/) -> ran ( iEdg ` S ) = ran (/) ) |
| 12 |
|
rn0 |
|- ran (/) = (/) |
| 13 |
11 12
|
eqtrdi |
|- ( ( iEdg ` S ) = (/) -> ran ( iEdg ` S ) = (/) ) |
| 14 |
10 13
|
biimtrdi |
|- ( ( S e. UHGraph /\ ( Vtx ` S ) = (/) ) -> ( S e. UHGraph -> ran ( iEdg ` S ) = (/) ) ) |
| 15 |
14
|
ex |
|- ( S e. UHGraph -> ( ( Vtx ` S ) = (/) -> ( S e. UHGraph -> ran ( iEdg ` S ) = (/) ) ) ) |
| 16 |
15
|
pm2.43a |
|- ( S e. UHGraph -> ( ( Vtx ` S ) = (/) -> ran ( iEdg ` S ) = (/) ) ) |
| 17 |
16
|
a1i |
|- ( G e. W -> ( S e. UHGraph -> ( ( Vtx ` S ) = (/) -> ran ( iEdg ` S ) = (/) ) ) ) |
| 18 |
17
|
3imp |
|- ( ( G e. W /\ S e. UHGraph /\ ( Vtx ` S ) = (/) ) -> ran ( iEdg ` S ) = (/) ) |
| 19 |
9 18
|
eqtrid |
|- ( ( G e. W /\ S e. UHGraph /\ ( Vtx ` S ) = (/) ) -> ( Edg ` S ) = (/) ) |
| 20 |
|
egrsubgr |
|- ( ( ( G e. W /\ S e. UHGraph ) /\ ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( Fun ( iEdg ` S ) /\ ( Edg ` S ) = (/) ) ) -> S SubGraph G ) |
| 21 |
1 5 8 19 20
|
syl112anc |
|- ( ( G e. W /\ S e. UHGraph /\ ( Vtx ` S ) = (/) ) -> S SubGraph G ) |