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 )