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

Metamath Proof Explorer

Theorem umgredg2

Description: An edge of a multigraph has exactly two ends. (Contributed by AV, 24-Nov-2020)

Ref Expression
Hypotheses isumgr.v ⊢ V = Vtx ⁡ G
isumgr.e ⊢ E = iEdg ⁡ G
Assertion umgredg2 ⊢ G ∈ UMGraph ∧ X ∈ dom ⁡ E → E ⁡ X = 2

Proof

Step Hyp Ref Expression
1 isumgr.v ⊢ V = Vtx ⁡ G
2 isumgr.e ⊢ E = iEdg ⁡ G
3 1 2 umgrf ⊢ G ∈ UMGraph → E : dom ⁡ E ⟶ x ∈ 𝒫 V | x = 2
4 3 ffvelcdmda ⊢ G ∈ UMGraph ∧ X ∈ dom ⁡ E → E ⁡ X ∈ x ∈ 𝒫 V | x = 2
5 fveqeq2 ⊢ x = E ⁡ X → x = 2 ↔ E ⁡ X = 2
6 5 elrab ⊢ E ⁡ X ∈ x ∈ 𝒫 V | x = 2 ↔ E ⁡ X ∈ 𝒫 V ∧ E ⁡ X = 2
7 6 simprbi ⊢ E ⁡ X ∈ x ∈ 𝒫 V | x = 2 → E ⁡ X = 2
8 4 7 syl ⊢ G ∈ UMGraph ∧ X ∈ dom ⁡ E → E ⁡ X = 2