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

Metamath Proof Explorer

Theorem nbgrnself

Description: A vertex in a graph is not a neighbor of itself. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 3-Nov-2020) (Revised by AV, 21-Mar-2021)

Ref Expression
Hypothesis nbgrnself.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion nbgrnself ∀ 𝑣 ∈ 𝑉 𝑣 ∉ ( 𝐺 NeighbVtx 𝑣 )

Proof

Step Hyp Ref Expression
1 nbgrnself.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 neldifsnd ⊢ ( 𝑣 ∈ 𝑉 → ¬ 𝑣 ∈ ( 𝑉 ∖ { 𝑣 } ) )
3 2 intnanrd ⊢ ( 𝑣 ∈ 𝑉 → ¬ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑣 } ) ∧ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑣 } ⊆ 𝑒 ) )
4 df-nel ⊢ ( 𝑣 ∉ { 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } ↔ ¬ 𝑣 ∈ { 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } )
5 preq2 ⊢ ( 𝑛 = 𝑣 → { 𝑣 , 𝑛 } = { 𝑣 , 𝑣 } )
6 5 sseq1d ⊢ ( 𝑛 = 𝑣 → ( { 𝑣 , 𝑛 } ⊆ 𝑒 ↔ { 𝑣 , 𝑣 } ⊆ 𝑒 ) )
7 6 rexbidv ⊢ ( 𝑛 = 𝑣 → ( ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑣 } ⊆ 𝑒 ) )
8 7 elrab ⊢ ( 𝑣 ∈ { 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } ↔ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑣 } ) ∧ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑣 } ⊆ 𝑒 ) )
9 4 8 xchbinx ⊢ ( 𝑣 ∉ { 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } ↔ ¬ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑣 } ) ∧ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑣 } ⊆ 𝑒 ) )
10 3 9 sylibr ⊢ ( 𝑣 ∈ 𝑉 → 𝑣 ∉ { 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } )
11 eqidd ⊢ ( 𝑣 ∈ 𝑉 → 𝑣 = 𝑣 )
12 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
13 1 12 nbgrval ⊢ ( 𝑣 ∈ 𝑉 → ( 𝐺 NeighbVtx 𝑣 ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } )
14 11 13 neleq12d ⊢ ( 𝑣 ∈ 𝑉 → ( 𝑣 ∉ ( 𝐺 NeighbVtx 𝑣 ) ↔ 𝑣 ∉ { 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } ) )
15 10 14 mpbird ⊢ ( 𝑣 ∈ 𝑉 → 𝑣 ∉ ( 𝐺 NeighbVtx 𝑣 ) )
16 15 rgen ⊢ ∀ 𝑣 ∈ 𝑉 𝑣 ∉ ( 𝐺 NeighbVtx 𝑣 )