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 = G NeighbVtx U
nbusgrf1o1.i ⊢ I = e ∈ E | U ∈ e
nbusgrf1o.f ⊢ F = n ∈ N ⟼ U n
Assertion nbusgrf1o0 ⊢ G ∈ USGraph ∧ U ∈ V → F : N ⟶ 1-1 onto I

Proof

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