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