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 biimpi ⊢ n U ∈ E → U n ∈ E
12 11 adantl ⊢ G ∈ USGraph ∧ U ∈ V ∧ n U ∈ E → U n ∈ E
13 prid1g ⊢ U ∈ V → U ∈ U n
14 13 adantl ⊢ G ∈ USGraph ∧ U ∈ V → U ∈ U n
15 14 adantr ⊢ G ∈ USGraph ∧ U ∈ V ∧ n U ∈ E → U ∈ U n
16 eleq2 ⊢ e = U n → U ∈ e ↔ U ∈ U n
17 16 4 elrab2 ⊢ U n ∈ I ↔ U n ∈ E ∧ U ∈ U n
18 12 15 17 sylanbrc ⊢ G ∈ USGraph ∧ U ∈ V ∧ n U ∈ E → U n ∈ I
19 18 ex ⊢ G ∈ USGraph ∧ U ∈ V → n U ∈ E → U n ∈ I
20 8 19 sylbid ⊢ G ∈ USGraph ∧ U ∈ V → n ∈ G NeighbVtx U → U n ∈ I
21 6 20 syl5bi ⊢ G ∈ USGraph ∧ U ∈ V → n ∈ N → U n ∈ I
22 21 ralrimiv ⊢ G ∈ USGraph ∧ U ∈ V → ∀ n ∈ N U n ∈ I
23 4 rabeq2i ⊢ e ∈ I ↔ e ∈ E ∧ U ∈ e
24 2 3 edgnbusgreu ⊢ G ∈ USGraph ∧ U ∈ V ∧ e ∈ E ∧ U ∈ e → ∃! n ∈ N e = U n
25 23 24 sylan2b ⊢ G ∈ USGraph ∧ U ∈ V ∧ e ∈ I → ∃! n ∈ N e = U n
26 25 ralrimiva ⊢ G ∈ USGraph ∧ U ∈ V → ∀ e ∈ I ∃! n ∈ N e = U n
27 5 f1ompt ⊢ F : N ⟶ 1-1 onto I ↔ ∀ n ∈ N U n ∈ I ∧ ∀ e ∈ I ∃! n ∈ N e = U n
28 22 26 27 sylanbrc ⊢ G ∈ USGraph ∧ U ∈ V → F : N ⟶ 1-1 onto I