Theorem usgr0e

Description: The empty graph, with vertices but no edges, is a simple graph. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 16-Oct-2020) (Proof shortened by AV, 25-Nov-2020)

	Ref	Expression
Hypotheses	usgr0e.g	$$⊢\phi \to G\in W$$
	usgr0e.e	$$⊢\phi \to \mathrm{iEdg}\left(G\right)=\varnothing$$
Assertion	usgr0e	$$⊢\phi \to G\in \mathrm{USGraph}$$

Proof

Step	Hyp	Ref	Expression
1		usgr0e.g	$$⊢\phi \to G\in W$$
2		usgr0e.e	$$⊢\phi \to \mathrm{iEdg}\left(G\right)=\varnothing$$
3	2	f10d	$$⊢\phi \to \mathrm{iEdg}\left(G\right):\mathrm{dom}\mathrm{iEdg}\left(G\right)\underset{1-1}{⟶}\left\{x\in \left(𝒫\mathrm{Vtx}\left(G\right)\setminus \left\{\varnothing \right\}\right)|\left|x\right|=2\right\}$$
4		eqid	$$⊢\mathrm{Vtx}\left(G\right)=\mathrm{Vtx}\left(G\right)$$
5		eqid	$$⊢\mathrm{iEdg}\left(G\right)=\mathrm{iEdg}\left(G\right)$$
6	4 5	isusgr	$$⊢G\in W\to \left(G\in \mathrm{USGraph}\leftrightarrow \mathrm{iEdg}\left(G\right):\mathrm{dom}\mathrm{iEdg}\left(G\right)\underset{1-1}{⟶}\left\{x\in \left(𝒫\mathrm{Vtx}\left(G\right)\setminus \left\{\varnothing \right\}\right)|\left|x\right|=2\right\}\right)$$
7	1 6	syl	$$⊢\phi \to \left(G\in \mathrm{USGraph}\leftrightarrow \mathrm{iEdg}\left(G\right):\mathrm{dom}\mathrm{iEdg}\left(G\right)\underset{1-1}{⟶}\left\{x\in \left(𝒫\mathrm{Vtx}\left(G\right)\setminus \left\{\varnothing \right\}\right)|\left|x\right|=2\right\}\right)$$
8	3 7	mpbird	$$⊢\phi \to G\in \mathrm{USGraph}$$