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