Theorem usgredgedg

Description: In a simple graph there is a 1-1 onto mapping between the indexed edges containing a fixed vertex and the set of edges containing this vertex. (Contributed by AV, 18-Oct-2020) (Proof shortened by AV, 11-Dec-2020)

	Ref	Expression
Hypotheses	ushgredgedg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	ushgredgedg.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	ushgredgedg.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	ushgredgedg.a	⊢ 𝐴 = { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) }
	ushgredgedg.b	⊢ 𝐵 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 }
	ushgredgedg.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐼 ‘ 𝑥 ) )
Assertion	usgredgedg	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ushgredgedg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
2		ushgredgedg.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3		ushgredgedg.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
4		ushgredgedg.a	⊢ 𝐴 = { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) }
5		ushgredgedg.b	⊢ 𝐵 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 }
6		ushgredgedg.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐼 ‘ 𝑥 ) )
7		usgruspgr	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ USPGraph )
8		uspgrushgr	⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ USHGraph )
9	7 8	syl	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ USHGraph )
10	1 2 3 4 5 6	ushgredgedg	⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
11	9 10	sylan	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )