Metamath Proof Explorer


Theorem nbgrcl

Description: If a class X has at least one neighbor, this class must be a vertex. (Contributed by AV, 6-Jun-2021) (Revised by AV, 12-Feb-2022)

Ref Expression
Hypothesis nbgrcl.v 𝑉 = ( Vtx ‘ 𝐺 )
Assertion nbgrcl ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝑋 ) → 𝑋𝑉 )

Proof

Step Hyp Ref Expression
1 nbgrcl.v 𝑉 = ( Vtx ‘ 𝐺 )
2 df-nbgr NeighbVtx = ( 𝑔 ∈ V , 𝑣 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑣 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } )
3 2 mpoxeldm ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝑋 ) → ( 𝐺 ∈ V ∧ 𝑋 𝐺 / 𝑔 ( Vtx ‘ 𝑔 ) ) )
4 csbfv 𝐺 / 𝑔 ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 )
5 4 1 eqtr4i 𝐺 / 𝑔 ( Vtx ‘ 𝑔 ) = 𝑉
6 5 eleq2i ( 𝑋 𝐺 / 𝑔 ( Vtx ‘ 𝑔 ) ↔ 𝑋𝑉 )
7 6 biimpi ( 𝑋 𝐺 / 𝑔 ( Vtx ‘ 𝑔 ) → 𝑋𝑉 )
8 3 7 simpl2im ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝑋 ) → 𝑋𝑉 )