| Step |
Hyp |
Ref |
Expression |
| 1 |
|
simp1 |
⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → 𝐺 ∈ USGraph ) |
| 2 |
1
|
anim2i |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐺 ∈ USGraph ) ) |
| 3 |
2
|
ancomd |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝐺 ∈ USGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) ) |
| 4 |
|
3simpc |
⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) |
| 5 |
4
|
adantl |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) |
| 6 |
|
usgr2wlkneq |
⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) ∧ ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 1 ) ) ) |
| 7 |
3 5 6
|
syl2anc |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 1 ) ) ) |
| 8 |
|
simpl |
⊢ ( ( ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 1 ) ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) ) |
| 9 |
|
fvex |
⊢ ( 𝑃 ‘ 0 ) ∈ V |
| 10 |
|
fvex |
⊢ ( 𝑃 ‘ 1 ) ∈ V |
| 11 |
|
fvex |
⊢ ( 𝑃 ‘ 2 ) ∈ V |
| 12 |
9 10 11
|
3pm3.2i |
⊢ ( ( 𝑃 ‘ 0 ) ∈ V ∧ ( 𝑃 ‘ 1 ) ∈ V ∧ ( 𝑃 ‘ 2 ) ∈ V ) |
| 13 |
8 12
|
jctil |
⊢ ( ( ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 1 ) ) → ( ( ( 𝑃 ‘ 0 ) ∈ V ∧ ( 𝑃 ‘ 1 ) ∈ V ∧ ( 𝑃 ‘ 2 ) ∈ V ) ∧ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) |
| 14 |
|
funcnvs3 |
⊢ ( ( ( ( 𝑃 ‘ 0 ) ∈ V ∧ ( 𝑃 ‘ 1 ) ∈ V ∧ ( 𝑃 ‘ 2 ) ∈ V ) ∧ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) ) → Fun ◡ ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ( 𝑃 ‘ 2 ) ”⟩ ) |
| 15 |
7 13 14
|
3syl |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → Fun ◡ ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ( 𝑃 ‘ 2 ) ”⟩ ) |
| 16 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
| 17 |
16
|
wlkpwrd |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) |
| 18 |
|
wlklenvp1 |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) |
| 19 |
|
oveq1 |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ( ♯ ‘ 𝐹 ) + 1 ) = ( 2 + 1 ) ) |
| 20 |
|
2p1e3 |
⊢ ( 2 + 1 ) = 3 |
| 21 |
19 20
|
eqtrdi |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ( ♯ ‘ 𝐹 ) + 1 ) = 3 ) |
| 22 |
21
|
3ad2ant2 |
⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( ♯ ‘ 𝐹 ) + 1 ) = 3 ) |
| 23 |
18 22
|
sylan9eq |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( ♯ ‘ 𝑃 ) = 3 ) |
| 24 |
|
wrdlen3s3 |
⊢ ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 3 ) → 𝑃 = ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ( 𝑃 ‘ 2 ) ”⟩ ) |
| 25 |
17 23 24
|
syl2an2r |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → 𝑃 = ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ( 𝑃 ‘ 2 ) ”⟩ ) |
| 26 |
25
|
cnveqd |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ◡ 𝑃 = ◡ ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ( 𝑃 ‘ 2 ) ”⟩ ) |
| 27 |
26
|
funeqd |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( Fun ◡ 𝑃 ↔ Fun ◡ ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ( 𝑃 ‘ 2 ) ”⟩ ) ) |
| 28 |
15 27
|
mpbird |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → Fun ◡ 𝑃 ) |