Theorem usgrausgri

Description: A simple graph represented by an alternatively defined simple graph. (Contributed by AV, 15-Oct-2020)

	Ref	Expression
Hypothesis	ausgr.1	$$⊢G=\left\{⟨v,e⟩|e\subseteq \left\{x\in 𝒫v|\left|x\right|=2\right\}\right\}$$
Assertion	usgrausgri	$$⊢H\in \mathrm{USGraph}\to \mathrm{Vtx}\left(H\right)G\mathrm{Edg}\left(H\right)$$

Proof

Step	Hyp	Ref	Expression
1		ausgr.1	$$⊢G=\left\{⟨v,e⟩|e\subseteq \left\{x\in 𝒫v|\left|x\right|=2\right\}\right\}$$
2		usgredgss	$$⊢H\in \mathrm{USGraph}\to \mathrm{Edg}\left(H\right)\subseteq \left\{x\in 𝒫\mathrm{Vtx}\left(H\right)|\left|x\right|=2\right\}$$
3		fvex	$$⊢\mathrm{Vtx}\left(H\right)\in \mathrm{V}$$
4		fvex	$$⊢\mathrm{Edg}\left(H\right)\in \mathrm{V}$$
5	1	isausgr	$$⊢\left(\mathrm{Vtx}\left(H\right)\in \mathrm{V}\wedge \mathrm{Edg}\left(H\right)\in \mathrm{V}\right)\to \left(\mathrm{Vtx}\left(H\right)G\mathrm{Edg}\left(H\right)\leftrightarrow \mathrm{Edg}\left(H\right)\subseteq \left\{x\in 𝒫\mathrm{Vtx}\left(H\right)|\left|x\right|=2\right\}\right)$$
6	3 4 5	mp2an	$$⊢\mathrm{Vtx}\left(H\right)G\mathrm{Edg}\left(H\right)\leftrightarrow \mathrm{Edg}\left(H\right)\subseteq \left\{x\in 𝒫\mathrm{Vtx}\left(H\right)|\left|x\right|=2\right\}$$
7	2 6	sylibr	$$⊢H\in \mathrm{USGraph}\to \mathrm{Vtx}\left(H\right)G\mathrm{Edg}\left(H\right)$$