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 ⊢ I = iEdg ⁡ G
Assertion upgrle2 ⊢ G ∈ UPGraph ∧ X ∈ dom ⁡ I → I ⁡ X ≤ 2

Proof

Step Hyp Ref Expression
1 upgrle2.i ⊢ I = iEdg ⁡ G
2 simpl ⊢ G ∈ UPGraph ∧ X ∈ dom ⁡ I → G ∈ UPGraph
3 upgruhgr ⊢ G ∈ UPGraph → G ∈ UHGraph
4 1 uhgrfun ⊢ G ∈ UHGraph → Fun ⁡ I
5 3 4 syl ⊢ G ∈ UPGraph → Fun ⁡ I
6 5 funfnd ⊢ G ∈ UPGraph → I Fn dom ⁡ I
7 6 adantr ⊢ G ∈ UPGraph ∧ X ∈ dom ⁡ I → I Fn dom ⁡ I
8 simpr ⊢ G ∈ UPGraph ∧ X ∈ dom ⁡ I → X ∈ dom ⁡ I
9 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
10 9 1 upgrle ⊢ G ∈ UPGraph ∧ I Fn dom ⁡ I ∧ X ∈ dom ⁡ I → I ⁡ X ≤ 2
11 2 7 8 10 syl3anc ⊢ G ∈ UPGraph ∧ X ∈ dom ⁡ I → I ⁡ X ≤ 2