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

Metamath Proof Explorer

Theorem wpthswwlks2on

Description: For two different vertices, a walk of length 2 between these vertices is a simple path of length 2 between these vertices in a simple graph. (Contributed by Alexander van der Vekens, 2-Mar-2018) (Revised by AV, 16-Mar-2022) (Revised by Ender Ting, 29-Jan-2026)

Ref Expression
Assertion wpthswwlks2on ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐵 ) = ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) )

Proof

Step Hyp Ref Expression
1 wwlknon ⊢ ( 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ↔ ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) )
2 1 a1i ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ↔ ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) )
3 2 anbi1d ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ↔ ( ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) )
4 3anass ⊢ ( ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ↔ ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) )
5 4 anbi1i ⊢ ( ( ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ↔ ( ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) )
6 anass ⊢ ( ( ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ↔ ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) )
7 5 6 bitri ⊢ ( ( ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ↔ ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) )
8 3 7 bitrdi ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ↔ ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) ) )
9 8 rabbidva2 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → { 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∣ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 } = { 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∣ ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) } )
10 usgruspgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ USPGraph )
11 wlklnwwlkn ⊢ ( 𝐺 ∈ USPGraph → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ↔ 𝑤 ∈ ( 2 WWalksN 𝐺 ) ) )
12 10 11 syl ⊢ ( 𝐺 ∈ USGraph → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ↔ 𝑤 ∈ ( 2 WWalksN 𝐺 ) ) )
13 12 bicomd ⊢ ( 𝐺 ∈ USGraph → ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ↔ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
14 13 adantr ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ↔ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
15 simprl ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → 𝑓 ( Walks ‘ 𝐺 ) 𝑤 )
16 simprl ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) → ( 𝑤 ‘ 0 ) = 𝐴 )
17 16 adantr ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝑤 ‘ 0 ) = 𝐴 )
18 fveq2 ⊢ ( ( ♯ ‘ 𝑓 ) = 2 → ( 𝑤 ‘ ( ♯ ‘ 𝑓 ) ) = ( 𝑤 ‘ 2 ) )
19 18 ad2antll ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝑤 ‘ ( ♯ ‘ 𝑓 ) ) = ( 𝑤 ‘ 2 ) )
20 simprr ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) → ( 𝑤 ‘ 2 ) = 𝐵 )
21 20 adantr ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝑤 ‘ 2 ) = 𝐵 )
22 19 21 eqtrd ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝑤 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 )
23 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
24 23 wlkp ⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 → 𝑤 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
25 oveq2 ⊢ ( ( ♯ ‘ 𝑓 ) = 2 → ( 0 ... ( ♯ ‘ 𝑓 ) ) = ( 0 ... 2 ) )
26 25 feq2d ⊢ ( ( ♯ ‘ 𝑓 ) = 2 → ( 𝑤 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ↔ 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) ) )
27 24 26 syl5ibcom ⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 → ( ( ♯ ‘ 𝑓 ) = 2 → 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) ) )
28 27 imp ⊢ ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) )
29 id ⊢ ( 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) → 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) )
30 2nn0 ⊢ 2 ∈ ℕ0
31 0elfz ⊢ ( 2 ∈ ℕ0 → 0 ∈ ( 0 ... 2 ) )
32 30 31 mp1i ⊢ ( 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) → 0 ∈ ( 0 ... 2 ) )
33 29 32 ffvelcdmd ⊢ ( 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) → ( 𝑤 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) )
34 nn0fz0 ⊢ ( 2 ∈ ℕ0 ↔ 2 ∈ ( 0 ... 2 ) )
35 30 34 mpbi ⊢ 2 ∈ ( 0 ... 2 )
36 35 a1i ⊢ ( 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) → 2 ∈ ( 0 ... 2 ) )
37 29 36 ffvelcdmd ⊢ ( 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) → ( 𝑤 ‘ 2 ) ∈ ( Vtx ‘ 𝐺 ) )
38 33 37 jca ⊢ ( 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( 𝑤 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑤 ‘ 2 ) ∈ ( Vtx ‘ 𝐺 ) ) )
39 28 38 syl ⊢ ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ( ( 𝑤 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑤 ‘ 2 ) ∈ ( Vtx ‘ 𝐺 ) ) )
40 eleq1 ⊢ ( ( 𝑤 ‘ 0 ) = 𝐴 → ( ( 𝑤 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ↔ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) )
41 eleq1 ⊢ ( ( 𝑤 ‘ 2 ) = 𝐵 → ( ( 𝑤 ‘ 2 ) ∈ ( Vtx ‘ 𝐺 ) ↔ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) )
42 40 41 bi2anan9 ⊢ ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) → ( ( ( 𝑤 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑤 ‘ 2 ) ∈ ( Vtx ‘ 𝐺 ) ) ↔ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) )
43 39 42 imbitrid ⊢ ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) → ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) )
44 43 adantl ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) → ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) )
45 44 imp ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) )
46 vex ⊢ 𝑓 ∈ V
47 vex ⊢ 𝑤 ∈ V
48 46 47 pm3.2i ⊢ ( 𝑓 ∈ V ∧ 𝑤 ∈ V )
49 23 iswlkon ⊢ ( ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑓 ∈ V ∧ 𝑤 ∈ V ) ) → ( 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑤 ↔ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) ) )
50 45 48 49 sylancl ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑤 ↔ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) ) )
51 15 17 22 50 mpbir3and ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑤 )
52 simplll ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → 𝐺 ∈ USGraph )
53 simprr ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( ♯ ‘ 𝑓 ) = 2 )
54 simpllr ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → 𝐴 ≠ 𝐵 )
55 usgr2wlkspth ⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ 𝐴 ≠ 𝐵 ) → ( 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑤 ↔ 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) )
56 52 53 54 55 syl3anc ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑤 ↔ 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) )
57 51 56 mpbid ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 )
58 57 ex ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) → ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) )
59 58 eximdv ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) )
60 59 ex ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) )
61 60 com23 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) → ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) )
62 14 61 sylbid ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) → ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) → ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) )
63 62 imp ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑤 ∈ ( 2 WWalksN 𝐺 ) ) → ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) → ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) )
64 63 pm4.71d ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑤 ∈ ( 2 WWalksN 𝐺 ) ) → ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ↔ ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) )
65 64 bicomd ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑤 ∈ ( 2 WWalksN 𝐺 ) ) → ( ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ↔ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) )
66 65 rabbidva ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → { 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∣ ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) } = { 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) } )
67 9 66 eqtrd ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → { 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∣ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 } = { 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) } )
68 23 iswspthsnon ⊢ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐵 ) = { 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∣ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 }
69 23 iswwlksnon ⊢ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) = { 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) }
70 67 68 69 3eqtr4g ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐵 ) = ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) )