Metamath Proof Explorer

Theorem nbusgrf1o0

Description: The mapping of neighbors of a vertex to edges incident to the vertex is a bijection ( 1-1 onto function) in a simple graph. (Contributed by Alexander van der Vekens, 17-Dec-2017) (Revised by AV, 28-Oct-2020)

Ref Expression
Hypotheses nbusgrf1o1.v ⊢V=Vtx⁡G
nbusgrf1o1.e ⊢E=Edg⁡G
nbusgrf1o1.n ⊢N=GNeighbVtxU
nbusgrf1o1.i ⊢I=e∈E|U∈e
nbusgrf1o.f ⊢F=n∈N⟼Un
Assertion nbusgrf1o0 ⊢G∈USGraph∧U∈V→F:N⟶1-1 ontoI

Proof

Step Hyp Ref Expression
1 nbusgrf1o1.v ⊢V=Vtx⁡G
2 nbusgrf1o1.e ⊢E=Edg⁡G
3 nbusgrf1o1.n ⊢N=GNeighbVtxU
4 nbusgrf1o1.i ⊢I=e∈E|U∈e
5 nbusgrf1o.f ⊢F=n∈N⟼Un
6 3 eleq2i ⊢n∈N↔n∈GNeighbVtxU
7 2 nbusgreledg ⊢G∈USGraph→n∈GNeighbVtxU↔nU∈E
8 7 adantr ⊢G∈USGraph∧U∈V→n∈GNeighbVtxU↔nU∈E
9 prcom ⊢nU=Un
10 9 eleq1i ⊢nU∈E↔Un∈E
11 10 biimpi ⊢nU∈E→Un∈E
12 11 adantl ⊢G∈USGraph∧U∈V∧nU∈E→Un∈E
13 prid1g ⊢U∈V→U∈Un
14 13 adantl ⊢G∈USGraph∧U∈V→U∈Un
15 14 adantr ⊢G∈USGraph∧U∈V∧nU∈E→U∈Un
16 eleq2 ⊢e=Un→U∈e↔U∈Un
17 16 4 elrab2 ⊢Un∈I↔Un∈E∧U∈Un
18 12 15 17 sylanbrc ⊢G∈USGraph∧U∈V∧nU∈E→Un∈I
19 18 ex ⊢G∈USGraph∧U∈V→nU∈E→Un∈I
20 8 19 sylbid ⊢G∈USGraph∧U∈V→n∈GNeighbVtxU→Un∈I
21 6 20 syl5bi ⊢G∈USGraph∧U∈V→n∈N→Un∈I
22 21 ralrimiv ⊢G∈USGraph∧U∈V→∀n∈NUn∈I
23 4 rabeq2i ⊢e∈I↔e∈E∧U∈e
24 2 3 edgnbusgreu ⊢G∈USGraph∧U∈V∧e∈E∧U∈e→∃!n∈Ne=Un
25 23 24 sylan2b ⊢G∈USGraph∧U∈V∧e∈I→∃!n∈Ne=Un
26 25 ralrimiva ⊢G∈USGraph∧U∈V→∀e∈I∃!n∈Ne=Un
27 5 f1ompt ⊢F:N⟶1-1 ontoI↔∀n∈NUn∈I∧∀e∈I∃!n∈Ne=Un
28 22 26 27 sylanbrc ⊢G∈USGraph∧U∈V→F:N⟶1-1 ontoI