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

Metamath Proof Explorer

Theorem uvtxusgrel

Description: A universal vertex, i.e. an element of 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 uvtxusgrel ( 𝐺 ∈ USGraph → ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ( 𝑁 ∈ 𝑉 ∧ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑘 , 𝑁 } ∈ 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 uvtxnbgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 uvtxusgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 uvtxusgr ⊢ ( 𝐺 ∈ USGraph → ( UnivVtx ‘ 𝐺 ) = { 𝑣 ∈ 𝑉 ∣ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑘 , 𝑣 } ∈ 𝐸 } )
4 3 eleq2d ⊢ ( 𝐺 ∈ USGraph → ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) ↔ 𝑁 ∈ { 𝑣 ∈ 𝑉 ∣ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑘 , 𝑣 } ∈ 𝐸 } ) )
5 sneq ⊢ ( 𝑣 = 𝑁 → { 𝑣 } = { 𝑁 } )
6 5 difeq2d ⊢ ( 𝑣 = 𝑁 → ( 𝑉 ∖ { 𝑣 } ) = ( 𝑉 ∖ { 𝑁 } ) )
7 preq2 ⊢ ( 𝑣 = 𝑁 → { 𝑘 , 𝑣 } = { 𝑘 , 𝑁 } )
8 7 eleq1d ⊢ ( 𝑣 = 𝑁 → ( { 𝑘 , 𝑣 } ∈ 𝐸 ↔ { 𝑘 , 𝑁 } ∈ 𝐸 ) )
9 6 8 raleqbidv ⊢ ( 𝑣 = 𝑁 → ( ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑘 , 𝑣 } ∈ 𝐸 ↔ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑘 , 𝑁 } ∈ 𝐸 ) )
10 9 elrab ⊢ ( 𝑁 ∈ { 𝑣 ∈ 𝑉 ∣ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑘 , 𝑣 } ∈ 𝐸 } ↔ ( 𝑁 ∈ 𝑉 ∧ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑘 , 𝑁 } ∈ 𝐸 ) )
11 4 10 bitrdi ⊢ ( 𝐺 ∈ USGraph → ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ( 𝑁 ∈ 𝑉 ∧ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑁 } ) { 𝑘 , 𝑁 } ∈ 𝐸 ) ) )