Proof of Theorem pthdlem2lem
Step | Hyp | Ref
| Expression |
1 | | pthd.s |
. . . . . 6
⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))) |
2 | 1 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))) |
3 | | ralcom 3258 |
. . . . . 6
⊢
(∀𝑖 ∈
(0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ↔ ∀𝑗 ∈ (1..^𝑅)∀𝑖 ∈ (0..^(♯‘𝑃))(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))) |
4 | | elfzo1 13179 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (1..^𝑅) ↔ (𝑗 ∈ ℕ ∧ 𝑅 ∈ ℕ ∧ 𝑗 < 𝑅)) |
5 | | nnne0 11751 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ → 𝑗 ≠ 0) |
6 | 5 | necomd 2989 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ℕ → 0 ≠
𝑗) |
7 | 6 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ ℕ ∧ 𝑅 ∈ ℕ ∧ 𝑗 < 𝑅) → 0 ≠ 𝑗) |
8 | 4, 7 | sylbi 220 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (1..^𝑅) → 0 ≠ 𝑗) |
9 | 8 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢
(((♯‘𝑃)
∈ ℕ ∧ 𝑗
∈ (1..^𝑅)) → 0
≠ 𝑗) |
10 | | neeq1 2996 |
. . . . . . . . . . . . . . 15
⊢ (𝐼 = 0 → (𝐼 ≠ 𝑗 ↔ 0 ≠ 𝑗)) |
11 | 9, 10 | syl5ibr 249 |
. . . . . . . . . . . . . 14
⊢ (𝐼 = 0 →
(((♯‘𝑃) ∈
ℕ ∧ 𝑗 ∈
(1..^𝑅)) → 𝐼 ≠ 𝑗)) |
12 | 11 | expd 419 |
. . . . . . . . . . . . 13
⊢ (𝐼 = 0 →
((♯‘𝑃) ∈
ℕ → (𝑗 ∈
(1..^𝑅) → 𝐼 ≠ 𝑗))) |
13 | | nnre 11724 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℝ) |
14 | 13 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ ℕ ∧ 𝑅 ∈ ℕ) → 𝑗 ∈
ℝ) |
15 | | nnre 11724 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ ℕ → 𝑅 ∈
ℝ) |
16 | 15 | adantl 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ ℕ ∧ 𝑅 ∈ ℕ) → 𝑅 ∈
ℝ) |
17 | 14, 16 | ltlend 10864 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ ℕ ∧ 𝑅 ∈ ℕ) → (𝑗 < 𝑅 ↔ (𝑗 ≤ 𝑅 ∧ 𝑅 ≠ 𝑗))) |
18 | | simpr 488 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ≤ 𝑅 ∧ 𝑅 ≠ 𝑗) → 𝑅 ≠ 𝑗) |
19 | 17, 18 | syl6bi 256 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ ℕ ∧ 𝑅 ∈ ℕ) → (𝑗 < 𝑅 → 𝑅 ≠ 𝑗)) |
20 | 19 | 3impia 1118 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ ℕ ∧ 𝑅 ∈ ℕ ∧ 𝑗 < 𝑅) → 𝑅 ≠ 𝑗) |
21 | 4, 20 | sylbi 220 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (1..^𝑅) → 𝑅 ≠ 𝑗) |
22 | 21 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢
(((♯‘𝑃)
∈ ℕ ∧ 𝑗
∈ (1..^𝑅)) →
𝑅 ≠ 𝑗) |
23 | | neeq1 2996 |
. . . . . . . . . . . . . . 15
⊢ (𝐼 = 𝑅 → (𝐼 ≠ 𝑗 ↔ 𝑅 ≠ 𝑗)) |
24 | 22, 23 | syl5ibr 249 |
. . . . . . . . . . . . . 14
⊢ (𝐼 = 𝑅 → (((♯‘𝑃) ∈ ℕ ∧ 𝑗 ∈ (1..^𝑅)) → 𝐼 ≠ 𝑗)) |
25 | 24 | expd 419 |
. . . . . . . . . . . . 13
⊢ (𝐼 = 𝑅 → ((♯‘𝑃) ∈ ℕ → (𝑗 ∈ (1..^𝑅) → 𝐼 ≠ 𝑗))) |
26 | 12, 25 | jaoi 856 |
. . . . . . . . . . . 12
⊢ ((𝐼 = 0 ∨ 𝐼 = 𝑅) → ((♯‘𝑃) ∈ ℕ → (𝑗 ∈ (1..^𝑅) → 𝐼 ≠ 𝑗))) |
27 | 26 | impcom 411 |
. . . . . . . . . . 11
⊢
(((♯‘𝑃)
∈ ℕ ∧ (𝐼 = 0
∨ 𝐼 = 𝑅)) → (𝑗 ∈ (1..^𝑅) → 𝐼 ≠ 𝑗)) |
28 | 27 | 3adant1 1131 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → (𝑗 ∈ (1..^𝑅) → 𝐼 ≠ 𝑗)) |
29 | 28 | imp 410 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) ∧ 𝑗 ∈ (1..^𝑅)) → 𝐼 ≠ 𝑗) |
30 | | lbfzo0 13169 |
. . . . . . . . . . . . . . . 16
⊢ (0 ∈
(0..^(♯‘𝑃))
↔ (♯‘𝑃)
∈ ℕ) |
31 | 30 | biimpri 231 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝑃)
∈ ℕ → 0 ∈ (0..^(♯‘𝑃))) |
32 | | eleq1 2820 |
. . . . . . . . . . . . . . 15
⊢ (𝐼 = 0 → (𝐼 ∈ (0..^(♯‘𝑃)) ↔ 0 ∈
(0..^(♯‘𝑃)))) |
33 | 31, 32 | syl5ibr 249 |
. . . . . . . . . . . . . 14
⊢ (𝐼 = 0 →
((♯‘𝑃) ∈
ℕ → 𝐼 ∈
(0..^(♯‘𝑃)))) |
34 | | pthd.r |
. . . . . . . . . . . . . . . 16
⊢ 𝑅 = ((♯‘𝑃) − 1) |
35 | | fzo0end 13221 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘𝑃)
∈ ℕ → ((♯‘𝑃) − 1) ∈
(0..^(♯‘𝑃))) |
36 | 34, 35 | eqeltrid 2837 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝑃)
∈ ℕ → 𝑅
∈ (0..^(♯‘𝑃))) |
37 | | eleq1 2820 |
. . . . . . . . . . . . . . 15
⊢ (𝐼 = 𝑅 → (𝐼 ∈ (0..^(♯‘𝑃)) ↔ 𝑅 ∈ (0..^(♯‘𝑃)))) |
38 | 36, 37 | syl5ibr 249 |
. . . . . . . . . . . . . 14
⊢ (𝐼 = 𝑅 → ((♯‘𝑃) ∈ ℕ → 𝐼 ∈ (0..^(♯‘𝑃)))) |
39 | 33, 38 | jaoi 856 |
. . . . . . . . . . . . 13
⊢ ((𝐼 = 0 ∨ 𝐼 = 𝑅) → ((♯‘𝑃) ∈ ℕ → 𝐼 ∈ (0..^(♯‘𝑃)))) |
40 | 39 | impcom 411 |
. . . . . . . . . . . 12
⊢
(((♯‘𝑃)
∈ ℕ ∧ (𝐼 = 0
∨ 𝐼 = 𝑅)) → 𝐼 ∈ (0..^(♯‘𝑃))) |
41 | 40 | 3adant1 1131 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → 𝐼 ∈ (0..^(♯‘𝑃))) |
42 | 41 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) ∧ 𝑗 ∈ (1..^𝑅)) → 𝐼 ∈ (0..^(♯‘𝑃))) |
43 | | neeq1 2996 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝐼 → (𝑖 ≠ 𝑗 ↔ 𝐼 ≠ 𝑗)) |
44 | | fveq2 6675 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝐼 → (𝑃‘𝑖) = (𝑃‘𝐼)) |
45 | 44 | neeq1d 2993 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝐼 → ((𝑃‘𝑖) ≠ (𝑃‘𝑗) ↔ (𝑃‘𝐼) ≠ (𝑃‘𝑗))) |
46 | 43, 45 | imbi12d 348 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝐼 → ((𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ↔ (𝐼 ≠ 𝑗 → (𝑃‘𝐼) ≠ (𝑃‘𝑗)))) |
47 | 46 | rspcv 3522 |
. . . . . . . . . 10
⊢ (𝐼 ∈
(0..^(♯‘𝑃))
→ (∀𝑖 ∈
(0..^(♯‘𝑃))(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) → (𝐼 ≠ 𝑗 → (𝑃‘𝐼) ≠ (𝑃‘𝑗)))) |
48 | 42, 47 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) ∧ 𝑗 ∈ (1..^𝑅)) → (∀𝑖 ∈ (0..^(♯‘𝑃))(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) → (𝐼 ≠ 𝑗 → (𝑃‘𝐼) ≠ (𝑃‘𝑗)))) |
49 | 29, 48 | mpid 44 |
. . . . . . . 8
⊢ (((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) ∧ 𝑗 ∈ (1..^𝑅)) → (∀𝑖 ∈ (0..^(♯‘𝑃))(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) → (𝑃‘𝐼) ≠ (𝑃‘𝑗))) |
50 | | nesym 2990 |
. . . . . . . 8
⊢ ((𝑃‘𝐼) ≠ (𝑃‘𝑗) ↔ ¬ (𝑃‘𝑗) = (𝑃‘𝐼)) |
51 | 49, 50 | syl6ib 254 |
. . . . . . 7
⊢ (((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) ∧ 𝑗 ∈ (1..^𝑅)) → (∀𝑖 ∈ (0..^(♯‘𝑃))(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) → ¬ (𝑃‘𝑗) = (𝑃‘𝐼))) |
52 | 51 | ralimdva 3091 |
. . . . . 6
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → (∀𝑗 ∈ (1..^𝑅)∀𝑖 ∈ (0..^(♯‘𝑃))(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) → ∀𝑗 ∈ (1..^𝑅) ¬ (𝑃‘𝑗) = (𝑃‘𝐼))) |
53 | 3, 52 | syl5bi 245 |
. . . . 5
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → (∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) → ∀𝑗 ∈ (1..^𝑅) ¬ (𝑃‘𝑗) = (𝑃‘𝐼))) |
54 | 2, 53 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → ∀𝑗 ∈ (1..^𝑅) ¬ (𝑃‘𝑗) = (𝑃‘𝐼)) |
55 | | ralnex 3149 |
. . . 4
⊢
(∀𝑗 ∈
(1..^𝑅) ¬ (𝑃‘𝑗) = (𝑃‘𝐼) ↔ ¬ ∃𝑗 ∈ (1..^𝑅)(𝑃‘𝑗) = (𝑃‘𝐼)) |
56 | 54, 55 | sylib 221 |
. . 3
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → ¬ ∃𝑗 ∈ (1..^𝑅)(𝑃‘𝑗) = (𝑃‘𝐼)) |
57 | | pthd.p |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ Word V) |
58 | | wrdf 13961 |
. . . . . 6
⊢ (𝑃 ∈ Word V → 𝑃:(0..^(♯‘𝑃))⟶V) |
59 | | ffun 6508 |
. . . . . 6
⊢ (𝑃:(0..^(♯‘𝑃))⟶V → Fun 𝑃) |
60 | 57, 58, 59 | 3syl 18 |
. . . . 5
⊢ (𝜑 → Fun 𝑃) |
61 | 60 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → Fun 𝑃) |
62 | | fvelima 6736 |
. . . . 5
⊢ ((Fun
𝑃 ∧ (𝑃‘𝐼) ∈ (𝑃 “ (1..^𝑅))) → ∃𝑗 ∈ (1..^𝑅)(𝑃‘𝑗) = (𝑃‘𝐼)) |
63 | 62 | ex 416 |
. . . 4
⊢ (Fun
𝑃 → ((𝑃‘𝐼) ∈ (𝑃 “ (1..^𝑅)) → ∃𝑗 ∈ (1..^𝑅)(𝑃‘𝑗) = (𝑃‘𝐼))) |
64 | 61, 63 | syl 17 |
. . 3
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → ((𝑃‘𝐼) ∈ (𝑃 “ (1..^𝑅)) → ∃𝑗 ∈ (1..^𝑅)(𝑃‘𝑗) = (𝑃‘𝐼))) |
65 | 56, 64 | mtod 201 |
. 2
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → ¬ (𝑃‘𝐼) ∈ (𝑃 “ (1..^𝑅))) |
66 | | df-nel 3039 |
. 2
⊢ ((𝑃‘𝐼) ∉ (𝑃 “ (1..^𝑅)) ↔ ¬ (𝑃‘𝐼) ∈ (𝑃 “ (1..^𝑅))) |
67 | 65, 66 | sylibr 237 |
1
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → (𝑃‘𝐼) ∉ (𝑃 “ (1..^𝑅))) |