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

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 usgrupgr ( 𝐺 ∈ USGraph → 𝐺 ∈ UPGraph )
11 wlklnwwlknupgr ( 𝐺 ∈ UPGraph → ( ∃ 𝑓 ( 𝑓 ( 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 ffvelrnd ( 𝑤 : ( 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 ffvelrnd ( 𝑤 : ( 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 syl5ib ( ( ( 𝑤 ‘ 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 𝐺 ) 𝐵 ) )