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 syl5bi ( ( 𝐺 ∈ USGraph ∧ 𝑈𝑉 ) → ( 𝑛𝑁 → { 𝑈 , 𝑛 } ∈ 𝐼 ) )
22 21 ralrimiv ( ( 𝐺 ∈ USGraph ∧ 𝑈𝑉 ) → ∀ 𝑛𝑁 { 𝑈 , 𝑛 } ∈ 𝐼 )
23 4 rabeq2i ( 𝑒𝐼 ↔ ( 𝑒𝐸𝑈𝑒 ) )
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𝐼 )