Proof of Theorem spthonepeq
Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . 3
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
2 | 1 | spthonprop 26641 |
. 2
⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(SPaths‘𝐺)𝑃))) |
3 | 1 | istrlson 26603 |
. . . . . 6
⊢ (((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ 𝐹(Trails‘𝐺)𝑃))) |
4 | 3 | 3adantl1 1217 |
. . . . 5
⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ 𝐹(Trails‘𝐺)𝑃))) |
5 | | isspth 26620 |
. . . . . 6
⊢ (𝐹(SPaths‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ Fun ◡𝑃)) |
6 | 5 | a1i 11 |
. . . . 5
⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(SPaths‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ Fun ◡𝑃))) |
7 | 4, 6 | anbi12d 747 |
. . . 4
⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(SPaths‘𝐺)𝑃) ↔ ((𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ 𝐹(Trails‘𝐺)𝑃) ∧ (𝐹(Trails‘𝐺)𝑃 ∧ Fun ◡𝑃)))) |
8 | 1 | wlkonprop 26554 |
. . . . . . . 8
⊢ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵))) |
9 | | wlkcl 26511 |
. . . . . . . . . . . . 13
⊢ (𝐹(Walks‘𝐺)𝑃 → (#‘𝐹) ∈
ℕ0) |
10 | 1 | wlkp 26512 |
. . . . . . . . . . . . 13
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) |
11 | | df-f1 5893 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃:(0...(#‘𝐹))–1-1→(Vtx‘𝐺) ↔ (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡𝑃)) |
12 | | eqeq2 2633 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 = 𝐵 → ((𝑃‘0) = 𝐴 ↔ (𝑃‘0) = 𝐵)) |
13 | | eqtr3 2643 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃‘(#‘𝐹)) = 𝐵 ∧ (𝑃‘0) = 𝐵) → (𝑃‘(#‘𝐹)) = (𝑃‘0)) |
14 | | elnn0uz 11725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝐹) ∈
ℕ0 ↔ (#‘𝐹) ∈
(ℤ≥‘0)) |
15 | | eluzfz2 12349 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝐹) ∈
(ℤ≥‘0) → (#‘𝐹) ∈ (0...(#‘𝐹))) |
16 | 14, 15 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ∈ (0...(#‘𝐹))) |
17 | | 0elfz 12436 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝐹) ∈
ℕ0 → 0 ∈ (0...(#‘𝐹))) |
18 | 16, 17 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝐹) ∈
ℕ0 → ((#‘𝐹) ∈ (0...(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)))) |
19 | | f1veqaeq 6514 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃:(0...(#‘𝐹))–1-1→(Vtx‘𝐺) ∧ ((#‘𝐹) ∈ (0...(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)))) → ((𝑃‘(#‘𝐹)) = (𝑃‘0) → (#‘𝐹) = 0)) |
20 | 18, 19 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃:(0...(#‘𝐹))–1-1→(Vtx‘𝐺) ∧ (#‘𝐹) ∈ ℕ0) → ((𝑃‘(#‘𝐹)) = (𝑃‘0) → (#‘𝐹) = 0)) |
21 | 20 | ex 450 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃:(0...(#‘𝐹))–1-1→(Vtx‘𝐺) → ((#‘𝐹) ∈ ℕ0 → ((𝑃‘(#‘𝐹)) = (𝑃‘0) → (#‘𝐹) = 0))) |
22 | 21 | com13 88 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃‘(#‘𝐹)) = (𝑃‘0) → ((#‘𝐹) ∈ ℕ0 → (𝑃:(0...(#‘𝐹))–1-1→(Vtx‘𝐺) → (#‘𝐹) = 0))) |
23 | 13, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃‘(#‘𝐹)) = 𝐵 ∧ (𝑃‘0) = 𝐵) → ((#‘𝐹) ∈ ℕ0 → (𝑃:(0...(#‘𝐹))–1-1→(Vtx‘𝐺) → (#‘𝐹) = 0))) |
24 | 23 | expcom 451 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃‘0) = 𝐵 → ((𝑃‘(#‘𝐹)) = 𝐵 → ((#‘𝐹) ∈ ℕ0 → (𝑃:(0...(#‘𝐹))–1-1→(Vtx‘𝐺) → (#‘𝐹) = 0)))) |
25 | 12, 24 | syl6bi 243 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 = 𝐵 → ((𝑃‘0) = 𝐴 → ((𝑃‘(#‘𝐹)) = 𝐵 → ((#‘𝐹) ∈ ℕ0 → (𝑃:(0...(#‘𝐹))–1-1→(Vtx‘𝐺) → (#‘𝐹) = 0))))) |
26 | 25 | com15 101 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃:(0...(#‘𝐹))–1-1→(Vtx‘𝐺) → ((𝑃‘0) = 𝐴 → ((𝑃‘(#‘𝐹)) = 𝐵 → ((#‘𝐹) ∈ ℕ0 → (𝐴 = 𝐵 → (#‘𝐹) = 0))))) |
27 | 11, 26 | sylbir 225 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡𝑃) → ((𝑃‘0) = 𝐴 → ((𝑃‘(#‘𝐹)) = 𝐵 → ((#‘𝐹) ∈ ℕ0 → (𝐴 = 𝐵 → (#‘𝐹) = 0))))) |
28 | 27 | expcom 451 |
. . . . . . . . . . . . . 14
⊢ (Fun
◡𝑃 → (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → ((𝑃‘0) = 𝐴 → ((𝑃‘(#‘𝐹)) = 𝐵 → ((#‘𝐹) ∈ ℕ0 → (𝐴 = 𝐵 → (#‘𝐹) = 0)))))) |
29 | 28 | com15 101 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) ∈
ℕ0 → (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → ((𝑃‘0) = 𝐴 → ((𝑃‘(#‘𝐹)) = 𝐵 → (Fun ◡𝑃 → (𝐴 = 𝐵 → (#‘𝐹) = 0)))))) |
30 | 9, 10, 29 | sylc 65 |
. . . . . . . . . . . 12
⊢ (𝐹(Walks‘𝐺)𝑃 → ((𝑃‘0) = 𝐴 → ((𝑃‘(#‘𝐹)) = 𝐵 → (Fun ◡𝑃 → (𝐴 = 𝐵 → (#‘𝐹) = 0))))) |
31 | 30 | 3imp1 1280 |
. . . . . . . . . . 11
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) ∧ Fun ◡𝑃) → (𝐴 = 𝐵 → (#‘𝐹) = 0)) |
32 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝐹) = 0
→ (𝑃‘(#‘𝐹)) = (𝑃‘0)) |
33 | 32 | eqeq1d 2624 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐹) = 0
→ ((𝑃‘(#‘𝐹)) = 𝐵 ↔ (𝑃‘0) = 𝐵)) |
34 | 33 | anbi2d 740 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐹) = 0
→ (((𝑃‘0) =
𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) ↔ ((𝑃‘0) = 𝐴 ∧ (𝑃‘0) = 𝐵))) |
35 | | eqtr2 2642 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘0) = 𝐵) → 𝐴 = 𝐵) |
36 | 34, 35 | syl6bi 243 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐹) = 0
→ (((𝑃‘0) =
𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → 𝐴 = 𝐵)) |
37 | 36 | com12 32 |
. . . . . . . . . . . . 13
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → ((#‘𝐹) = 0 → 𝐴 = 𝐵)) |
38 | 37 | 3adant1 1079 |
. . . . . . . . . . . 12
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → ((#‘𝐹) = 0 → 𝐴 = 𝐵)) |
39 | 38 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) ∧ Fun ◡𝑃) → ((#‘𝐹) = 0 → 𝐴 = 𝐵)) |
40 | 31, 39 | impbid 202 |
. . . . . . . . . 10
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) ∧ Fun ◡𝑃) → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0)) |
41 | 40 | ex 450 |
. . . . . . . . 9
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → (Fun ◡𝑃 → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0))) |
42 | 41 | 3ad2ant3 1084 |
. . . . . . . 8
⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) → (Fun ◡𝑃 → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0))) |
43 | 8, 42 | syl 17 |
. . . . . . 7
⊢ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → (Fun ◡𝑃 → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0))) |
44 | 43 | adantld 483 |
. . . . . 6
⊢ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → ((𝐹(Trails‘𝐺)𝑃 ∧ Fun ◡𝑃) → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0))) |
45 | 44 | adantr 481 |
. . . . 5
⊢ ((𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ 𝐹(Trails‘𝐺)𝑃) → ((𝐹(Trails‘𝐺)𝑃 ∧ Fun ◡𝑃) → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0))) |
46 | 45 | imp 445 |
. . . 4
⊢ (((𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ 𝐹(Trails‘𝐺)𝑃) ∧ (𝐹(Trails‘𝐺)𝑃 ∧ Fun ◡𝑃)) → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0)) |
47 | 7, 46 | syl6bi 243 |
. . 3
⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(SPaths‘𝐺)𝑃) → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0))) |
48 | 47 | 3impia 1261 |
. 2
⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(SPaths‘𝐺)𝑃)) → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0)) |
49 | 2, 48 | syl 17 |
1
⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0)) |