Theorem usgrexmpl

Description: G is a simple graph of five vertices 0 , 1 , 2 , 3 , 4 , with edges { 0 , 1 } , { 1 , 2 } , { 2 , 0 } , { 0 , 3 } . (Contributed by Alexander van der Vekens, 15-Aug-2017) (Revised by AV, 21-Oct-2020) (Proof shortened by AV, 7-Aug-2025)

	Ref	Expression
Hypotheses	usgrexmpl.v	$$⊢V=\left(0\dots 4\right)$$
	usgrexmpl.e	$$⊢E=⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,0\right\}\left\{0,3\right\}”⟩$$
	usgrexmpl.g	$$⊢G=⟨V,E⟩$$
Assertion	usgrexmpl	$$⊢G\in \mathrm{USGraph}$$

Proof

Step	Hyp	Ref	Expression
1		usgrexmpl.v	$$⊢V=\left(0\dots 4\right)$$
2		usgrexmpl.e	$$⊢E=⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,0\right\}\left\{0,3\right\}”⟩$$
3		usgrexmpl.g	$$⊢G=⟨V,E⟩$$
4	1 2	usgrexmplef	$$⊢E:\mathrm{dom}E\underset{1-1}{⟶}\left\{e\in 𝒫V|\left|e\right|=2\right\}$$
5	3	eleq1i	$$⊢G\in \mathrm{USGraph}\leftrightarrow ⟨V,E⟩\in \mathrm{USGraph}$$
6	1	ovexi	$$⊢V\in \mathrm{V}$$
7		s4cli	$$⊢⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,0\right\}\left\{0,3\right\}”⟩\in \mathrm{Word}\mathrm{V}$$
8	2 7	eqeltri	$$⊢E\in \mathrm{Word}\mathrm{V}$$
9		isusgrop	$$⊢\left(V\in \mathrm{V}\wedge E\in \mathrm{Word}\mathrm{V}\right)\to \left(⟨V,E⟩\in \mathrm{USGraph}\leftrightarrow E:\mathrm{dom}E\underset{1-1}{⟶}\left\{e\in 𝒫V|\left|e\right|=2\right\}\right)$$
10	6 8 9	mp2an	$$⊢⟨V,E⟩\in \mathrm{USGraph}\leftrightarrow E:\mathrm{dom}E\underset{1-1}{⟶}\left\{e\in 𝒫V|\left|e\right|=2\right\}$$
11	5 10	bitri	$$⊢G\in \mathrm{USGraph}\leftrightarrow E:\mathrm{dom}E\underset{1-1}{⟶}\left\{e\in 𝒫V|\left|e\right|=2\right\}$$
12	4 11	mpbir	$$⊢G\in \mathrm{USGraph}$$