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∈W→∅SubGraphG

Proof

Step Hyp Ref Expression
1 0ss ⊢∅⊆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 ⊢∅⊆𝒫∅
7 1 5 6 3pm3.2i ⊢∅⊆Vtx⁡G∧∅=iEdg⁡G↾dom⁡∅∧∅⊆𝒫∅
8 0ex ⊢∅∈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∈W∧∅∈V→∅SubGraphG↔∅⊆Vtx⁡G∧∅=iEdg⁡G↾dom⁡∅∧∅⊆𝒫∅
20 8 19 mpan2 ⊢G∈W→∅SubGraphG↔∅⊆Vtx⁡G∧∅=iEdg⁡G↾dom⁡∅∧∅⊆𝒫∅
21 7 20 mpbiri ⊢G∈W→∅SubGraphG