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 ( 𝐺𝑊 → ∅ SubGraph 𝐺 )

Proof

Step Hyp Ref Expression
1 0ss ∅ ⊆ ( Vtx ‘ 𝐺 )
2 dm0 dom ∅ = ∅
3 2 reseq2i ( ( iEdg ‘ 𝐺 ) ↾ dom ∅ ) = ( ( iEdg ‘ 𝐺 ) ↾ ∅ )
4 res0 ( ( iEdg ‘ 𝐺 ) ↾ ∅ ) = ∅
5 3 4 eqtr2i ∅ = ( ( iEdg ‘ 𝐺 ) ↾ dom ∅ )
6 0ss ∅ ⊆ 𝒫 ∅
7 1 5 6 3pm3.2i ( ∅ ⊆ ( Vtx ‘ 𝐺 ) ∧ ∅ = ( ( iEdg ‘ 𝐺 ) ↾ dom ∅ ) ∧ ∅ ⊆ 𝒫 ∅ )
8 0ex ∅ ∈ V
9 vtxval0 ( Vtx ‘ ∅ ) = ∅
10 9 eqcomi ∅ = ( Vtx ‘ ∅ )
11 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
12 iedgval0 ( iEdg ‘ ∅ ) = ∅
13 12 eqcomi ∅ = ( iEdg ‘ ∅ )
14 eqid ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
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 ( ( 𝐺𝑊 ∧ ∅ ∈ V ) → ( ∅ SubGraph 𝐺 ↔ ( ∅ ⊆ ( Vtx ‘ 𝐺 ) ∧ ∅ = ( ( iEdg ‘ 𝐺 ) ↾ dom ∅ ) ∧ ∅ ⊆ 𝒫 ∅ ) ) )
20 8 19 mpan2 ( 𝐺𝑊 → ( ∅ SubGraph 𝐺 ↔ ( ∅ ⊆ ( Vtx ‘ 𝐺 ) ∧ ∅ = ( ( iEdg ‘ 𝐺 ) ↾ dom ∅ ) ∧ ∅ ⊆ 𝒫 ∅ ) ) )
21 7 20 mpbiri ( 𝐺𝑊 → ∅ SubGraph 𝐺 )