This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ComplUSGraph$

Proof

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