Metamath Proof Explorer

Theorem uspgredgleord

Description: In a simple pseudograph the number of edges which contain a given vertex is not greater than the number of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018) (Revised by AV, 6-Dec-2020)

Ref Expression
Hypotheses usgredgleord.v ⊢V=Vtx⁡G
usgredgleord.e ⊢E=Edg⁡G
Assertion uspgredgleord ⊢G∈USHGraph∧N∈V→e∈E|N∈e≤V

Proof

Step Hyp Ref Expression
1 usgredgleord.v ⊢V=Vtx⁡G
2 usgredgleord.e ⊢E=Edg⁡G
3 1 fvexi ⊢V∈V
4 eqid ⊢e∈E|N∈e=e∈E|N∈e
5 eqid ⊢x∈e∈E|N∈e⟼ιy∈V|x=Ny=x∈e∈E|N∈e⟼ιy∈V|x=Ny
6 1 2 4 5 uspgredg2v ⊢G∈USHGraph∧N∈V→x∈e∈E|N∈e⟼ιy∈V|x=Ny:e∈E|N∈e⟶1-1V
7 f1domg ⊢V∈V→x∈e∈E|N∈e⟼ιy∈V|x=Ny:e∈E|N∈e⟶1-1V→e∈E|N∈e≼V
8 3 6 7 mpsyl ⊢G∈USHGraph∧N∈V→e∈E|N∈e≼V
9 hashdomi ⊢e∈E|N∈e≼V→e∈E|N∈e≤V
10 8 9 syl ⊢G∈USHGraph∧N∈V→e∈E|N∈e≤V