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 onto e ∈ 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