Metamath Proof Explorer

Theorem usgriedgleord

Description: Alternate version of usgredgleord , not using the notation ( EdgG ) . In a simple graph 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, 18-Oct-2020)

Ref Expression
Hypotheses usgredg2v.v ⊢ V = Vtx ⁡ G
usgredg2v.e ⊢ E = iEdg ⁡ G
Assertion usgriedgleord ⊢ G ∈ USGraph ∧ N ∈ V → x ∈ dom ⁡ E | N ∈ E ⁡ x ≤ V

Proof

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