Theorem usgrexi

Description: An arbitrary set regarded as vertices together with the set of pairs of elements of this set regarded as edges is a simple graph. (Contributed by Alexander van der Vekens, 12-Jan-2018) (Revised by AV, 5-Nov-2020) (Proof shortened by AV, 10-Nov-2021)

	Ref	Expression
Hypothesis	usgrexi.p	$$⊢P=\left\{x\in 𝒫V|\left|x\right|=2\right\}$$
Assertion	usgrexi	$$⊢V\in W\to ⟨V,{\mathrm{I}\upharpoonright }_P⟩\in \mathrm{USGraph}$$

Proof

Step	Hyp	Ref	Expression
1		usgrexi.p	$$⊢P=\left\{x\in 𝒫V|\left|x\right|=2\right\}$$
2	1	usgrexilem	$$⊢V\in W\to \left({\mathrm{I}\upharpoonright }_P\right):\mathrm{dom}\left({\mathrm{I}\upharpoonright }_P\right)\underset{1-1}{⟶}\left\{x\in 𝒫V|\left|x\right|=2\right\}$$
3	1	cusgrexilem1	$$⊢V\in W\to {\mathrm{I}\upharpoonright }_P\in \mathrm{V}$$
4		opiedgfv	$$⊢\left(V\in W\wedge {\mathrm{I}\upharpoonright }_P\in \mathrm{V}\right)\to \mathrm{iEdg}\left(⟨V,{\mathrm{I}\upharpoonright }_P⟩\right)={\mathrm{I}\upharpoonright }_P$$
5	3 4	mpdan	$$⊢V\in W\to \mathrm{iEdg}\left(⟨V,{\mathrm{I}\upharpoonright }_P⟩\right)={\mathrm{I}\upharpoonright }_P$$
6	5	dmeqd	$$⊢V\in W\to \mathrm{dom}\mathrm{iEdg}\left(⟨V,{\mathrm{I}\upharpoonright }_P⟩\right)=\mathrm{dom}\left({\mathrm{I}\upharpoonright }_P\right)$$
7		opvtxfv	$$⊢\left(V\in W\wedge {\mathrm{I}\upharpoonright }_P\in \mathrm{V}\right)\to \mathrm{Vtx}\left(⟨V,{\mathrm{I}\upharpoonright }_P⟩\right)=V$$
8	3 7	mpdan	$$⊢V\in W\to \mathrm{Vtx}\left(⟨V,{\mathrm{I}\upharpoonright }_P⟩\right)=V$$
9	8	pweqd	$$⊢V\in W\to 𝒫\mathrm{Vtx}\left(⟨V,{\mathrm{I}\upharpoonright }_P⟩\right)=𝒫V$$
10	9	rabeqdv	$$⊢V\in W\to \left\{x\in 𝒫\mathrm{Vtx}\left(⟨V,{\mathrm{I}\upharpoonright }_P⟩\right)|\left|x\right|=2\right\}=\left\{x\in 𝒫V|\left|x\right|=2\right\}$$
11	5 6 10	f1eq123d	$$⊢V\in W\to \left(\mathrm{iEdg}\left(⟨V,{\mathrm{I}\upharpoonright }_P⟩\right):\mathrm{dom}\mathrm{iEdg}\left(⟨V,{\mathrm{I}\upharpoonright }_P⟩\right)\underset{1-1}{⟶}\left\{x\in 𝒫\mathrm{Vtx}\left(⟨V,{\mathrm{I}\upharpoonright }_P⟩\right)|\left|x\right|=2\right\}\leftrightarrow \left({\mathrm{I}\upharpoonright }_P\right):\mathrm{dom}\left({\mathrm{I}\upharpoonright }_P\right)\underset{1-1}{⟶}\left\{x\in 𝒫V|\left|x\right|=2\right\}\right)$$
12	2 11	mpbird	$$⊢V\in W\to \mathrm{iEdg}\left(⟨V,{\mathrm{I}\upharpoonright }_P⟩\right):\mathrm{dom}\mathrm{iEdg}\left(⟨V,{\mathrm{I}\upharpoonright }_P⟩\right)\underset{1-1}{⟶}\left\{x\in 𝒫\mathrm{Vtx}\left(⟨V,{\mathrm{I}\upharpoonright }_P⟩\right)|\left|x\right|=2\right\}$$
13		opex	$$⊢⟨V,{\mathrm{I}\upharpoonright }_P⟩\in \mathrm{V}$$
14		eqid	$$⊢\mathrm{Vtx}\left(⟨V,{\mathrm{I}\upharpoonright }_P⟩\right)=\mathrm{Vtx}\left(⟨V,{\mathrm{I}\upharpoonright }_P⟩\right)$$
15		eqid	$$⊢\mathrm{iEdg}\left(⟨V,{\mathrm{I}\upharpoonright }_P⟩\right)=\mathrm{iEdg}\left(⟨V,{\mathrm{I}\upharpoonright }_P⟩\right)$$
16	14 15	isusgrs	$$⊢⟨V,{\mathrm{I}\upharpoonright }_P⟩\in \mathrm{V}\to \left(⟨V,{\mathrm{I}\upharpoonright }_P⟩\in \mathrm{USGraph}\leftrightarrow \mathrm{iEdg}\left(⟨V,{\mathrm{I}\upharpoonright }_P⟩\right):\mathrm{dom}\mathrm{iEdg}\left(⟨V,{\mathrm{I}\upharpoonright }_P⟩\right)\underset{1-1}{⟶}\left\{x\in 𝒫\mathrm{Vtx}\left(⟨V,{\mathrm{I}\upharpoonright }_P⟩\right)|\left|x\right|=2\right\}\right)$$
17	13 16	mp1i	$$⊢V\in W\to \left(⟨V,{\mathrm{I}\upharpoonright }_P⟩\in \mathrm{USGraph}\leftrightarrow \mathrm{iEdg}\left(⟨V,{\mathrm{I}\upharpoonright }_P⟩\right):\mathrm{dom}\mathrm{iEdg}\left(⟨V,{\mathrm{I}\upharpoonright }_P⟩\right)\underset{1-1}{⟶}\left\{x\in 𝒫\mathrm{Vtx}\left(⟨V,{\mathrm{I}\upharpoonright }_P⟩\right)|\left|x\right|=2\right\}\right)$$
18	12 17	mpbird	$$⊢V\in W\to ⟨V,{\mathrm{I}\upharpoonright }_P⟩\in \mathrm{USGraph}$$