Metamath Proof Explorer

Theorem upgrle

Description: An edge of an undirected pseudograph has at most two ends. (Contributed by Mario Carneiro, 11-Mar-2015) (Revised by AV, 10-Oct-2020)

Ref Expression
Hypotheses isupgr.v ⊢ V = Vtx ⁡ G
isupgr.e ⊢ E = iEdg ⁡ G
Assertion upgrle ⊢ G ∈ UPGraph ∧ E Fn A ∧ F ∈ A → E ⁡ F ≤ 2

Proof

Step Hyp Ref Expression
1 isupgr.v ⊢ V = Vtx ⁡ G
2 isupgr.e ⊢ E = iEdg ⁡ G
3 1 2 upgrfn ⊢ G ∈ UPGraph ∧ E Fn A → E : A ⟶ x ∈ 𝒫 V ∖ ∅ | x ≤ 2
4 3 ffvelcdmda ⊢ G ∈ UPGraph ∧ E Fn A ∧ F ∈ A → E ⁡ F ∈ x ∈ 𝒫 V ∖ ∅ | x ≤ 2
5 4 3impa ⊢ G ∈ UPGraph ∧ E Fn A ∧ F ∈ A → E ⁡ F ∈ x ∈ 𝒫 V ∖ ∅ | x ≤ 2
6 fveq2 ⊢ x = E ⁡ F → x = E ⁡ F
7 6 breq1d ⊢ x = E ⁡ F → x ≤ 2 ↔ E ⁡ F ≤ 2
8 7 elrab ⊢ E ⁡ F ∈ x ∈ 𝒫 V ∖ ∅ | x ≤ 2 ↔ E ⁡ F ∈ 𝒫 V ∖ ∅ ∧ E ⁡ F ≤ 2
9 8 simprbi ⊢ E ⁡ F ∈ x ∈ 𝒫 V ∖ ∅ | x ≤ 2 → E ⁡ F ≤ 2
10 5 9 syl ⊢ G ∈ UPGraph ∧ E Fn A ∧ F ∈ A → E ⁡ F ≤ 2