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