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 𝑋 ) → 𝑋 ∈ 𝑉 ) |
| 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 𝑋 ) → 𝑋 ∈ 𝑉 ) |