Theorem isusgrs

Description: The property of being a simple graph, simplified version of isusgr . (Contributed by Alexander van der Vekens, 13-Aug-2017) (Revised by AV, 13-Oct-2020) (Proof shortened by AV, 24-Nov-2020)

	Ref	Expression
Hypotheses	isuspgr.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	isuspgr.e	$$⊢E=\mathrm{iEdg}\left(G\right)$$
Assertion	isusgrs	$$⊢G\in U\to \left(G\in \mathrm{USGraph}\leftrightarrow E:\mathrm{dom}E\underset{1-1}{⟶}\left\{x\in 𝒫V|\left|x\right|=2\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		isuspgr.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		isuspgr.e	$$⊢E=\mathrm{iEdg}\left(G\right)$$
3	1 2	isusgr	$$⊢G\in U\to \left(G\in \mathrm{USGraph}\leftrightarrow E:\mathrm{dom}E\underset{1-1}{⟶}\left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|=2\right\}\right)$$
4		prprrab	$$⊢\left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|=2\right\}=\left\{x\in 𝒫V|\left|x\right|=2\right\}$$
5		f1eq3	$$⊢\left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|=2\right\}=\left\{x\in 𝒫V|\left|x\right|=2\right\}\to \left(E:\mathrm{dom}E\underset{1-1}{⟶}\left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|=2\right\}\leftrightarrow E:\mathrm{dom}E\underset{1-1}{⟶}\left\{x\in 𝒫V|\left|x\right|=2\right\}\right)$$
6	4 5	mp1i	$$⊢G\in U\to \left(E:\mathrm{dom}E\underset{1-1}{⟶}\left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|=2\right\}\leftrightarrow E:\mathrm{dom}E\underset{1-1}{⟶}\left\{x\in 𝒫V|\left|x\right|=2\right\}\right)$$
7	3 6	bitrd	$$⊢G\in U\to \left(G\in \mathrm{USGraph}\leftrightarrow E:\mathrm{dom}E\underset{1-1}{⟶}\left\{x\in 𝒫V|\left|x\right|=2\right\}\right)$$