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	bilani	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ { 𝑛 , 𝑈 } ∈ 𝐸 ) → { 𝑈 , 𝑛 } ∈ 𝐸 )
12		prid1g	⊢ ( 𝑈 ∈ 𝑉 → 𝑈 ∈ { 𝑈 , 𝑛 } )
13	12	adantl	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → 𝑈 ∈ { 𝑈 , 𝑛 } )
14	13	adantr	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ { 𝑛 , 𝑈 } ∈ 𝐸 ) → 𝑈 ∈ { 𝑈 , 𝑛 } )
15		eleq2	⊢ ( 𝑒 = { 𝑈 , 𝑛 } → ( 𝑈 ∈ 𝑒 ↔ 𝑈 ∈ { 𝑈 , 𝑛 } ) )
16	15 4	elrab2	⊢ ( { 𝑈 , 𝑛 } ∈ 𝐼 ↔ ( { 𝑈 , 𝑛 } ∈ 𝐸 ∧ 𝑈 ∈ { 𝑈 , 𝑛 } ) )
17	11 14 16	sylanbrc	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ { 𝑛 , 𝑈 } ∈ 𝐸 ) → { 𝑈 , 𝑛 } ∈ 𝐼 )
18	17	ex	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( { 𝑛 , 𝑈 } ∈ 𝐸 → { 𝑈 , 𝑛 } ∈ 𝐼 ) )
19	8 18	sylbid	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑈 ) → { 𝑈 , 𝑛 } ∈ 𝐼 ) )
20	6 19	biimtrid	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝑛 ∈ 𝑁 → { 𝑈 , 𝑛 } ∈ 𝐼 ) )
21	20	ralrimiv	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ∀ 𝑛 ∈ 𝑁 { 𝑈 , 𝑛 } ∈ 𝐼 )
22	4	reqabi	⊢ ( 𝑒 ∈ 𝐼 ↔ ( 𝑒 ∈ 𝐸 ∧ 𝑈 ∈ 𝑒 ) )
23	2 3	edgnbusgreu	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ ( 𝑒 ∈ 𝐸 ∧ 𝑈 ∈ 𝑒 ) ) → ∃! 𝑛 ∈ 𝑁 𝑒 = { 𝑈 , 𝑛 } )
24	22 23	sylan2b	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐼 ) → ∃! 𝑛 ∈ 𝑁 𝑒 = { 𝑈 , 𝑛 } )
25	24	ralrimiva	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ∀ 𝑒 ∈ 𝐼 ∃! 𝑛 ∈ 𝑁 𝑒 = { 𝑈 , 𝑛 } )
26	5	f1ompt	⊢ ( 𝐹 : 𝑁 –1-1-onto→ 𝐼 ↔ ( ∀ 𝑛 ∈ 𝑁 { 𝑈 , 𝑛 } ∈ 𝐼 ∧ ∀ 𝑒 ∈ 𝐼 ∃! 𝑛 ∈ 𝑁 𝑒 = { 𝑈 , 𝑛 } ) )
27	21 25 26	sylanbrc	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → 𝐹 : 𝑁 –1-1-onto→ 𝐼 )