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 syl5bb ( ( 𝑁𝑉 ∧ Fun 𝐼 ) → ( ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ ∃ 𝑖 ∈ dom 𝐼 { 𝑁 , 𝑛 } ⊆ ( 𝐼𝑖 ) ) )
18 17 rabbidv ( ( 𝑁𝑉 ∧ Fun 𝐼 ) → { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑁 , 𝑛 } ⊆ 𝑒 } = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑖 ∈ dom 𝐼 { 𝑁 , 𝑛 } ⊆ ( 𝐼𝑖 ) } )
19 5 18 eqtrd ( ( 𝑁𝑉 ∧ Fun 𝐼 ) → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑖 ∈ dom 𝐼 { 𝑁 , 𝑛 } ⊆ ( 𝐼𝑖 ) } )