Metamath Proof Explorer


Theorem 0grsubgr

Description: The null graph (represented by an empty set) is a subgraph of all graphs. (Contributed by AV, 17-Nov-2020)

Ref Expression
Assertion 0grsubgr
|- ( G e. W -> (/) SubGraph G )

Proof

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 )