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

Metamath Proof Explorer

Theorem g0wlk0

Description: There is no walk in a null graph (a class without vertices). (Contributed by Alexander van der Vekens, 2-Sep-2018) (Revised by AV, 5-Mar-2021)

Ref Expression
Assertion g0wlk0 ⊢ Vtx ⁡ G = ∅ → Walks ⁡ G = ∅

Proof

Step Hyp Ref Expression
1 ax-1 ⊢ Walks ⁡ G = ∅ → Vtx ⁡ G = ∅ → Walks ⁡ G = ∅
2 neq0 ⊢ ¬ Walks ⁡ G = ∅ ↔ ∃ w w ∈ Walks ⁡ G
3 wlkv0 ⊢ Vtx ⁡ G = ∅ ∧ w ∈ Walks ⁡ G → 1 st ⁡ w = ∅ ∧ 2 nd ⁡ w = ∅
4 wlkcpr ⊢ w ∈ Walks ⁡ G ↔ 1 st ⁡ w Walks ⁡ G 2 nd ⁡ w
5 wlkn0 ⊢ 1 st ⁡ w Walks ⁡ G 2 nd ⁡ w → 2 nd ⁡ w ≠ ∅
6 eqneqall ⊢ 2 nd ⁡ w = ∅ → 2 nd ⁡ w ≠ ∅ → Walks ⁡ G = ∅
7 6 adantl ⊢ 1 st ⁡ w = ∅ ∧ 2 nd ⁡ w = ∅ → 2 nd ⁡ w ≠ ∅ → Walks ⁡ G = ∅
8 5 7 syl5com ⊢ 1 st ⁡ w Walks ⁡ G 2 nd ⁡ w → 1 st ⁡ w = ∅ ∧ 2 nd ⁡ w = ∅ → Walks ⁡ G = ∅
9 4 8 sylbi ⊢ w ∈ Walks ⁡ G → 1 st ⁡ w = ∅ ∧ 2 nd ⁡ w = ∅ → Walks ⁡ G = ∅
10 9 adantl ⊢ Vtx ⁡ G = ∅ ∧ w ∈ Walks ⁡ G → 1 st ⁡ w = ∅ ∧ 2 nd ⁡ w = ∅ → Walks ⁡ G = ∅
11 3 10 mpd ⊢ Vtx ⁡ G = ∅ ∧ w ∈ Walks ⁡ G → Walks ⁡ G = ∅
12 11 expcom ⊢ w ∈ Walks ⁡ G → Vtx ⁡ G = ∅ → Walks ⁡ G = ∅
13 12 exlimiv ⊢ ∃ w w ∈ Walks ⁡ G → Vtx ⁡ G = ∅ → Walks ⁡ G = ∅
14 2 13 sylbi ⊢ ¬ Walks ⁡ G = ∅ → Vtx ⁡ G = ∅ → Walks ⁡ G = ∅
15 1 14 pm2.61i ⊢ Vtx ⁡ G = ∅ → Walks ⁡ G = ∅