Metamath Proof Explorer

Theorem dfnbgr6

Description: Alternate definition of the (open) neighborhood of a vertex as a difference of its semiopen neighborhood and the singleton of itself. (Contributed by AV, 17-May-2025)

Ref Expression
Hypotheses dfvopnbgr2.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
dfvopnbgr2.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
dfvopnbgr2.u ⊢ 𝑈 = { 𝑛 ∈ 𝑉 ∣ ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑁 ) ∨ ∃ 𝑒 ∈ 𝐸 ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ) }
Assertion dfnbgr6 ( 𝑁 ∈ 𝑉 → ( 𝐺 NeighbVtx 𝑁 ) = ( 𝑈 ∖ { 𝑁 } ) )

Proof

Step Hyp Ref Expression
1 dfvopnbgr2.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 dfvopnbgr2.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 dfvopnbgr2.u ⊢ 𝑈 = { 𝑛 ∈ 𝑉 ∣ ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑁 ) ∨ ∃ 𝑒 ∈ 𝐸 ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ) }
4 rabdif ⊢ ( { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ∖ { 𝑁 } ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) }
5 3anass ⊢ ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ↔ ( 𝑣 ≠ 𝑁 ∧ ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) )
6 5 biimpri ⊢ ( ( 𝑣 ≠ 𝑁 ∧ ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) → ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) )
7 6 orcd ⊢ ( ( 𝑣 ≠ 𝑁 ∧ ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) → ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) )
8 7 ex ⊢ ( 𝑣 ≠ 𝑁 → ( ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) → ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) )
9 3simpc ⊢ ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) → ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) )
10 9 a1i ⊢ ( 𝑣 ≠ 𝑁 → ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) → ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) )
11 eqneqall ⊢ ( 𝑣 = 𝑁 → ( 𝑣 ≠ 𝑁 → ( 𝑒 = { 𝑣 } → ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) ) )
12 11 com12 ⊢ ( 𝑣 ≠ 𝑁 → ( 𝑣 = 𝑁 → ( 𝑒 = { 𝑣 } → ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) ) )
13 12 impd ⊢ ( 𝑣 ≠ 𝑁 → ( ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) → ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) )
14 10 13 jaod ⊢ ( 𝑣 ≠ 𝑁 → ( ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) → ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) )
15 8 14 impbid ⊢ ( 𝑣 ≠ 𝑁 → ( ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ↔ ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) )
16 15 rexbidv ⊢ ( 𝑣 ≠ 𝑁 → ( ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ↔ ∃ 𝑒 ∈ 𝐸 ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) )
17 16 anbi2d ⊢ ( 𝑣 ≠ 𝑁 → ( ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) ↔ ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) ) )
18 17 pm5.32ri ⊢ ( ( ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) ∧ 𝑣 ≠ 𝑁 ) ↔ ( ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) ∧ 𝑣 ≠ 𝑁 ) )
19 18 a1i ⊢ ( 𝑁 ∈ 𝑉 → ( ( ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) ∧ 𝑣 ≠ 𝑁 ) ↔ ( ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) ∧ 𝑣 ≠ 𝑁 ) ) )
20 eldif ⊢ ( 𝑣 ∈ ( { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ∖ { 𝑁 } ) ↔ ( 𝑣 ∈ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ∧ ¬ 𝑣 ∈ { 𝑁 } ) )
21 elequ1 ⊢ ( 𝑛 = 𝑣 → ( 𝑛 ∈ 𝑒 ↔ 𝑣 ∈ 𝑒 ) )
22 21 anbi2d ⊢ ( 𝑛 = 𝑣 → ( ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ↔ ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) )
23 22 rexbidv ⊢ ( 𝑛 = 𝑣 → ( ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ↔ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) )
24 23 elrab ⊢ ( 𝑣 ∈ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ↔ ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) )
25 velsn ⊢ ( 𝑣 ∈ { 𝑁 } ↔ 𝑣 = 𝑁 )
26 25 necon3bbii ⊢ ( ¬ 𝑣 ∈ { 𝑁 } ↔ 𝑣 ≠ 𝑁 )
27 24 26 anbi12i ⊢ ( ( 𝑣 ∈ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ∧ ¬ 𝑣 ∈ { 𝑁 } ) ↔ ( ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) ∧ 𝑣 ≠ 𝑁 ) )
28 20 27 bitri ⊢ ( 𝑣 ∈ ( { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ∖ { 𝑁 } ) ↔ ( ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) ∧ 𝑣 ≠ 𝑁 ) )
29 eldif ⊢ ( 𝑣 ∈ ( { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) } ∖ { 𝑁 } ) ↔ ( 𝑣 ∈ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) } ∧ ¬ 𝑣 ∈ { 𝑁 } ) )
30 neeq1 ⊢ ( 𝑛 = 𝑣 → ( 𝑛 ≠ 𝑁 ↔ 𝑣 ≠ 𝑁 ) )
31 30 21 3anbi13d ⊢ ( 𝑛 = 𝑣 → ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ↔ ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) )
32 eqeq1 ⊢ ( 𝑛 = 𝑣 → ( 𝑛 = 𝑁 ↔ 𝑣 = 𝑁 ) )
33 sneq ⊢ ( 𝑛 = 𝑣 → { 𝑛 } = { 𝑣 } )
34 33 eqeq2d ⊢ ( 𝑛 = 𝑣 → ( 𝑒 = { 𝑛 } ↔ 𝑒 = { 𝑣 } ) )
35 32 34 anbi12d ⊢ ( 𝑛 = 𝑣 → ( ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ↔ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) )
36 31 35 orbi12d ⊢ ( 𝑛 = 𝑣 → ( ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) ↔ ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) )
37 36 rexbidv ⊢ ( 𝑛 = 𝑣 → ( ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) ↔ ∃ 𝑒 ∈ 𝐸 ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) )
38 37 elrab ⊢ ( 𝑣 ∈ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) } ↔ ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) )
39 38 26 anbi12i ⊢ ( ( 𝑣 ∈ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) } ∧ ¬ 𝑣 ∈ { 𝑁 } ) ↔ ( ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) ∧ 𝑣 ≠ 𝑁 ) )
40 29 39 bitri ⊢ ( 𝑣 ∈ ( { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) } ∖ { 𝑁 } ) ↔ ( ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) ∧ 𝑣 ≠ 𝑁 ) )
41 19 28 40 3bitr4g ⊢ ( 𝑁 ∈ 𝑉 → ( 𝑣 ∈ ( { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ∖ { 𝑁 } ) ↔ 𝑣 ∈ ( { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) } ∖ { 𝑁 } ) ) )
42 41 eqrdv ⊢ ( 𝑁 ∈ 𝑉 → ( { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ∖ { 𝑁 } ) = ( { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) } ∖ { 𝑁 } ) )
43 4 42 eqtr3id ⊢ ( 𝑁 ∈ 𝑉 → { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } = ( { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) } ∖ { 𝑁 } ) )
44 1 2 dfnbgr2 ⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } )
45 1 2 3 dfvopnbgr2 ⊢ ( 𝑁 ∈ 𝑉 → 𝑈 = { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) } )
46 45 difeq1d ⊢ ( 𝑁 ∈ 𝑉 → ( 𝑈 ∖ { 𝑁 } ) = ( { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) } ∖ { 𝑁 } ) )
47 43 44 46 3eqtr4d ⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 NeighbVtx 𝑁 ) = ( 𝑈 ∖ { 𝑁 } ) )