Metamath Proof Explorer

Theorem iswspthsnon

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, 12-May-2021) (Revised by AV, 14-Mar-2022)

Ref Expression
Hypothesis iswspthsnon.v ⊢V=Vtx⁡G
Assertion iswspthsnon ⊢ANWSPathsNOnGB=w∈ANWWalksNOnGB|∃ffASPathsOn⁡GBw

Proof

Step Hyp Ref Expression
1 iswspthsnon.v ⊢V=Vtx⁡G
2 0ov ⊢A∅B=∅
3 df-wspthsnon ⊢WSPathsNOn=n∈ℕ0,g∈V⟼a∈Vtx⁡g,b∈Vtx⁡g⟼w∈anWWalksNOngb|∃ffaSPathsOn⁡gbw
4 3 mpondm0 ⊢¬N∈ℕ0∧G∈V→NWSPathsNOnG=∅
5 4 oveqd ⊢¬N∈ℕ0∧G∈V→ANWSPathsNOnGB=A∅B
6 id ⊢¬N∈ℕ0∧G∈V→¬N∈ℕ0∧G∈V
7 6 intnanrd ⊢¬N∈ℕ0∧G∈V→¬N∈ℕ0∧G∈V∧A∈V∧B∈V
8 1 wwlksnon0 ⊢¬N∈ℕ0∧G∈V∧A∈V∧B∈V→ANWWalksNOnGB=∅
9 7 8 syl ⊢¬N∈ℕ0∧G∈V→ANWWalksNOnGB=∅
10 9 rabeqdv ⊢¬N∈ℕ0∧G∈V→w∈ANWWalksNOnGB|∃ffASPathsOn⁡GBw=w∈∅|∃ffASPathsOn⁡GBw
11 rab0 ⊢w∈∅|∃ffASPathsOn⁡GBw=∅
12 10 11 eqtrdi ⊢¬N∈ℕ0∧G∈V→w∈ANWWalksNOnGB|∃ffASPathsOn⁡GBw=∅
13 2 5 12 3eqtr4a ⊢¬N∈ℕ0∧G∈V→ANWSPathsNOnGB=w∈ANWWalksNOnGB|∃ffASPathsOn⁡GBw
14 1 wspthsnon ⊢N∈ℕ0∧G∈V→NWSPathsNOnG=a∈V,b∈V⟼w∈aNWWalksNOnGb|∃ffaSPathsOn⁡Gbw
15 14 adantr ⊢N∈ℕ0∧G∈V∧¬A∈V∧B∈V→NWSPathsNOnG=a∈V,b∈V⟼w∈aNWWalksNOnGb|∃ffaSPathsOn⁡Gbw
16 15 oveqd ⊢N∈ℕ0∧G∈V∧¬A∈V∧B∈V→ANWSPathsNOnGB=Aa∈V,b∈V⟼w∈aNWWalksNOnGb|∃ffaSPathsOn⁡GbwB
17 eqid ⊢a∈V,b∈V⟼w∈aNWWalksNOnGb|∃ffaSPathsOn⁡Gbw=a∈V,b∈V⟼w∈aNWWalksNOnGb|∃ffaSPathsOn⁡Gbw
18 17 mpondm0 ⊢¬A∈V∧B∈V→Aa∈V,b∈V⟼w∈aNWWalksNOnGb|∃ffaSPathsOn⁡GbwB=∅
19 18 adantl ⊢N∈ℕ0∧G∈V∧¬A∈V∧B∈V→Aa∈V,b∈V⟼w∈aNWWalksNOnGb|∃ffaSPathsOn⁡GbwB=∅
20 16 19 eqtrd ⊢N∈ℕ0∧G∈V∧¬A∈V∧B∈V→ANWSPathsNOnGB=∅
21 20 ex ⊢N∈ℕ0∧G∈V→¬A∈V∧B∈V→ANWSPathsNOnGB=∅
22 5 2 eqtrdi ⊢¬N∈ℕ0∧G∈V→ANWSPathsNOnGB=∅
23 22 a1d ⊢¬N∈ℕ0∧G∈V→¬A∈V∧B∈V→ANWSPathsNOnGB=∅
24 21 23 pm2.61i ⊢¬A∈V∧B∈V→ANWSPathsNOnGB=∅
25 1 wwlksonvtx ⊢w∈ANWWalksNOnGB→A∈V∧B∈V
26 25 pm2.24d ⊢w∈ANWWalksNOnGB→¬A∈V∧B∈V→¬fASPathsOn⁡GBw
27 26 impcom ⊢¬A∈V∧B∈V∧w∈ANWWalksNOnGB→¬fASPathsOn⁡GBw
28 27 nexdv ⊢¬A∈V∧B∈V∧w∈ANWWalksNOnGB→¬∃ffASPathsOn⁡GBw
29 28 ralrimiva ⊢¬A∈V∧B∈V→∀w∈ANWWalksNOnGB¬∃ffASPathsOn⁡GBw
30 rabeq0 ⊢w∈ANWWalksNOnGB|∃ffASPathsOn⁡GBw=∅↔∀w∈ANWWalksNOnGB¬∃ffASPathsOn⁡GBw
31 29 30 sylibr ⊢¬A∈V∧B∈V→w∈ANWWalksNOnGB|∃ffASPathsOn⁡GBw=∅
32 24 31 eqtr4d ⊢¬A∈V∧B∈V→ANWSPathsNOnGB=w∈ANWWalksNOnGB|∃ffASPathsOn⁡GBw
33 14 adantr ⊢N∈ℕ0∧G∈V∧A∈V∧B∈V→NWSPathsNOnG=a∈V,b∈V⟼w∈aNWWalksNOnGb|∃ffaSPathsOn⁡Gbw
34 oveq12 ⊢a=A∧b=B→aNWWalksNOnGb=ANWWalksNOnGB
35 oveq12 ⊢a=A∧b=B→aSPathsOn⁡Gb=ASPathsOn⁡GB
36 35 breqd ⊢a=A∧b=B→faSPathsOn⁡Gbw↔fASPathsOn⁡GBw
37 36 exbidv ⊢a=A∧b=B→∃ffaSPathsOn⁡Gbw↔∃ffASPathsOn⁡GBw
38 34 37 rabeqbidv ⊢a=A∧b=B→w∈aNWWalksNOnGb|∃ffaSPathsOn⁡Gbw=w∈ANWWalksNOnGB|∃ffASPathsOn⁡GBw
39 38 adantl ⊢N∈ℕ0∧G∈V∧A∈V∧B∈V∧a=A∧b=B→w∈aNWWalksNOnGb|∃ffaSPathsOn⁡Gbw=w∈ANWWalksNOnGB|∃ffASPathsOn⁡GBw
40 simprl ⊢N∈ℕ0∧G∈V∧A∈V∧B∈V→A∈V
41 simprr ⊢N∈ℕ0∧G∈V∧A∈V∧B∈V→B∈V
42 ovex ⊢ANWWalksNOnGB∈V
43 42 rabex ⊢w∈ANWWalksNOnGB|∃ffASPathsOn⁡GBw∈V
44 43 a1i ⊢N∈ℕ0∧G∈V∧A∈V∧B∈V→w∈ANWWalksNOnGB|∃ffASPathsOn⁡GBw∈V
45 33 39 40 41 44 ovmpod ⊢N∈ℕ0∧G∈V∧A∈V∧B∈V→ANWSPathsNOnGB=w∈ANWWalksNOnGB|∃ffASPathsOn⁡GBw
46 13 32 45 ecase ⊢ANWSPathsNOnGB=w∈ANWWalksNOnGB|∃ffASPathsOn⁡GBw