This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
nbusgrf1o1.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
nbusgrf1o1.n ⊢ 𝑁 = ( 𝐺 NeighbVtx 𝑈 )
nbusgrf1o1.i ⊢ 𝐼 = { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 }
nbusgrf1o.f ⊢ 𝐹 = ( 𝑛 ∈ 𝑁 ↦ { 𝑈 , 𝑛 } )
Assertion nbusgrf1o0 ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → 𝐹 : 𝑁 –1-1-onto→ 𝐼 )

Proof

Step Hyp Ref Expression
1 nbusgrf1o1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 nbusgrf1o1.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 nbusgrf1o1.n ⊢ 𝑁 = ( 𝐺 NeighbVtx 𝑈 )
4 nbusgrf1o1.i ⊢ 𝐼 = { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 }
5 nbusgrf1o.f ⊢ 𝐹 = ( 𝑛 ∈ 𝑁 ↦ { 𝑈 , 𝑛 } )
6 3 eleq2i ⊢ ( 𝑛 ∈ 𝑁 ↔ 𝑛 ∈ ( 𝐺 NeighbVtx 𝑈 ) )
7 2 nbusgreledg ⊢ ( 𝐺 ∈ USGraph → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑈 ) ↔ { 𝑛 , 𝑈 } ∈ 𝐸 ) )
8 7 adantr ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑈 ) ↔ { 𝑛 , 𝑈 } ∈ 𝐸 ) )
9 prcom ⊢ { 𝑛 , 𝑈 } = { 𝑈 , 𝑛 }
10 9 eleq1i ⊢ ( { 𝑛 , 𝑈 } ∈ 𝐸 ↔ { 𝑈 , 𝑛 } ∈ 𝐸 )
11 10 biimpi ⊢ ( { 𝑛 , 𝑈 } ∈ 𝐸 → { 𝑈 , 𝑛 } ∈ 𝐸 )
12 11 adantl ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ { 𝑛 , 𝑈 } ∈ 𝐸 ) → { 𝑈 , 𝑛 } ∈ 𝐸 )
13 prid1g ⊢ ( 𝑈 ∈ 𝑉 → 𝑈 ∈ { 𝑈 , 𝑛 } )
14 13 adantl ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → 𝑈 ∈ { 𝑈 , 𝑛 } )
15 14 adantr ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ { 𝑛 , 𝑈 } ∈ 𝐸 ) → 𝑈 ∈ { 𝑈 , 𝑛 } )
16 eleq2 ⊢ ( 𝑒 = { 𝑈 , 𝑛 } → ( 𝑈 ∈ 𝑒 ↔ 𝑈 ∈ { 𝑈 , 𝑛 } ) )
17 16 4 elrab2 ⊢ ( { 𝑈 , 𝑛 } ∈ 𝐼 ↔ ( { 𝑈 , 𝑛 } ∈ 𝐸 ∧ 𝑈 ∈ { 𝑈 , 𝑛 } ) )
18 12 15 17 sylanbrc ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ { 𝑛 , 𝑈 } ∈ 𝐸 ) → { 𝑈 , 𝑛 } ∈ 𝐼 )
19 18 ex ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( { 𝑛 , 𝑈 } ∈ 𝐸 → { 𝑈 , 𝑛 } ∈ 𝐼 ) )
20 8 19 sylbid ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑈 ) → { 𝑈 , 𝑛 } ∈ 𝐼 ) )
21 6 20 biimtrid ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝑛 ∈ 𝑁 → { 𝑈 , 𝑛 } ∈ 𝐼 ) )
22 21 ralrimiv ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ∀ 𝑛 ∈ 𝑁 { 𝑈 , 𝑛 } ∈ 𝐼 )
23 4 reqabi ⊢ ( 𝑒 ∈ 𝐼 ↔ ( 𝑒 ∈ 𝐸 ∧ 𝑈 ∈ 𝑒 ) )
24 2 3 edgnbusgreu ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ ( 𝑒 ∈ 𝐸 ∧ 𝑈 ∈ 𝑒 ) ) → ∃! 𝑛 ∈ 𝑁 𝑒 = { 𝑈 , 𝑛 } )
25 23 24 sylan2b ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐼 ) → ∃! 𝑛 ∈ 𝑁 𝑒 = { 𝑈 , 𝑛 } )
26 25 ralrimiva ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ∀ 𝑒 ∈ 𝐼 ∃! 𝑛 ∈ 𝑁 𝑒 = { 𝑈 , 𝑛 } )
27 5 f1ompt ⊢ ( 𝐹 : 𝑁 –1-1-onto→ 𝐼 ↔ ( ∀ 𝑛 ∈ 𝑁 { 𝑈 , 𝑛 } ∈ 𝐼 ∧ ∀ 𝑒 ∈ 𝐼 ∃! 𝑛 ∈ 𝑁 𝑒 = { 𝑈 , 𝑛 } ) )
28 22 26 27 sylanbrc ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → 𝐹 : 𝑁 –1-1-onto→ 𝐼 )