Metamath Proof Explorer

Theorem clnbgrval

Description: The closed neighborhood of a vertex V in a graph G . (Contributed by AV, 7-May-2025)

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

Proof

Step Hyp Ref Expression
1 clnbgrval.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 clnbgrval.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 df-clnbgr ⊢ ClNeighbVtx = ( 𝑔 ∈ V , 𝑣 ∈ ( Vtx ‘ 𝑔 ) ↦ ( { 𝑣 } ∪ { 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } ) )
4 1 1vgrex ⊢ ( 𝑁 ∈ 𝑉 → 𝐺 ∈ V )
5 fveq2 ⊢ ( 𝐺 = 𝑔 → ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝑔 ) )
6 5 eqcoms ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝑔 ) )
7 1 6 eqtrid ⊢ ( 𝑔 = 𝐺 → 𝑉 = ( Vtx ‘ 𝑔 ) )
8 7 eleq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑁 ∈ 𝑉 ↔ 𝑁 ∈ ( Vtx ‘ 𝑔 ) ) )
9 8 biimpac ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑔 = 𝐺 ) → 𝑁 ∈ ( Vtx ‘ 𝑔 ) )
10 vsnex ⊢ { 𝑣 } ∈ V
11 10 a1i ⊢ ( ( 𝑁 ∈ 𝑉 ∧ ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑁 ) ) → { 𝑣 } ∈ V )
12 fvex ⊢ ( Vtx ‘ 𝑔 ) ∈ V
13 rabexg ⊢ ( ( Vtx ‘ 𝑔 ) ∈ V → { 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } ∈ V )
14 12 13 mp1i ⊢ ( ( 𝑁 ∈ 𝑉 ∧ ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑁 ) ) → { 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } ∈ V )
15 11 14 unexd ⊢ ( ( 𝑁 ∈ 𝑉 ∧ ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑁 ) ) → ( { 𝑣 } ∪ { 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } ) ∈ V )
16 sneq ⊢ ( 𝑣 = 𝑁 → { 𝑣 } = { 𝑁 } )
17 16 adantl ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑁 ) → { 𝑣 } = { 𝑁 } )
18 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
19 18 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = 𝑉 )
20 19 adantr ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑁 ) → ( Vtx ‘ 𝑔 ) = 𝑉 )
21 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Edg ‘ 𝑔 ) = ( Edg ‘ 𝐺 ) )
22 21 2 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Edg ‘ 𝑔 ) = 𝐸 )
23 22 adantr ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑁 ) → ( Edg ‘ 𝑔 ) = 𝐸 )
24 preq1 ⊢ ( 𝑣 = 𝑁 → { 𝑣 , 𝑛 } = { 𝑁 , 𝑛 } )
25 24 sseq1d ⊢ ( 𝑣 = 𝑁 → ( { 𝑣 , 𝑛 } ⊆ 𝑒 ↔ { 𝑁 , 𝑛 } ⊆ 𝑒 ) )
26 25 adantl ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑁 ) → ( { 𝑣 , 𝑛 } ⊆ 𝑒 ↔ { 𝑁 , 𝑛 } ⊆ 𝑒 ) )
27 23 26 rexeqbidv ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑁 ) → ( ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 ) )
28 20 27 rabeqbidv ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑁 ) → { 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } = { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } )
29 17 28 uneq12d ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑁 ) → ( { 𝑣 } ∪ { 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } ) )
30 29 adantl ⊢ ( ( 𝑁 ∈ 𝑉 ∧ ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑁 ) ) → ( { 𝑣 } ∪ { 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } ) )
31 4 9 15 30 ovmpodv2 ⊢ ( 𝑁 ∈ 𝑉 → ( ClNeighbVtx = ( 𝑔 ∈ V , 𝑣 ∈ ( Vtx ‘ 𝑔 ) ↦ ( { 𝑣 } ∪ { 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } ) ) → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } ) ) )
32 3 31 mpi ⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } ) )