Metamath Proof Explorer

Theorem vtxdusgr0edgnelALT

Description: Alternate proof of vtxdusgr0edgnel , not based on vtxduhgr0edgnel . A vertex in a simple graph has degree 0 if there is no edge incident with this vertex. (Contributed by AV, 17-Dec-2020) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses vtxdushgrfvedg.v ⊢ V = Vtx ⁡ G
vtxdushgrfvedg.e ⊢ E = Edg ⁡ G
vtxdushgrfvedg.d ⊢ D = VtxDeg ⁡ G
Assertion vtxdusgr0edgnelALT ⊢ G ∈ USGraph ∧ U ∈ V → D ⁡ U = 0 ↔ ¬ ∃ e ∈ E U ∈ e

Proof

Step Hyp Ref Expression
1 vtxdushgrfvedg.v ⊢ V = Vtx ⁡ G
2 vtxdushgrfvedg.e ⊢ E = Edg ⁡ G
3 vtxdushgrfvedg.d ⊢ D = VtxDeg ⁡ G
4 1 2 3 vtxdusgrfvedg ⊢ G ∈ USGraph ∧ U ∈ V → D ⁡ U = e ∈ E | U ∈ e
5 4 eqeq1d ⊢ G ∈ USGraph ∧ U ∈ V → D ⁡ U = 0 ↔ e ∈ E | U ∈ e = 0
6 fvex ⊢ Edg ⁡ G ∈ V
7 2 6 eqeltri ⊢ E ∈ V
8 7 rabex ⊢ e ∈ E | U ∈ e ∈ V
9 hasheq0 ⊢ e ∈ E | U ∈ e ∈ V → e ∈ E | U ∈ e = 0 ↔ e ∈ E | U ∈ e = ∅
10 8 9 mp1i ⊢ G ∈ USGraph ∧ U ∈ V → e ∈ E | U ∈ e = 0 ↔ e ∈ E | U ∈ e = ∅
11 rabeq0 ⊢ e ∈ E | U ∈ e = ∅ ↔ ∀ e ∈ E ¬ U ∈ e
12 ralnex ⊢ ∀ e ∈ E ¬ U ∈ e ↔ ¬ ∃ e ∈ E U ∈ e
13 12 a1i ⊢ G ∈ USGraph ∧ U ∈ V → ∀ e ∈ E ¬ U ∈ e ↔ ¬ ∃ e ∈ E U ∈ e
14 11 13 bitrid ⊢ G ∈ USGraph ∧ U ∈ V → e ∈ E | U ∈ e = ∅ ↔ ¬ ∃ e ∈ E U ∈ e
15 5 10 14 3bitrd ⊢ G ∈ USGraph ∧ U ∈ V → D ⁡ U = 0 ↔ ¬ ∃ e ∈ E U ∈ e