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 )