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 syl5eq ( 𝐺 ∈ USGraph → ( UnivVtx ‘ 𝐺 ) = { 𝑛𝑉 ∣ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑛 } ) { 𝑘 , 𝑛 } ∈ 𝐸 } )