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 𝑉 = ( Vtx ‘ 𝐺 )
isumgr.e 𝐸 = ( iEdg ‘ 𝐺 )
Assertion umgredg2 ( ( 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( ♯ ‘ ( 𝐸𝑋 ) ) = 2 )

Proof

Step Hyp Ref Expression
1 isumgr.v 𝑉 = ( Vtx ‘ 𝐺 )
2 isumgr.e 𝐸 = ( iEdg ‘ 𝐺 )
3 1 2 umgrf ( 𝐺 ∈ UMGraph → 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
4 3 ffvelrnda ( ( 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( 𝐸𝑋 ) ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
5 fveqeq2 ( 𝑥 = ( 𝐸𝑋 ) → ( ( ♯ ‘ 𝑥 ) = 2 ↔ ( ♯ ‘ ( 𝐸𝑋 ) ) = 2 ) )
6 5 elrab ( ( 𝐸𝑋 ) ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( ( 𝐸𝑋 ) ∈ 𝒫 𝑉 ∧ ( ♯ ‘ ( 𝐸𝑋 ) ) = 2 ) )
7 6 simprbi ( ( 𝐸𝑋 ) ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( ♯ ‘ ( 𝐸𝑋 ) ) = 2 )
8 4 7 syl ( ( 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( ♯ ‘ ( 𝐸𝑋 ) ) = 2 )