Metamath Proof Explorer

Theorem wspthsnon

Description: The set of simple paths of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 1-Mar-2018) (Revised by AV, 11-May-2021)

Ref Expression
Hypothesis wwlksnon.v ⊢V=Vtx⁡G
Assertion wspthsnon ⊢N∈ℕ0∧G∈U→NWSPathsNOnG=a∈V,b∈V⟼w∈aNWWalksNOnGb|∃ffaSPathsOn⁡Gbw

Proof

Step Hyp Ref Expression
1 wwlksnon.v ⊢V=Vtx⁡G
2 df-wspthsnon ⊢WSPathsNOn=n∈ℕ0,g∈V⟼a∈Vtx⁡g,b∈Vtx⁡g⟼w∈anWWalksNOngb|∃ffaSPathsOn⁡gbw
3 2 a1i ⊢N∈ℕ0∧G∈U→WSPathsNOn=n∈ℕ0,g∈V⟼a∈Vtx⁡g,b∈Vtx⁡g⟼w∈anWWalksNOngb|∃ffaSPathsOn⁡gbw
4 fveq2 ⊢g=G→Vtx⁡g=Vtx⁡G
5 4 1 eqtr4di ⊢g=G→Vtx⁡g=V
6 5 adantl ⊢n=N∧g=G→Vtx⁡g=V
7 oveq12 ⊢n=N∧g=G→nWWalksNOng=NWWalksNOnG
8 7 oveqd ⊢n=N∧g=G→anWWalksNOngb=aNWWalksNOnGb
9 fveq2 ⊢g=G→SPathsOn⁡g=SPathsOn⁡G
10 9 oveqd ⊢g=G→aSPathsOn⁡gb=aSPathsOn⁡Gb
11 10 breqd ⊢g=G→faSPathsOn⁡gbw↔faSPathsOn⁡Gbw
12 11 adantl ⊢n=N∧g=G→faSPathsOn⁡gbw↔faSPathsOn⁡Gbw
13 12 exbidv ⊢n=N∧g=G→∃ffaSPathsOn⁡gbw↔∃ffaSPathsOn⁡Gbw
14 8 13 rabeqbidv ⊢n=N∧g=G→w∈anWWalksNOngb|∃ffaSPathsOn⁡gbw=w∈aNWWalksNOnGb|∃ffaSPathsOn⁡Gbw
15 6 6 14 mpoeq123dv ⊢n=N∧g=G→a∈Vtx⁡g,b∈Vtx⁡g⟼w∈anWWalksNOngb|∃ffaSPathsOn⁡gbw=a∈V,b∈V⟼w∈aNWWalksNOnGb|∃ffaSPathsOn⁡Gbw
16 15 adantl ⊢N∈ℕ0∧G∈U∧n=N∧g=G→a∈Vtx⁡g,b∈Vtx⁡g⟼w∈anWWalksNOngb|∃ffaSPathsOn⁡gbw=a∈V,b∈V⟼w∈aNWWalksNOnGb|∃ffaSPathsOn⁡Gbw
17 simpl ⊢N∈ℕ0∧G∈U→N∈ℕ0
18 elex ⊢G∈U→G∈V
19 18 adantl ⊢N∈ℕ0∧G∈U→G∈V
20 1 fvexi ⊢V∈V
21 20 20 mpoex ⊢a∈V,b∈V⟼w∈aNWWalksNOnGb|∃ffaSPathsOn⁡Gbw∈V
22 21 a1i ⊢N∈ℕ0∧G∈U→a∈V,b∈V⟼w∈aNWWalksNOnGb|∃ffaSPathsOn⁡Gbw∈V
23 3 16 17 19 22 ovmpod ⊢N∈ℕ0∧G∈U→NWSPathsNOnG=a∈V,b∈V⟼w∈aNWWalksNOnGb|∃ffaSPathsOn⁡Gbw