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

Metamath Proof Explorer

Theorem uvtxusgr

Description: The set of all universal vertices of a simple graph. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 31-Oct-2020)

Ref Expression
Hypotheses uvtxnbgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
uvtxusgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion uvtxusgr ( 𝐺 ∈ USGraph → ( UnivVtx ‘ 𝐺 ) = { 𝑛 ∈ 𝑉 ∣ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑛 } ) { 𝑘 , 𝑛 } ∈ 𝐸 } )

Proof

Step Hyp Ref Expression
1 uvtxnbgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 uvtxusgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 uvtxval ⊢ ( UnivVtx ‘ 𝐺 ) = { 𝑛 ∈ 𝑉 ∣ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑛 } ) 𝑘 ∈ ( 𝐺 NeighbVtx 𝑛 ) }
4 2 nbusgreledg ⊢ ( 𝐺 ∈ USGraph → ( 𝑘 ∈ ( 𝐺 NeighbVtx 𝑛 ) ↔ { 𝑘 , 𝑛 } ∈ 𝐸 ) )
5 4 ralbidv ⊢ ( 𝐺 ∈ USGraph → ( ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑛 } ) 𝑘 ∈ ( 𝐺 NeighbVtx 𝑛 ) ↔ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑛 } ) { 𝑘 , 𝑛 } ∈ 𝐸 ) )
6 5 rabbidv ⊢ ( 𝐺 ∈ USGraph → { 𝑛 ∈ 𝑉 ∣ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑛 } ) 𝑘 ∈ ( 𝐺 NeighbVtx 𝑛 ) } = { 𝑛 ∈ 𝑉 ∣ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑛 } ) { 𝑘 , 𝑛 } ∈ 𝐸 } )
7 3 6 eqtrid ⊢ ( 𝐺 ∈ USGraph → ( UnivVtx ‘ 𝐺 ) = { 𝑛 ∈ 𝑉 ∣ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑛 } ) { 𝑘 , 𝑛 } ∈ 𝐸 } )