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

Metamath Proof Explorer

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 )