Metamath Proof Explorer

Theorem wspthnonp

Description: Properties of a set being a simple path of a fixed length between two vertices as word. (Contributed by AV, 14-May-2021) (Proof shortened by AV, 15-Mar-2022)

Ref Expression
Hypothesis wspthnonp.v ⊢ V = Vtx ⁡ G
Assertion wspthnonp ⊢ W ∈ A N WSPathsNOn G B → N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ W ∈ A N WWalksNOn G B ∧ ∃ f f A SPathsOn ⁡ G B W

Proof

Step Hyp Ref Expression
1 wspthnonp.v ⊢ V = Vtx ⁡ G
2 fvex ⊢ Vtx ⁡ g ∈ V
3 2 2 pm3.2i ⊢ Vtx ⁡ g ∈ V ∧ Vtx ⁡ g ∈ V
4 3 rgen2w ⊢ ∀ n ∈ ℕ 0 ∀ g ∈ V Vtx ⁡ g ∈ V ∧ Vtx ⁡ g ∈ V
5 df-wspthsnon ⊢ WSPathsNOn = n ∈ ℕ 0 , g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ w ∈ a n WWalksNOn g b | ∃ f f a SPathsOn ⁡ g b w
6 fveq2 ⊢ g = G → Vtx ⁡ g = Vtx ⁡ G
7 6 6 jca ⊢ g = G → Vtx ⁡ g = Vtx ⁡ G ∧ Vtx ⁡ g = Vtx ⁡ G
8 7 adantl ⊢ n = N ∧ g = G → Vtx ⁡ g = Vtx ⁡ G ∧ Vtx ⁡ g = Vtx ⁡ G
9 5 8 el2mpocl ⊢ ∀ n ∈ ℕ 0 ∀ g ∈ V Vtx ⁡ g ∈ V ∧ Vtx ⁡ g ∈ V → W ∈ A N WSPathsNOn G B → N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G
10 4 9 ax-mp ⊢ W ∈ A N WSPathsNOn G B → N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G
11 simprl ⊢ W ∈ A N WSPathsNOn G B ∧ N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G → N ∈ ℕ 0 ∧ G ∈ V
12 1 eleq2i ⊢ A ∈ V ↔ A ∈ Vtx ⁡ G
13 1 eleq2i ⊢ B ∈ V ↔ B ∈ Vtx ⁡ G
14 12 13 anbi12i ⊢ A ∈ V ∧ B ∈ V ↔ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G
15 14 biimpri ⊢ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G → A ∈ V ∧ B ∈ V
16 15 adantl ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G → A ∈ V ∧ B ∈ V
17 16 adantl ⊢ W ∈ A N WSPathsNOn G B ∧ N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G → A ∈ V ∧ B ∈ V
18 wspthnon ⊢ W ∈ A N WSPathsNOn G B ↔ W ∈ A N WWalksNOn G B ∧ ∃ f f A SPathsOn ⁡ G B W
19 18 biimpi ⊢ W ∈ A N WSPathsNOn G B → W ∈ A N WWalksNOn G B ∧ ∃ f f A SPathsOn ⁡ G B W
20 19 adantr ⊢ W ∈ A N WSPathsNOn G B ∧ N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G → W ∈ A N WWalksNOn G B ∧ ∃ f f A SPathsOn ⁡ G B W
21 11 17 20 3jca ⊢ W ∈ A N WSPathsNOn G B ∧ N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G → N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ W ∈ A N WWalksNOn G B ∧ ∃ f f A SPathsOn ⁡ G B W
22 10 21 mpdan ⊢ W ∈ A N WSPathsNOn G B → N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ W ∈ A N WWalksNOn G B ∧ ∃ f f A SPathsOn ⁡ G B W