Metamath Proof Explorer

Theorem usgredgleordALT

Description: Alternate proof for usgredgleord based on usgriedgleord . 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) (Proof shortened by AV, 5-May-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses usgredgleord.v ⊢V=Vtx⁡G
usgredgleord.e ⊢E=Edg⁡G
Assertion usgredgleordALT ⊢G∈USGraph∧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 fvex ⊢iEdg⁡G∈V
4 3 dmex ⊢dom⁡iEdg⁡G∈V
5 4 rabex ⊢x∈dom⁡iEdg⁡G|N∈iEdg⁡G⁡x∈V
6 5 a1i ⊢G∈USGraph∧N∈V→x∈dom⁡iEdg⁡G|N∈iEdg⁡G⁡x∈V
7 eqid ⊢iEdg⁡G=iEdg⁡G
8 eqid ⊢x∈dom⁡iEdg⁡G|N∈iEdg⁡G⁡x=x∈dom⁡iEdg⁡G|N∈iEdg⁡G⁡x
9 eleq2w ⊢e=f→N∈e↔N∈f
10 9 cbvrabv ⊢e∈E|N∈e=f∈E|N∈f
11 eqid ⊢y∈x∈dom⁡iEdg⁡G|N∈iEdg⁡G⁡x⟼iEdg⁡G⁡y=y∈x∈dom⁡iEdg⁡G|N∈iEdg⁡G⁡x⟼iEdg⁡G⁡y
12 2 7 1 8 10 11 usgredgedg ⊢G∈USGraph∧N∈V→y∈x∈dom⁡iEdg⁡G|N∈iEdg⁡G⁡x⟼iEdg⁡G⁡y:x∈dom⁡iEdg⁡G|N∈iEdg⁡G⁡x⟶1-1 ontoe∈E|N∈e
13 6 12 hasheqf1od ⊢G∈USGraph∧N∈V→x∈dom⁡iEdg⁡G|N∈iEdg⁡G⁡x=e∈E|N∈e
14 1 7 usgriedgleord ⊢G∈USGraph∧N∈V→x∈dom⁡iEdg⁡G|N∈iEdg⁡G⁡x≤V
15 13 14 eqbrtrrd ⊢G∈USGraph∧N∈V→e∈E|N∈e≤V