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

Metamath Proof Explorer

Theorem nbgrval

Description: The set of neighbors of a vertex V in a graph G . (Contributed by Alexander van der Vekens, 7-Oct-2017) (Revised by AV, 24-Oct-2020) (Revised by AV, 21-Mar-2021)

Ref Expression
Hypotheses nbgrval.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
nbgrval.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion nbgrval ( 𝑁 ∈ 𝑉 → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } )

Proof

Step Hyp Ref Expression
1 nbgrval.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 nbgrval.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 df-nbgr ⊢ NeighbVtx = ( 𝑔 ∈ V , 𝑘 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑘 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑘 , 𝑛 } ⊆ 𝑒 } )
4 1 1vgrex ⊢ ( 𝑁 ∈ 𝑉 → 𝐺 ∈ V )
5 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
6 1 5 eqtr4id ⊢ ( 𝑔 = 𝐺 → 𝑉 = ( Vtx ‘ 𝑔 ) )
7 6 eleq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑁 ∈ 𝑉 ↔ 𝑁 ∈ ( Vtx ‘ 𝑔 ) ) )
8 7 biimpac ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑔 = 𝐺 ) → 𝑁 ∈ ( Vtx ‘ 𝑔 ) )
9 fvex ⊢ ( Vtx ‘ 𝑔 ) ∈ V
10 9 difexi ⊢ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑘 } ) ∈ V
11 rabexg ⊢ ( ( ( Vtx ‘ 𝑔 ) ∖ { 𝑘 } ) ∈ V → { 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑘 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑘 , 𝑛 } ⊆ 𝑒 } ∈ V )
12 10 11 mp1i ⊢ ( ( 𝑁 ∈ 𝑉 ∧ ( 𝑔 = 𝐺 ∧ 𝑘 = 𝑁 ) ) → { 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑘 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑘 , 𝑛 } ⊆ 𝑒 } ∈ V )
13 5 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = 𝑉 )
14 13 adantr ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑘 = 𝑁 ) → ( Vtx ‘ 𝑔 ) = 𝑉 )
15 sneq ⊢ ( 𝑘 = 𝑁 → { 𝑘 } = { 𝑁 } )
16 15 adantl ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑘 = 𝑁 ) → { 𝑘 } = { 𝑁 } )
17 14 16 difeq12d ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑘 = 𝑁 ) → ( ( Vtx ‘ 𝑔 ) ∖ { 𝑘 } ) = ( 𝑉 ∖ { 𝑁 } ) )
18 17 adantl ⊢ ( ( 𝑁 ∈ 𝑉 ∧ ( 𝑔 = 𝐺 ∧ 𝑘 = 𝑁 ) ) → ( ( Vtx ‘ 𝑔 ) ∖ { 𝑘 } ) = ( 𝑉 ∖ { 𝑁 } ) )
19 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Edg ‘ 𝑔 ) = ( Edg ‘ 𝐺 ) )
20 19 2 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Edg ‘ 𝑔 ) = 𝐸 )
21 20 adantr ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑘 = 𝑁 ) → ( Edg ‘ 𝑔 ) = 𝐸 )
22 21 adantl ⊢ ( ( 𝑁 ∈ 𝑉 ∧ ( 𝑔 = 𝐺 ∧ 𝑘 = 𝑁 ) ) → ( Edg ‘ 𝑔 ) = 𝐸 )
23 preq1 ⊢ ( 𝑘 = 𝑁 → { 𝑘 , 𝑛 } = { 𝑁 , 𝑛 } )
24 23 sseq1d ⊢ ( 𝑘 = 𝑁 → ( { 𝑘 , 𝑛 } ⊆ 𝑒 ↔ { 𝑁 , 𝑛 } ⊆ 𝑒 ) )
25 24 adantl ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑘 = 𝑁 ) → ( { 𝑘 , 𝑛 } ⊆ 𝑒 ↔ { 𝑁 , 𝑛 } ⊆ 𝑒 ) )
26 25 adantl ⊢ ( ( 𝑁 ∈ 𝑉 ∧ ( 𝑔 = 𝐺 ∧ 𝑘 = 𝑁 ) ) → ( { 𝑘 , 𝑛 } ⊆ 𝑒 ↔ { 𝑁 , 𝑛 } ⊆ 𝑒 ) )
27 22 26 rexeqbidv ⊢ ( ( 𝑁 ∈ 𝑉 ∧ ( 𝑔 = 𝐺 ∧ 𝑘 = 𝑁 ) ) → ( ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑘 , 𝑛 } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 ) )
28 18 27 rabeqbidv ⊢ ( ( 𝑁 ∈ 𝑉 ∧ ( 𝑔 = 𝐺 ∧ 𝑘 = 𝑁 ) ) → { 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑘 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑘 , 𝑛 } ⊆ 𝑒 } = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } )
29 4 8 12 28 ovmpodv2 ⊢ ( 𝑁 ∈ 𝑉 → ( NeighbVtx = ( 𝑔 ∈ V , 𝑘 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑘 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑘 , 𝑛 } ⊆ 𝑒 } ) → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } ) )
30 3 29 mpi ⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } )