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

Metamath Proof Explorer

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 ⊢ E = Edg ⁡ G
ushgredgedg.i ⊢ I = iEdg ⁡ G
ushgredgedg.v ⊢ V = Vtx ⁡ G
ushgredgedg.a ⊢ A = i ∈ dom ⁡ I | N ∈ I ⁡ i
ushgredgedg.b ⊢ B = e ∈ E | N ∈ e
ushgredgedg.f ⊢ F = x ∈ A ⟼ I ⁡ x
Assertion usgredgedg ⊢ G ∈ USGraph ∧ N ∈ V → F : A ⟶ 1-1 onto B

Proof

Step Hyp Ref Expression
1 ushgredgedg.e ⊢ E = Edg ⁡ G
2 ushgredgedg.i ⊢ I = iEdg ⁡ G
3 ushgredgedg.v ⊢ V = Vtx ⁡ G
4 ushgredgedg.a ⊢ A = i ∈ dom ⁡ I | N ∈ I ⁡ i
5 ushgredgedg.b ⊢ B = e ∈ E | N ∈ e
6 ushgredgedg.f ⊢ F = x ∈ A ⟼ I ⁡ x
7 usgruspgr ⊢ G ∈ USGraph → G ∈ USHGraph
8 uspgrushgr ⊢ G ∈ USHGraph → G ∈ USHGraph
9 7 8 syl ⊢ G ∈ USGraph → G ∈ USHGraph
10 1 2 3 4 5 6 ushgredgedg ⊢ G ∈ USHGraph ∧ N ∈ V → F : A ⟶ 1-1 onto B
11 9 10 sylan ⊢ G ∈ USGraph ∧ N ∈ V → F : A ⟶ 1-1 onto B