Step |
Hyp |
Ref |
Expression |
1 |
|
0ss |
|- (/) C_ ( Vtx ` G ) |
2 |
|
dm0 |
|- dom (/) = (/) |
3 |
2
|
reseq2i |
|- ( ( iEdg ` G ) |` dom (/) ) = ( ( iEdg ` G ) |` (/) ) |
4 |
|
res0 |
|- ( ( iEdg ` G ) |` (/) ) = (/) |
5 |
3 4
|
eqtr2i |
|- (/) = ( ( iEdg ` G ) |` dom (/) ) |
6 |
|
0ss |
|- (/) C_ ~P (/) |
7 |
1 5 6
|
3pm3.2i |
|- ( (/) C_ ( Vtx ` G ) /\ (/) = ( ( iEdg ` G ) |` dom (/) ) /\ (/) C_ ~P (/) ) |
8 |
|
0ex |
|- (/) e. _V |
9 |
|
vtxval0 |
|- ( Vtx ` (/) ) = (/) |
10 |
9
|
eqcomi |
|- (/) = ( Vtx ` (/) ) |
11 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
12 |
|
iedgval0 |
|- ( iEdg ` (/) ) = (/) |
13 |
12
|
eqcomi |
|- (/) = ( iEdg ` (/) ) |
14 |
|
eqid |
|- ( iEdg ` G ) = ( iEdg ` G ) |
15 |
|
edgval |
|- ( Edg ` (/) ) = ran ( iEdg ` (/) ) |
16 |
12
|
rneqi |
|- ran ( iEdg ` (/) ) = ran (/) |
17 |
|
rn0 |
|- ran (/) = (/) |
18 |
15 16 17
|
3eqtrri |
|- (/) = ( Edg ` (/) ) |
19 |
10 11 13 14 18
|
issubgr |
|- ( ( G e. W /\ (/) e. _V ) -> ( (/) SubGraph G <-> ( (/) C_ ( Vtx ` G ) /\ (/) = ( ( iEdg ` G ) |` dom (/) ) /\ (/) C_ ~P (/) ) ) ) |
20 |
8 19
|
mpan2 |
|- ( G e. W -> ( (/) SubGraph G <-> ( (/) C_ ( Vtx ` G ) /\ (/) = ( ( iEdg ` G ) |` dom (/) ) /\ (/) C_ ~P (/) ) ) ) |
21 |
7 20
|
mpbiri |
|- ( G e. W -> (/) SubGraph G ) |