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

Metamath Proof Explorer

Theorem dfclnbgr3

Description: Alternate definition of the closed neighborhood of a vertex using the edge function instead of the edges themselves (see also clnbgrval ). (Contributed by AV, 8-May-2025)

Ref Expression
Hypotheses dfclnbgr3.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
dfclnbgr3.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion dfclnbgr3 ( ( 𝑁 ∈ 𝑉 ∧ Fun 𝐼 ) → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑖 ∈ dom 𝐼 { 𝑁 , 𝑛 } ⊆ ( 𝐼 ‘ 𝑖 ) } ) )

Proof

Step Hyp Ref Expression
1 dfclnbgr3.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 dfclnbgr3.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
4 3 eqcomi ⊢ ran ( iEdg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
5 1 4 clnbgrval ⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ ran ( iEdg ‘ 𝐺 ) { 𝑁 , 𝑛 } ⊆ 𝑒 } ) )
6 5 adantr ⊢ ( ( 𝑁 ∈ 𝑉 ∧ Fun 𝐼 ) → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ ran ( iEdg ‘ 𝐺 ) { 𝑁 , 𝑛 } ⊆ 𝑒 } ) )
7 2 eqcomi ⊢ ( iEdg ‘ 𝐺 ) = 𝐼
8 7 rneqi ⊢ ran ( iEdg ‘ 𝐺 ) = ran 𝐼
9 8 rexeqi ⊢ ( ∃ 𝑒 ∈ ran ( iEdg ‘ 𝐺 ) { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ ran 𝐼 { 𝑁 , 𝑛 } ⊆ 𝑒 )
10 funfn ⊢ ( Fun 𝐼 ↔ 𝐼 Fn dom 𝐼 )
11 10 biimpi ⊢ ( Fun 𝐼 → 𝐼 Fn dom 𝐼 )
12 11 adantl ⊢ ( ( 𝑁 ∈ 𝑉 ∧ Fun 𝐼 ) → 𝐼 Fn dom 𝐼 )
13 sseq2 ⊢ ( 𝑒 = ( 𝐼 ‘ 𝑖 ) → ( { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ { 𝑁 , 𝑛 } ⊆ ( 𝐼 ‘ 𝑖 ) ) )
14 13 rexrn ⊢ ( 𝐼 Fn dom 𝐼 → ( ∃ 𝑒 ∈ ran 𝐼 { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ ∃ 𝑖 ∈ dom 𝐼 { 𝑁 , 𝑛 } ⊆ ( 𝐼 ‘ 𝑖 ) ) )
15 12 14 syl ⊢ ( ( 𝑁 ∈ 𝑉 ∧ Fun 𝐼 ) → ( ∃ 𝑒 ∈ ran 𝐼 { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ ∃ 𝑖 ∈ dom 𝐼 { 𝑁 , 𝑛 } ⊆ ( 𝐼 ‘ 𝑖 ) ) )
16 9 15 bitrid ⊢ ( ( 𝑁 ∈ 𝑉 ∧ Fun 𝐼 ) → ( ∃ 𝑒 ∈ ran ( iEdg ‘ 𝐺 ) { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ ∃ 𝑖 ∈ dom 𝐼 { 𝑁 , 𝑛 } ⊆ ( 𝐼 ‘ 𝑖 ) ) )
17 16 rabbidv ⊢ ( ( 𝑁 ∈ 𝑉 ∧ Fun 𝐼 ) → { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ ran ( iEdg ‘ 𝐺 ) { 𝑁 , 𝑛 } ⊆ 𝑒 } = { 𝑛 ∈ 𝑉 ∣ ∃ 𝑖 ∈ dom 𝐼 { 𝑁 , 𝑛 } ⊆ ( 𝐼 ‘ 𝑖 ) } )
18 17 uneq2d ⊢ ( ( 𝑁 ∈ 𝑉 ∧ Fun 𝐼 ) → ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ ran ( iEdg ‘ 𝐺 ) { 𝑁 , 𝑛 } ⊆ 𝑒 } ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑖 ∈ dom 𝐼 { 𝑁 , 𝑛 } ⊆ ( 𝐼 ‘ 𝑖 ) } ) )
19 6 18 eqtrd ⊢ ( ( 𝑁 ∈ 𝑉 ∧ Fun 𝐼 ) → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑖 ∈ dom 𝐼 { 𝑁 , 𝑛 } ⊆ ( 𝐼 ‘ 𝑖 ) } ) )