Metamath Proof Explorer


Theorem dfclnbgr2

Description: Alternate definition of the closed neighborhood of a vertex breaking up the subset relationship of an unordered pair. (Contributed by AV, 7-May-2025)

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

Proof

Step Hyp Ref Expression
1 clnbgrval.v 𝑉 = ( Vtx ‘ 𝐺 )
2 clnbgrval.e 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 clnbgrval ( 𝑁𝑉 → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ { 𝑛𝑉 ∣ ∃ 𝑒𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } ) )
4 prssg ( ( 𝑁𝑉𝑛 ∈ V ) → ( ( 𝑁𝑒𝑛𝑒 ) ↔ { 𝑁 , 𝑛 } ⊆ 𝑒 ) )
5 4 elvd ( 𝑁𝑉 → ( ( 𝑁𝑒𝑛𝑒 ) ↔ { 𝑁 , 𝑛 } ⊆ 𝑒 ) )
6 5 bicomd ( 𝑁𝑉 → ( { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ ( 𝑁𝑒𝑛𝑒 ) ) )
7 6 rexbidv ( 𝑁𝑉 → ( ∃ 𝑒𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ ∃ 𝑒𝐸 ( 𝑁𝑒𝑛𝑒 ) ) )
8 7 rabbidv ( 𝑁𝑉 → { 𝑛𝑉 ∣ ∃ 𝑒𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } = { 𝑛𝑉 ∣ ∃ 𝑒𝐸 ( 𝑁𝑒𝑛𝑒 ) } )
9 8 uneq2d ( 𝑁𝑉 → ( { 𝑁 } ∪ { 𝑛𝑉 ∣ ∃ 𝑒𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } ) = ( { 𝑁 } ∪ { 𝑛𝑉 ∣ ∃ 𝑒𝐸 ( 𝑁𝑒𝑛𝑒 ) } ) )
10 3 9 eqtrd ( 𝑁𝑉 → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ { 𝑛𝑉 ∣ ∃ 𝑒𝐸 ( 𝑁𝑒𝑛𝑒 ) } ) )