This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐺 )