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)

	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		opex	$$⊢⟨V,E⟩\in \mathrm{V}$$
6	3 5	eqeltri	$$⊢G\in \mathrm{V}$$
7		eqid	$$⊢\mathrm{Vtx}\left(G\right)=\mathrm{Vtx}\left(G\right)$$
8		eqid	$$⊢\mathrm{iEdg}\left(G\right)=\mathrm{iEdg}\left(G\right)$$
9	7 8	isusgrs	$$⊢G\in \mathrm{V}\to \left(G\in \mathrm{USGraph}\leftrightarrow \mathrm{iEdg}\left(G\right):\mathrm{dom}\mathrm{iEdg}\left(G\right)\underset{1-1}{⟶}\left\{e\in 𝒫\mathrm{Vtx}\left(G\right)|\left|e\right|=2\right\}\right)$$
10	1 2 3	usgrexmpllem	$$⊢\left(\mathrm{Vtx}\left(G\right)=V\wedge \mathrm{iEdg}\left(G\right)=E\right)$$
11		simpr	$$⊢\left(\mathrm{Vtx}\left(G\right)=V\wedge \mathrm{iEdg}\left(G\right)=E\right)\to \mathrm{iEdg}\left(G\right)=E$$
12	11	dmeqd	$$⊢\left(\mathrm{Vtx}\left(G\right)=V\wedge \mathrm{iEdg}\left(G\right)=E\right)\to \mathrm{dom}\mathrm{iEdg}\left(G\right)=\mathrm{dom}E$$
13		pweq	$$⊢\mathrm{Vtx}\left(G\right)=V\to 𝒫\mathrm{Vtx}\left(G\right)=𝒫V$$
14	13	adantr	$$⊢\left(\mathrm{Vtx}\left(G\right)=V\wedge \mathrm{iEdg}\left(G\right)=E\right)\to 𝒫\mathrm{Vtx}\left(G\right)=𝒫V$$
15	14	rabeqdv	$$⊢\left(\mathrm{Vtx}\left(G\right)=V\wedge \mathrm{iEdg}\left(G\right)=E\right)\to \left\{e\in 𝒫\mathrm{Vtx}\left(G\right)|\left|e\right|=2\right\}=\left\{e\in 𝒫V|\left|e\right|=2\right\}$$
16	11 12 15	f1eq123d	$$⊢\left(\mathrm{Vtx}\left(G\right)=V\wedge \mathrm{iEdg}\left(G\right)=E\right)\to \left(\mathrm{iEdg}\left(G\right):\mathrm{dom}\mathrm{iEdg}\left(G\right)\underset{1-1}{⟶}\left\{e\in 𝒫\mathrm{Vtx}\left(G\right)|\left|e\right|=2\right\}\leftrightarrow E:\mathrm{dom}E\underset{1-1}{⟶}\left\{e\in 𝒫V|\left|e\right|=2\right\}\right)$$
17	10 16	ax-mp	$$⊢\mathrm{iEdg}\left(G\right):\mathrm{dom}\mathrm{iEdg}\left(G\right)\underset{1-1}{⟶}\left\{e\in 𝒫\mathrm{Vtx}\left(G\right)|\left|e\right|=2\right\}\leftrightarrow E:\mathrm{dom}E\underset{1-1}{⟶}\left\{e\in 𝒫V|\left|e\right|=2\right\}$$
18	9 17	bitrdi	$$⊢G\in \mathrm{V}\to \left(G\in \mathrm{USGraph}\leftrightarrow E:\mathrm{dom}E\underset{1-1}{⟶}\left\{e\in 𝒫V|\left|e\right|=2\right\}\right)$$
19	6 18	ax-mp	$$⊢G\in \mathrm{USGraph}\leftrightarrow E:\mathrm{dom}E\underset{1-1}{⟶}\left\{e\in 𝒫V|\left|e\right|=2\right\}$$
20	4 19	mpbir	$$⊢G\in \mathrm{USGraph}$$