Theorem upgrle2

Description: An edge of an undirected pseudograph has at most two ends. (Contributed by AV, 6-Feb-2021)

	Ref	Expression
Hypothesis	upgrle2.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion	upgrle2	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑋 ∈ dom 𝐼 ) → ( ♯ ‘ ( 𝐼 ‘ 𝑋 ) ) ≤ 2 )

Proof

Step	Hyp	Ref	Expression
1		upgrle2.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2		simpl	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑋 ∈ dom 𝐼 ) → 𝐺 ∈ UPGraph )
3		upgruhgr	⊢ ( 𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph )
4	1	uhgrfun	⊢ ( 𝐺 ∈ UHGraph → Fun 𝐼 )
5	3 4	syl	⊢ ( 𝐺 ∈ UPGraph → Fun 𝐼 )
6	5	funfnd	⊢ ( 𝐺 ∈ UPGraph → 𝐼 Fn dom 𝐼 )
7	6	adantr	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑋 ∈ dom 𝐼 ) → 𝐼 Fn dom 𝐼 )
8		simpr	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑋 ∈ dom 𝐼 ) → 𝑋 ∈ dom 𝐼 )
9		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
10	9 1	upgrle	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐼 Fn dom 𝐼 ∧ 𝑋 ∈ dom 𝐼 ) → ( ♯ ‘ ( 𝐼 ‘ 𝑋 ) ) ≤ 2 )
11	2 7 8 10	syl3anc	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑋 ∈ dom 𝐼 ) → ( ♯ ‘ ( 𝐼 ‘ 𝑋 ) ) ≤ 2 )