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

Metamath Proof Explorer

Theorem dfnbgr3

Description: Alternate definition of the neighbors of a vertex using the edge function instead of the edges themselves (see also nbgrval ). (Contributed by Alexander van der Vekens, 17-Dec-2017) (Revised by AV, 25-Oct-2020) (Revised by AV, 21-Mar-2021)

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

Proof

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