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∈ANWSPathsNOnGB→N∈ℕ0∧G∈V∧A∈V∧B∈V∧W∈ANWWalksNOnGB∧∃ffASPathsOn⁡GBW

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∈VVtx⁡g∈V∧Vtx⁡g∈V
5 df-wspthsnon ⊢WSPathsNOn=n∈ℕ0,g∈V⟼a∈Vtx⁡g,b∈Vtx⁡g⟼w∈anWWalksNOngb|∃ffaSPathsOn⁡gbw
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∈VVtx⁡g∈V∧Vtx⁡g∈V→W∈ANWSPathsNOnGB→N∈ℕ0∧G∈V∧A∈Vtx⁡G∧B∈Vtx⁡G
10 4 9 ax-mp ⊢W∈ANWSPathsNOnGB→N∈ℕ0∧G∈V∧A∈Vtx⁡G∧B∈Vtx⁡G
11 simprl ⊢W∈ANWSPathsNOnGB∧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∈ANWSPathsNOnGB∧N∈ℕ0∧G∈V∧A∈Vtx⁡G∧B∈Vtx⁡G→A∈V∧B∈V
18 wspthnon ⊢W∈ANWSPathsNOnGB↔W∈ANWWalksNOnGB∧∃ffASPathsOn⁡GBW
19 18 biimpi ⊢W∈ANWSPathsNOnGB→W∈ANWWalksNOnGB∧∃ffASPathsOn⁡GBW
20 19 adantr ⊢W∈ANWSPathsNOnGB∧N∈ℕ0∧G∈V∧A∈Vtx⁡G∧B∈Vtx⁡G→W∈ANWWalksNOnGB∧∃ffASPathsOn⁡GBW
21 11 17 20 3jca ⊢W∈ANWSPathsNOnGB∧N∈ℕ0∧G∈V∧A∈Vtx⁡G∧B∈Vtx⁡G→N∈ℕ0∧G∈V∧A∈V∧B∈V∧W∈ANWWalksNOnGB∧∃ffASPathsOn⁡GBW
22 10 21 mpdan ⊢W∈ANWSPathsNOnGB→N∈ℕ0∧G∈V∧A∈V∧B∈V∧W∈ANWWalksNOnGB∧∃ffASPathsOn⁡GBW