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 ◡ 𝑃 ) |