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 ⊢V=Vtx⁡G
dfnbgr3.i ⊢I=iEdg⁡G
Assertion dfnbgr3 ⊢N∈V∧Fun⁡I→GNeighbVtxN=n∈V∖N|∃i∈dom⁡INn⊆I⁡i

Proof

Step Hyp Ref Expression
1 dfnbgr3.v ⊢V=Vtx⁡G
2 dfnbgr3.i ⊢I=iEdg⁡G
3 eqid ⊢Edg⁡G=Edg⁡G
4 1 3 nbgrval ⊢N∈V→GNeighbVtxN=n∈V∖N|∃e∈Edg⁡GNn⊆e
5 4 adantr ⊢N∈V∧Fun⁡I→GNeighbVtxN=n∈V∖N|∃e∈Edg⁡GNn⊆e
6 edgval ⊢Edg⁡G=ran⁡iEdg⁡G
7 2 eqcomi ⊢iEdg⁡G=I
8 7 rneqi ⊢ran⁡iEdg⁡G=ran⁡I
9 6 8 eqtri ⊢Edg⁡G=ran⁡I
10 9 rexeqi ⊢∃e∈Edg⁡GNn⊆e↔∃e∈ran⁡INn⊆e
11 funfn ⊢Fun⁡I↔IFndom⁡I
12 11 biimpi ⊢Fun⁡I→IFndom⁡I
13 12 adantl ⊢N∈V∧Fun⁡I→IFndom⁡I
14 sseq2 ⊢e=I⁡i→Nn⊆e↔Nn⊆I⁡i
15 14 rexrn ⊢IFndom⁡I→∃e∈ran⁡INn⊆e↔∃i∈dom⁡INn⊆I⁡i
16 13 15 syl ⊢N∈V∧Fun⁡I→∃e∈ran⁡INn⊆e↔∃i∈dom⁡INn⊆I⁡i
17 10 16 syl5bb ⊢N∈V∧Fun⁡I→∃e∈Edg⁡GNn⊆e↔∃i∈dom⁡INn⊆I⁡i
18 17 rabbidv ⊢N∈V∧Fun⁡I→n∈V∖N|∃e∈Edg⁡GNn⊆e=n∈V∖N|∃i∈dom⁡INn⊆I⁡i
19 5 18 eqtrd ⊢N∈V∧Fun⁡I→GNeighbVtxN=n∈V∖N|∃i∈dom⁡INn⊆I⁡i