Step |
Hyp |
Ref |
Expression |
1 |
|
1wlkd.p |
⊢ 𝑃 = 〈“ 𝑋 𝑌 ”〉 |
2 |
|
1wlkd.f |
⊢ 𝐹 = 〈“ 𝐽 ”〉 |
3 |
|
1wlkd.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝑉 ) |
4 |
|
1wlkd.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝑉 ) |
5 |
|
1wlkd.l |
⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝐼 ‘ 𝐽 ) = { 𝑋 } ) |
6 |
|
1wlkd.j |
⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → { 𝑋 , 𝑌 } ⊆ ( 𝐼 ‘ 𝐽 ) ) |
7 |
|
1wlkd.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
8 |
|
1wlkd.i |
⊢ 𝐼 = ( iEdg ‘ 𝐺 ) |
9 |
1 2 3 4 5 6 7 8
|
1wlkd |
⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) |
10 |
1
|
fveq1i |
⊢ ( 𝑃 ‘ 0 ) = ( 〈“ 𝑋 𝑌 ”〉 ‘ 0 ) |
11 |
|
s2fv0 |
⊢ ( 𝑋 ∈ 𝑉 → ( 〈“ 𝑋 𝑌 ”〉 ‘ 0 ) = 𝑋 ) |
12 |
10 11
|
syl5eq |
⊢ ( 𝑋 ∈ 𝑉 → ( 𝑃 ‘ 0 ) = 𝑋 ) |
13 |
3 12
|
syl |
⊢ ( 𝜑 → ( 𝑃 ‘ 0 ) = 𝑋 ) |
14 |
2
|
fveq2i |
⊢ ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 〈“ 𝐽 ”〉 ) |
15 |
|
s1len |
⊢ ( ♯ ‘ 〈“ 𝐽 ”〉 ) = 1 |
16 |
14 15
|
eqtri |
⊢ ( ♯ ‘ 𝐹 ) = 1 |
17 |
1 16
|
fveq12i |
⊢ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 〈“ 𝑋 𝑌 ”〉 ‘ 1 ) |
18 |
|
s2fv1 |
⊢ ( 𝑌 ∈ 𝑉 → ( 〈“ 𝑋 𝑌 ”〉 ‘ 1 ) = 𝑌 ) |
19 |
4 18
|
syl |
⊢ ( 𝜑 → ( 〈“ 𝑋 𝑌 ”〉 ‘ 1 ) = 𝑌 ) |
20 |
17 19
|
syl5eq |
⊢ ( 𝜑 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝑌 ) |
21 |
|
wlkv |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) |
22 |
|
3simpc |
⊢ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) |
23 |
9 21 22
|
3syl |
⊢ ( 𝜑 → ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) |
24 |
3 4 23
|
jca31 |
⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) |
25 |
7
|
iswlkon |
⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( 𝐹 ( 𝑋 ( WalksOn ‘ 𝐺 ) 𝑌 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝑋 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝑌 ) ) ) |
26 |
24 25
|
syl |
⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( WalksOn ‘ 𝐺 ) 𝑌 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝑋 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝑌 ) ) ) |
27 |
9 13 20 26
|
mpbir3and |
⊢ ( 𝜑 → 𝐹 ( 𝑋 ( WalksOn ‘ 𝐺 ) 𝑌 ) 𝑃 ) |
28 |
1 2 3 4 5 6 7 8
|
1trld |
⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) |
29 |
7
|
istrlson |
⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( 𝐹 ( 𝑋 ( TrailsOn ‘ 𝐺 ) 𝑌 ) 𝑃 ↔ ( 𝐹 ( 𝑋 ( WalksOn ‘ 𝐺 ) 𝑌 ) 𝑃 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) ) ) |
30 |
24 29
|
syl |
⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( TrailsOn ‘ 𝐺 ) 𝑌 ) 𝑃 ↔ ( 𝐹 ( 𝑋 ( WalksOn ‘ 𝐺 ) 𝑌 ) 𝑃 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) ) ) |
31 |
27 28 30
|
mpbir2and |
⊢ ( 𝜑 → 𝐹 ( 𝑋 ( TrailsOn ‘ 𝐺 ) 𝑌 ) 𝑃 ) |
32 |
1 2 3 4 5 6 7 8
|
1pthd |
⊢ ( 𝜑 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) |
33 |
3
|
adantl |
⊢ ( ( ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝜑 ) → 𝑋 ∈ 𝑉 ) |
34 |
4
|
adantl |
⊢ ( ( ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝜑 ) → 𝑌 ∈ 𝑉 ) |
35 |
|
simpl |
⊢ ( ( ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝜑 ) → ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) |
36 |
33 34 35
|
jca31 |
⊢ ( ( ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝜑 ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) |
37 |
36
|
ex |
⊢ ( ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( 𝜑 → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) ) |
38 |
21 22 37
|
3syl |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝜑 → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) ) |
39 |
9 38
|
mpcom |
⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) |
40 |
7
|
ispthson |
⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( 𝐹 ( 𝑋 ( PathsOn ‘ 𝐺 ) 𝑌 ) 𝑃 ↔ ( 𝐹 ( 𝑋 ( TrailsOn ‘ 𝐺 ) 𝑌 ) 𝑃 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ) ) |
41 |
39 40
|
syl |
⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( PathsOn ‘ 𝐺 ) 𝑌 ) 𝑃 ↔ ( 𝐹 ( 𝑋 ( TrailsOn ‘ 𝐺 ) 𝑌 ) 𝑃 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ) ) |
42 |
31 32 41
|
mpbir2and |
⊢ ( 𝜑 → 𝐹 ( 𝑋 ( PathsOn ‘ 𝐺 ) 𝑌 ) 𝑃 ) |