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 → ∅ SubGraph G

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 → ∅ SubGraph G ↔ ∅ ⊆ Vtx ⁡ G ∧ ∅ = iEdg ⁡ G ↾ dom ⁡ ∅ ∧ ∅ ⊆ 𝒫 ∅
20 8 19 mpan2 ⊢ G ∈ W → ∅ SubGraph G ↔ ∅ ⊆ Vtx ⁡ G ∧ ∅ = iEdg ⁡ G ↾ dom ⁡ ∅ ∧ ∅ ⊆ 𝒫 ∅
21 7 20 mpbiri ⊢ G ∈ W → ∅ SubGraph G