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 )