This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem usgrvd0nedg

Description: If a vertex in a simple graph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 16-Dec-2020) (Proof shortened by AV, 23-Dec-2020)

Ref Expression
Hypotheses vtxdusgradjvtx.v ⊢ V = Vtx ⁡ G
vtxdusgradjvtx.e ⊢ E = Edg ⁡ G
Assertion usgrvd0nedg ⊢ G ∈ USGraph ∧ U ∈ V → VtxDeg ⁡ G ⁡ U = 0 → ¬ ∃ v ∈ V U v ∈ E

Proof

Step Hyp Ref Expression
1 vtxdusgradjvtx.v ⊢ V = Vtx ⁡ G
2 vtxdusgradjvtx.e ⊢ E = Edg ⁡ G
3 1 2 vtxdusgradjvtx ⊢ G ∈ USGraph ∧ U ∈ V → VtxDeg ⁡ G ⁡ U = v ∈ V | U v ∈ E
4 3 eqeq1d ⊢ G ∈ USGraph ∧ U ∈ V → VtxDeg ⁡ G ⁡ U = 0 ↔ v ∈ V | U v ∈ E = 0
5 1 fvexi ⊢ V ∈ V
6 5 rabex ⊢ v ∈ V | U v ∈ E ∈ V
7 hasheq0 ⊢ v ∈ V | U v ∈ E ∈ V → v ∈ V | U v ∈ E = 0 ↔ v ∈ V | U v ∈ E = ∅
8 6 7 ax-mp ⊢ v ∈ V | U v ∈ E = 0 ↔ v ∈ V | U v ∈ E = ∅
9 rabeq0 ⊢ v ∈ V | U v ∈ E = ∅ ↔ ∀ v ∈ V ¬ U v ∈ E
10 ralnex ⊢ ∀ v ∈ V ¬ U v ∈ E ↔ ¬ ∃ v ∈ V U v ∈ E
11 10 biimpi ⊢ ∀ v ∈ V ¬ U v ∈ E → ¬ ∃ v ∈ V U v ∈ E
12 11 a1i ⊢ G ∈ USGraph ∧ U ∈ V → ∀ v ∈ V ¬ U v ∈ E → ¬ ∃ v ∈ V U v ∈ E
13 9 12 biimtrid ⊢ G ∈ USGraph ∧ U ∈ V → v ∈ V | U v ∈ E = ∅ → ¬ ∃ v ∈ V U v ∈ E
14 8 13 biimtrid ⊢ G ∈ USGraph ∧ U ∈ V → v ∈ V | U v ∈ E = 0 → ¬ ∃ v ∈ V U v ∈ E
15 4 14 sylbid ⊢ G ∈ USGraph ∧ U ∈ V → VtxDeg ⁡ G ⁡ U = 0 → ¬ ∃ v ∈ V U v ∈ E