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 = N y = x e E | N e ι y V | x = N y
6 1 2 4 5 uspgredg2v G USHGraph N V x e E | N e ι y V | x = N y : e E | N e 1-1 V
7 f1domg V V x e E | N e ι y V | x = N y : e E | N e 1-1 V 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