Proof of Theorem spthonepeq
Step | Hyp | Ref
| Expression |
1 | | spthonprp 26115 |
. 2
⊢ (𝐹(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑃 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 ∧ 𝐹(𝑉 SPaths 𝐸)𝑃))) |
2 | | iswlkon 26062 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 ↔ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵))) |
3 | | isspth 26099 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 SPaths 𝐸)𝑃 ↔ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃))) |
4 | 3 | 3adant3 1074 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹(𝑉 SPaths 𝐸)𝑃 ↔ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃))) |
5 | 2, 4 | anbi12d 743 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → ((𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 ∧ 𝐹(𝑉 SPaths 𝐸)𝑃) ↔ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) ∧ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃)))) |
6 | | 2mwlk 26049 |
. . . . . . . 8
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) |
7 | | lencl 13179 |
. . . . . . . . 9
⊢ (𝐹 ∈ Word dom 𝐸 → (#‘𝐹) ∈
ℕ0) |
8 | 7 | anim1i 590 |
. . . . . . . 8
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → ((#‘𝐹) ∈ ℕ0 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) |
9 | | df-f1 5809 |
. . . . . . . . . . . 12
⊢ (𝑃:(0...(#‘𝐹))–1-1→𝑉 ↔ (𝑃:(0...(#‘𝐹))⟶𝑉 ∧ Fun ◡𝑃)) |
10 | | eqeq2 2621 |
. . . . . . . . . . . . . 14
⊢ (𝐴 = 𝐵 → ((𝑃‘0) = 𝐴 ↔ (𝑃‘0) = 𝐵)) |
11 | | eqtr3 2631 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃‘(#‘𝐹)) = 𝐵 ∧ (𝑃‘0) = 𝐵) → (𝑃‘(#‘𝐹)) = (𝑃‘0)) |
12 | | elnn0uz 11601 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝐹) ∈
ℕ0 ↔ (#‘𝐹) ∈
(ℤ≥‘0)) |
13 | | eluzfz2 12220 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝐹) ∈
(ℤ≥‘0) → (#‘𝐹) ∈ (0...(#‘𝐹))) |
14 | 12, 13 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ∈ (0...(#‘𝐹))) |
15 | | 0elfz 12305 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝐹) ∈
ℕ0 → 0 ∈ (0...(#‘𝐹))) |
16 | 14, 15 | jca 553 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝐹) ∈
ℕ0 → ((#‘𝐹) ∈ (0...(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)))) |
17 | | f1veqaeq 6418 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ ((#‘𝐹) ∈ (0...(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)))) → ((𝑃‘(#‘𝐹)) = (𝑃‘0) → (#‘𝐹) = 0)) |
18 | 16, 17 | sylan2 490 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ (#‘𝐹) ∈ ℕ0) → ((𝑃‘(#‘𝐹)) = (𝑃‘0) → (#‘𝐹) = 0)) |
19 | 18 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃:(0...(#‘𝐹))–1-1→𝑉 → ((#‘𝐹) ∈ ℕ0 → ((𝑃‘(#‘𝐹)) = (𝑃‘0) → (#‘𝐹) = 0))) |
20 | 19 | com13 86 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃‘(#‘𝐹)) = (𝑃‘0) → ((#‘𝐹) ∈ ℕ0 → (𝑃:(0...(#‘𝐹))–1-1→𝑉 → (#‘𝐹) = 0))) |
21 | 11, 20 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃‘(#‘𝐹)) = 𝐵 ∧ (𝑃‘0) = 𝐵) → ((#‘𝐹) ∈ ℕ0 → (𝑃:(0...(#‘𝐹))–1-1→𝑉 → (#‘𝐹) = 0))) |
22 | 21 | expcom 450 |
. . . . . . . . . . . . . 14
⊢ ((𝑃‘0) = 𝐵 → ((𝑃‘(#‘𝐹)) = 𝐵 → ((#‘𝐹) ∈ ℕ0 → (𝑃:(0...(#‘𝐹))–1-1→𝑉 → (#‘𝐹) = 0)))) |
23 | 10, 22 | syl6bi 242 |
. . . . . . . . . . . . 13
⊢ (𝐴 = 𝐵 → ((𝑃‘0) = 𝐴 → ((𝑃‘(#‘𝐹)) = 𝐵 → ((#‘𝐹) ∈ ℕ0 → (𝑃:(0...(#‘𝐹))–1-1→𝑉 → (#‘𝐹) = 0))))) |
24 | 23 | com15 99 |
. . . . . . . . . . . 12
⊢ (𝑃:(0...(#‘𝐹))–1-1→𝑉 → ((𝑃‘0) = 𝐴 → ((𝑃‘(#‘𝐹)) = 𝐵 → ((#‘𝐹) ∈ ℕ0 → (𝐴 = 𝐵 → (#‘𝐹) = 0))))) |
25 | 9, 24 | sylbir 224 |
. . . . . . . . . . 11
⊢ ((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ Fun ◡𝑃) → ((𝑃‘0) = 𝐴 → ((𝑃‘(#‘𝐹)) = 𝐵 → ((#‘𝐹) ∈ ℕ0 → (𝐴 = 𝐵 → (#‘𝐹) = 0))))) |
26 | 25 | expcom 450 |
. . . . . . . . . 10
⊢ (Fun
◡𝑃 → (𝑃:(0...(#‘𝐹))⟶𝑉 → ((𝑃‘0) = 𝐴 → ((𝑃‘(#‘𝐹)) = 𝐵 → ((#‘𝐹) ∈ ℕ0 → (𝐴 = 𝐵 → (#‘𝐹) = 0)))))) |
27 | 26 | com15 99 |
. . . . . . . . 9
⊢
((#‘𝐹) ∈
ℕ0 → (𝑃:(0...(#‘𝐹))⟶𝑉 → ((𝑃‘0) = 𝐴 → ((𝑃‘(#‘𝐹)) = 𝐵 → (Fun ◡𝑃 → (𝐴 = 𝐵 → (#‘𝐹) = 0)))))) |
28 | 27 | imp 444 |
. . . . . . . 8
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → ((𝑃‘0) = 𝐴 → ((𝑃‘(#‘𝐹)) = 𝐵 → (Fun ◡𝑃 → (𝐴 = 𝐵 → (#‘𝐹) = 0))))) |
29 | 6, 8, 28 | 3syl 18 |
. . . . . . 7
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → ((𝑃‘0) = 𝐴 → ((𝑃‘(#‘𝐹)) = 𝐵 → (Fun ◡𝑃 → (𝐴 = 𝐵 → (#‘𝐹) = 0))))) |
30 | 29 | 3imp1 1272 |
. . . . . 6
⊢ (((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) ∧ Fun ◡𝑃) → (𝐴 = 𝐵 → (#‘𝐹) = 0)) |
31 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) = 0
→ (𝑃‘(#‘𝐹)) = (𝑃‘0)) |
32 | 31 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢
((#‘𝐹) = 0
→ ((𝑃‘(#‘𝐹)) = 𝐵 ↔ (𝑃‘0) = 𝐵)) |
33 | 32 | anbi2d 736 |
. . . . . . . . . 10
⊢
((#‘𝐹) = 0
→ (((𝑃‘0) =
𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) ↔ ((𝑃‘0) = 𝐴 ∧ (𝑃‘0) = 𝐵))) |
34 | | eqtr2 2630 |
. . . . . . . . . 10
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘0) = 𝐵) → 𝐴 = 𝐵) |
35 | 33, 34 | syl6bi 242 |
. . . . . . . . 9
⊢
((#‘𝐹) = 0
→ (((𝑃‘0) =
𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → 𝐴 = 𝐵)) |
36 | 35 | com12 32 |
. . . . . . . 8
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → ((#‘𝐹) = 0 → 𝐴 = 𝐵)) |
37 | 36 | 3adant1 1072 |
. . . . . . 7
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → ((#‘𝐹) = 0 → 𝐴 = 𝐵)) |
38 | 37 | adantr 480 |
. . . . . 6
⊢ (((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) ∧ Fun ◡𝑃) → ((#‘𝐹) = 0 → 𝐴 = 𝐵)) |
39 | 30, 38 | impbid 201 |
. . . . 5
⊢ (((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) ∧ Fun ◡𝑃) → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0)) |
40 | 39 | adantrl 748 |
. . . 4
⊢ (((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) ∧ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃)) → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0)) |
41 | 5, 40 | syl6bi 242 |
. . 3
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → ((𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 ∧ 𝐹(𝑉 SPaths 𝐸)𝑃) → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0))) |
42 | 41 | imp 444 |
. 2
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 ∧ 𝐹(𝑉 SPaths 𝐸)𝑃)) → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0)) |
43 | 1, 42 | syl 17 |
1
⊢ (𝐹(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑃 → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0)) |