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=zN=y∈x∈dom⁡E|N∈E⁡x⟼ιz∈V|E⁡y=zN
6 1 2 4 5 usgredg2v ⊢G∈USGraph∧N∈V→y∈x∈dom⁡E|N∈E⁡x⟼ιz∈V|E⁡y=zN:x∈dom⁡E|N∈E⁡x⟶1-1V
7 f1domg ⊢V∈V→y∈x∈dom⁡E|N∈E⁡x⟼ιz∈V|E⁡y=zN:x∈dom⁡E|N∈E⁡x⟶1-1V→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