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	⊢ ( 𝑉 ∈ 𝑊 → ∃ 𝑒 ⟨ 𝑉 , 𝑒 ⟩ ∈ ComplUSGraph )

Proof

Step	Hyp	Ref	Expression
1		fveqeq2	⊢ ( 𝑦 = 𝑥 → ( ( ♯ ‘ 𝑦 ) = 2 ↔ ( ♯ ‘ 𝑥 ) = 2 ) )
2	1	cbvrabv	⊢ { 𝑦 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑦 ) = 2 } = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 }
3	2	cusgrexilem1	⊢ ( 𝑉 ∈ 𝑊 → ( I ↾ { 𝑦 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑦 ) = 2 } ) ∈ V )
4	2	cusgrexi	⊢ ( 𝑉 ∈ 𝑊 → ⟨ 𝑉 , ( I ↾ { 𝑦 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑦 ) = 2 } ) ⟩ ∈ ComplUSGraph )
5		opeq2	⊢ ( 𝑒 = ( I ↾ { 𝑦 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑦 ) = 2 } ) → ⟨ 𝑉 , 𝑒 ⟩ = ⟨ 𝑉 , ( I ↾ { 𝑦 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑦 ) = 2 } ) ⟩ )
6	5	eleq1d	⊢ ( 𝑒 = ( I ↾ { 𝑦 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑦 ) = 2 } ) → ( ⟨ 𝑉 , 𝑒 ⟩ ∈ ComplUSGraph ↔ ⟨ 𝑉 , ( I ↾ { 𝑦 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑦 ) = 2 } ) ⟩ ∈ ComplUSGraph ) )
7	3 4 6	spcedv	⊢ ( 𝑉 ∈ 𝑊 → ∃ 𝑒 ⟨ 𝑉 , 𝑒 ⟩ ∈ ComplUSGraph )