Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
2 |
1
|
wlkp |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) |
3 |
|
fdm |
⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → dom 𝑃 = ( 0 ... ( ♯ ‘ 𝐹 ) ) ) |
4 |
3
|
eqcomd |
⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( 0 ... ( ♯ ‘ 𝐹 ) ) = dom 𝑃 ) |
5 |
2 4
|
syl |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 0 ... ( ♯ ‘ 𝐹 ) ) = dom 𝑃 ) |
6 |
|
wlkcl |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) |
7 |
|
elnn0uz |
⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 0 ) ) |
8 |
|
fzn0 |
⊢ ( ( 0 ... ( ♯ ‘ 𝐹 ) ) ≠ ∅ ↔ ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 0 ) ) |
9 |
7 8
|
sylbb2 |
⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 0 ... ( ♯ ‘ 𝐹 ) ) ≠ ∅ ) |
10 |
6 9
|
syl |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 0 ... ( ♯ ‘ 𝐹 ) ) ≠ ∅ ) |
11 |
5 10
|
eqnetrrd |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → dom 𝑃 ≠ ∅ ) |
12 |
|
frel |
⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → Rel 𝑃 ) |
13 |
2 12
|
syl |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → Rel 𝑃 ) |
14 |
|
reldm0 |
⊢ ( Rel 𝑃 → ( 𝑃 = ∅ ↔ dom 𝑃 = ∅ ) ) |
15 |
14
|
necon3bid |
⊢ ( Rel 𝑃 → ( 𝑃 ≠ ∅ ↔ dom 𝑃 ≠ ∅ ) ) |
16 |
13 15
|
syl |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝑃 ≠ ∅ ↔ dom 𝑃 ≠ ∅ ) ) |
17 |
11 16
|
mpbird |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 ≠ ∅ ) |