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 → G NeighbVtx N = n ∈ V ∖ N | ∃ i ∈ dom ⁡ I N n ⊆ 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 → G NeighbVtx N = n ∈ V ∖ N | ∃ e ∈ Edg ⁡ G N n ⊆ e
5 4 adantr ⊢ N ∈ V ∧ Fun ⁡ I → G NeighbVtx N = n ∈ V ∖ N | ∃ e ∈ Edg ⁡ G N n ⊆ 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 ⁡ G N n ⊆ e ↔ ∃ e ∈ ran ⁡ I N n ⊆ e
11 funfn ⊢ Fun ⁡ I ↔ I Fn dom ⁡ I
12 11 biimpi ⊢ Fun ⁡ I → I Fn dom ⁡ I
13 12 adantl ⊢ N ∈ V ∧ Fun ⁡ I → I Fn dom ⁡ I
14 sseq2 ⊢ e = I ⁡ i → N n ⊆ e ↔ N n ⊆ I ⁡ i
15 14 rexrn ⊢ I Fn dom ⁡ I → ∃ e ∈ ran ⁡ I N n ⊆ e ↔ ∃ i ∈ dom ⁡ I N n ⊆ I ⁡ i
16 13 15 syl ⊢ N ∈ V ∧ Fun ⁡ I → ∃ e ∈ ran ⁡ I N n ⊆ e ↔ ∃ i ∈ dom ⁡ I N n ⊆ I ⁡ i
17 10 16 syl5bb ⊢ N ∈ V ∧ Fun ⁡ I → ∃ e ∈ Edg ⁡ G N n ⊆ e ↔ ∃ i ∈ dom ⁡ I N n ⊆ I ⁡ i
18 17 rabbidv ⊢ N ∈ V ∧ Fun ⁡ I → n ∈ V ∖ N | ∃ e ∈ Edg ⁡ G N n ⊆ e = n ∈ V ∖ N | ∃ i ∈ dom ⁡ I N n ⊆ I ⁡ i
19 5 18 eqtrd ⊢ N ∈ V ∧ Fun ⁡ I → G NeighbVtx N = n ∈ V ∖ N | ∃ i ∈ dom ⁡ I N n ⊆ I ⁡ i