Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
2 |
1
|
wlkonprop |
⊢ ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( ( 𝐺 ∈ V ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) ) |
3 |
|
fveqeq2 |
⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ( ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ↔ ( 𝑃 ‘ 0 ) = 𝐵 ) ) |
4 |
3
|
anbi2d |
⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ↔ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 0 ) = 𝐵 ) ) ) |
5 |
|
eqtr2 |
⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 0 ) = 𝐵 ) → 𝐴 = 𝐵 ) |
6 |
|
nne |
⊢ ( ¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵 ) |
7 |
5 6
|
sylibr |
⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 0 ) = 𝐵 ) → ¬ 𝐴 ≠ 𝐵 ) |
8 |
4 7
|
syl6bi |
⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ¬ 𝐴 ≠ 𝐵 ) ) |
9 |
8
|
com12 |
⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( ( ♯ ‘ 𝐹 ) = 0 → ¬ 𝐴 ≠ 𝐵 ) ) |
10 |
9
|
3adant1 |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( ( ♯ ‘ 𝐹 ) = 0 → ¬ 𝐴 ≠ 𝐵 ) ) |
11 |
10
|
3ad2ant3 |
⊢ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) → ( ( ♯ ‘ 𝐹 ) = 0 → ¬ 𝐴 ≠ 𝐵 ) ) |
12 |
2 11
|
syl |
⊢ ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( ( ♯ ‘ 𝐹 ) = 0 → ¬ 𝐴 ≠ 𝐵 ) ) |
13 |
12
|
necon2ad |
⊢ ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( 𝐴 ≠ 𝐵 → ( ♯ ‘ 𝐹 ) ≠ 0 ) ) |
14 |
13
|
imp |
⊢ ( ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐴 ≠ 𝐵 ) → ( ♯ ‘ 𝐹 ) ≠ 0 ) |