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 ⊢ 𝑉 = ( 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 ffvelcdmda ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝑋 ) ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
5 fveqeq2 ⊢ ( 𝑥 = ( 𝐸 ‘ 𝑋 ) → ( ( ♯ ‘ 𝑥 ) = 2 ↔ ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 ) )
6 5 elrab ⊢ ( ( 𝐸 ‘ 𝑋 ) ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( ( 𝐸 ‘ 𝑋 ) ∈ 𝒫 𝑉 ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 ) )
7 6 simprbi ⊢ ( ( 𝐸 ‘ 𝑋 ) ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 )
8 4 7 syl ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 )