Theorem usgrexmpl1

Description: G is a simple graph of six vertices 0 , 1 , 2 , 3 , 4 , 5 , with edges { 0 , 1 } , { 1 , 2 } , { 0 , 2 } , { 0 , 3 } , { 3 , 4 } , { 3 , 5 } , { 4 , 5 } . (Contributed by AV, 3-Aug-2025)

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

Proof

Step	Hyp	Ref	Expression
1		usgrexmpl1.v	$$⊢V=\left(0\dots 5\right)$$
2		usgrexmpl1.e	$$⊢E=⟨“\left\{0,1\right\}\left\{0,2\right\}\left\{1,2\right\}\left\{0,3\right\}\left\{3,4\right\}\left\{3,5\right\}\left\{4,5\right\}”⟩$$
3		usgrexmpl1.g	$$⊢G=⟨V,E⟩$$
4	1 2	usgrexmpl1lem	$$⊢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		s7cli	$$⊢⟨“\left\{0,1\right\}\left\{0,2\right\}\left\{1,2\right\}\left\{0,3\right\}\left\{3,4\right\}\left\{3,5\right\}\left\{4,5\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}$$