Theorem cusgrexg

Description: For each set there is a set of edges so that the set together with these edges is a complete simple graph. (Contributed by Alexander van der Vekens, 12-Jan-2018) (Revised by AV, 5-Nov-2020)

	Ref	Expression
Assertion	cusgrexg	$$⊢V\in W\to \exists e⟨V,e⟩\in \mathrm{ComplUSGraph}$$

Proof

Step	Hyp	Ref	Expression
1		fveqeq2	$$⊢y=x\to \left(\left|y\right|=2\leftrightarrow \left|x\right|=2\right)$$
2	1	cbvrabv	$$⊢\left\{y\in 𝒫V|\left|y\right|=2\right\}=\left\{x\in 𝒫V|\left|x\right|=2\right\}$$
3	2	cusgrexilem1	$$⊢V\in W\to {\mathrm{I}\upharpoonright }_{\left\{y\in 𝒫V|\left|y\right|=2\right\}}\in \mathrm{V}$$
4	2	cusgrexi	$$⊢V\in W\to ⟨V,{\mathrm{I}\upharpoonright }_{\left\{y\in 𝒫V|\left|y\right|=2\right\}}⟩\in \mathrm{ComplUSGraph}$$
5		opeq2	$$⊢e={\mathrm{I}\upharpoonright }_{\left\{y\in 𝒫V|\left|y\right|=2\right\}}\to ⟨V,e⟩=⟨V,{\mathrm{I}\upharpoonright }_{\left\{y\in 𝒫V|\left|y\right|=2\right\}}⟩$$
6	5	eleq1d	$$⊢e={\mathrm{I}\upharpoonright }_{\left\{y\in 𝒫V|\left|y\right|=2\right\}}\to \left(⟨V,e⟩\in \mathrm{ComplUSGraph}\leftrightarrow ⟨V,{\mathrm{I}\upharpoonright }_{\left\{y\in 𝒫V|\left|y\right|=2\right\}}⟩\in \mathrm{ComplUSGraph}\right)$$
7	3 4 6	spcedv	$$⊢V\in W\to \exists e⟨V,e⟩\in \mathrm{ComplUSGraph}$$