Proof of Theorem pthdlem2lem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pthd.s | . . . . . 6
⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))) | 
| 2 | 1 | 3ad2ant1 1133 | . . . . 5
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))) | 
| 3 |  | ralcom 3288 | . . . . . 6
⊢
(∀𝑖 ∈
(0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ↔ ∀𝑗 ∈ (1..^𝑅)∀𝑖 ∈ (0..^(♯‘𝑃))(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))) | 
| 4 |  | elfzo1 13753 | . . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (1..^𝑅) ↔ (𝑗 ∈ ℕ ∧ 𝑅 ∈ ℕ ∧ 𝑗 < 𝑅)) | 
| 5 |  | nnne0 12301 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ → 𝑗 ≠ 0) | 
| 6 | 5 | necomd 2995 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ℕ → 0 ≠
𝑗) | 
| 7 | 6 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ ℕ ∧ 𝑅 ∈ ℕ ∧ 𝑗 < 𝑅) → 0 ≠ 𝑗) | 
| 8 | 4, 7 | sylbi 217 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (1..^𝑅) → 0 ≠ 𝑗) | 
| 9 | 8 | adantl 481 | . . . . . . . . . . . . . . 15
⊢
(((♯‘𝑃)
∈ ℕ ∧ 𝑗
∈ (1..^𝑅)) → 0
≠ 𝑗) | 
| 10 |  | neeq1 3002 | . . . . . . . . . . . . . . 15
⊢ (𝐼 = 0 → (𝐼 ≠ 𝑗 ↔ 0 ≠ 𝑗)) | 
| 11 | 9, 10 | imbitrrid 246 | . . . . . . . . . . . . . 14
⊢ (𝐼 = 0 →
(((♯‘𝑃) ∈
ℕ ∧ 𝑗 ∈
(1..^𝑅)) → 𝐼 ≠ 𝑗)) | 
| 12 | 11 | expd 415 | . . . . . . . . . . . . 13
⊢ (𝐼 = 0 →
((♯‘𝑃) ∈
ℕ → (𝑗 ∈
(1..^𝑅) → 𝐼 ≠ 𝑗))) | 
| 13 |  | nnre 12274 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℝ) | 
| 14 | 13 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ ℕ ∧ 𝑅 ∈ ℕ) → 𝑗 ∈
ℝ) | 
| 15 |  | nnre 12274 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ ℕ → 𝑅 ∈
ℝ) | 
| 16 | 15 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ ℕ ∧ 𝑅 ∈ ℕ) → 𝑅 ∈
ℝ) | 
| 17 | 14, 16 | ltlend 11407 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ ℕ ∧ 𝑅 ∈ ℕ) → (𝑗 < 𝑅 ↔ (𝑗 ≤ 𝑅 ∧ 𝑅 ≠ 𝑗))) | 
| 18 |  | simpr 484 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ≤ 𝑅 ∧ 𝑅 ≠ 𝑗) → 𝑅 ≠ 𝑗) | 
| 19 | 17, 18 | biimtrdi 253 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ ℕ ∧ 𝑅 ∈ ℕ) → (𝑗 < 𝑅 → 𝑅 ≠ 𝑗)) | 
| 20 | 19 | 3impia 1117 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ ℕ ∧ 𝑅 ∈ ℕ ∧ 𝑗 < 𝑅) → 𝑅 ≠ 𝑗) | 
| 21 | 4, 20 | sylbi 217 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (1..^𝑅) → 𝑅 ≠ 𝑗) | 
| 22 | 21 | adantl 481 | . . . . . . . . . . . . . . 15
⊢
(((♯‘𝑃)
∈ ℕ ∧ 𝑗
∈ (1..^𝑅)) →
𝑅 ≠ 𝑗) | 
| 23 |  | neeq1 3002 | . . . . . . . . . . . . . . 15
⊢ (𝐼 = 𝑅 → (𝐼 ≠ 𝑗 ↔ 𝑅 ≠ 𝑗)) | 
| 24 | 22, 23 | imbitrrid 246 | . . . . . . . . . . . . . 14
⊢ (𝐼 = 𝑅 → (((♯‘𝑃) ∈ ℕ ∧ 𝑗 ∈ (1..^𝑅)) → 𝐼 ≠ 𝑗)) | 
| 25 | 24 | expd 415 | . . . . . . . . . . . . 13
⊢ (𝐼 = 𝑅 → ((♯‘𝑃) ∈ ℕ → (𝑗 ∈ (1..^𝑅) → 𝐼 ≠ 𝑗))) | 
| 26 | 12, 25 | jaoi 857 | . . . . . . . . . . . 12
⊢ ((𝐼 = 0 ∨ 𝐼 = 𝑅) → ((♯‘𝑃) ∈ ℕ → (𝑗 ∈ (1..^𝑅) → 𝐼 ≠ 𝑗))) | 
| 27 | 26 | impcom 407 | . . . . . . . . . . 11
⊢
(((♯‘𝑃)
∈ ℕ ∧ (𝐼 = 0
∨ 𝐼 = 𝑅)) → (𝑗 ∈ (1..^𝑅) → 𝐼 ≠ 𝑗)) | 
| 28 | 27 | 3adant1 1130 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → (𝑗 ∈ (1..^𝑅) → 𝐼 ≠ 𝑗)) | 
| 29 | 28 | imp 406 | . . . . . . . . 9
⊢ (((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) ∧ 𝑗 ∈ (1..^𝑅)) → 𝐼 ≠ 𝑗) | 
| 30 |  | lbfzo0 13740 | . . . . . . . . . . . . . . . 16
⊢ (0 ∈
(0..^(♯‘𝑃))
↔ (♯‘𝑃)
∈ ℕ) | 
| 31 | 30 | biimpri 228 | . . . . . . . . . . . . . . 15
⊢
((♯‘𝑃)
∈ ℕ → 0 ∈ (0..^(♯‘𝑃))) | 
| 32 |  | eleq1 2828 | . . . . . . . . . . . . . . 15
⊢ (𝐼 = 0 → (𝐼 ∈ (0..^(♯‘𝑃)) ↔ 0 ∈
(0..^(♯‘𝑃)))) | 
| 33 | 31, 32 | imbitrrid 246 | . . . . . . . . . . . . . 14
⊢ (𝐼 = 0 →
((♯‘𝑃) ∈
ℕ → 𝐼 ∈
(0..^(♯‘𝑃)))) | 
| 34 |  | pthd.r | . . . . . . . . . . . . . . . 16
⊢ 𝑅 = ((♯‘𝑃) − 1) | 
| 35 |  | fzo0end 13798 | . . . . . . . . . . . . . . . 16
⊢
((♯‘𝑃)
∈ ℕ → ((♯‘𝑃) − 1) ∈
(0..^(♯‘𝑃))) | 
| 36 | 34, 35 | eqeltrid 2844 | . . . . . . . . . . . . . . 15
⊢
((♯‘𝑃)
∈ ℕ → 𝑅
∈ (0..^(♯‘𝑃))) | 
| 37 |  | eleq1 2828 | . . . . . . . . . . . . . . 15
⊢ (𝐼 = 𝑅 → (𝐼 ∈ (0..^(♯‘𝑃)) ↔ 𝑅 ∈ (0..^(♯‘𝑃)))) | 
| 38 | 36, 37 | imbitrrid 246 | . . . . . . . . . . . . . 14
⊢ (𝐼 = 𝑅 → ((♯‘𝑃) ∈ ℕ → 𝐼 ∈ (0..^(♯‘𝑃)))) | 
| 39 | 33, 38 | jaoi 857 | . . . . . . . . . . . . 13
⊢ ((𝐼 = 0 ∨ 𝐼 = 𝑅) → ((♯‘𝑃) ∈ ℕ → 𝐼 ∈ (0..^(♯‘𝑃)))) | 
| 40 | 39 | impcom 407 | . . . . . . . . . . . 12
⊢
(((♯‘𝑃)
∈ ℕ ∧ (𝐼 = 0
∨ 𝐼 = 𝑅)) → 𝐼 ∈ (0..^(♯‘𝑃))) | 
| 41 | 40 | 3adant1 1130 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → 𝐼 ∈ (0..^(♯‘𝑃))) | 
| 42 | 41 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) ∧ 𝑗 ∈ (1..^𝑅)) → 𝐼 ∈ (0..^(♯‘𝑃))) | 
| 43 |  | neeq1 3002 | . . . . . . . . . . . 12
⊢ (𝑖 = 𝐼 → (𝑖 ≠ 𝑗 ↔ 𝐼 ≠ 𝑗)) | 
| 44 |  | fveq2 6905 | . . . . . . . . . . . . 13
⊢ (𝑖 = 𝐼 → (𝑃‘𝑖) = (𝑃‘𝐼)) | 
| 45 | 44 | neeq1d 2999 | . . . . . . . . . . . 12
⊢ (𝑖 = 𝐼 → ((𝑃‘𝑖) ≠ (𝑃‘𝑗) ↔ (𝑃‘𝐼) ≠ (𝑃‘𝑗))) | 
| 46 | 43, 45 | imbi12d 344 | . . . . . . . . . . 11
⊢ (𝑖 = 𝐼 → ((𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) ↔ (𝐼 ≠ 𝑗 → (𝑃‘𝐼) ≠ (𝑃‘𝑗)))) | 
| 47 | 46 | rspcv 3617 | . . . . . . . . . 10
⊢ (𝐼 ∈
(0..^(♯‘𝑃))
→ (∀𝑖 ∈
(0..^(♯‘𝑃))(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) → (𝐼 ≠ 𝑗 → (𝑃‘𝐼) ≠ (𝑃‘𝑗)))) | 
| 48 | 42, 47 | syl 17 | . . . . . . . . 9
⊢ (((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) ∧ 𝑗 ∈ (1..^𝑅)) → (∀𝑖 ∈ (0..^(♯‘𝑃))(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) → (𝐼 ≠ 𝑗 → (𝑃‘𝐼) ≠ (𝑃‘𝑗)))) | 
| 49 | 29, 48 | mpid 44 | . . . . . . . 8
⊢ (((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) ∧ 𝑗 ∈ (1..^𝑅)) → (∀𝑖 ∈ (0..^(♯‘𝑃))(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) → (𝑃‘𝐼) ≠ (𝑃‘𝑗))) | 
| 50 |  | nesym 2996 | . . . . . . . 8
⊢ ((𝑃‘𝐼) ≠ (𝑃‘𝑗) ↔ ¬ (𝑃‘𝑗) = (𝑃‘𝐼)) | 
| 51 | 49, 50 | imbitrdi 251 | . . . . . . 7
⊢ (((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) ∧ 𝑗 ∈ (1..^𝑅)) → (∀𝑖 ∈ (0..^(♯‘𝑃))(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) → ¬ (𝑃‘𝑗) = (𝑃‘𝐼))) | 
| 52 | 51 | ralimdva 3166 | . . . . . 6
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → (∀𝑗 ∈ (1..^𝑅)∀𝑖 ∈ (0..^(♯‘𝑃))(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) → ∀𝑗 ∈ (1..^𝑅) ¬ (𝑃‘𝑗) = (𝑃‘𝐼))) | 
| 53 | 3, 52 | biimtrid 242 | . . . . 5
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → (∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)) → ∀𝑗 ∈ (1..^𝑅) ¬ (𝑃‘𝑗) = (𝑃‘𝐼))) | 
| 54 | 2, 53 | mpd 15 | . . . 4
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → ∀𝑗 ∈ (1..^𝑅) ¬ (𝑃‘𝑗) = (𝑃‘𝐼)) | 
| 55 |  | ralnex 3071 | . . . 4
⊢
(∀𝑗 ∈
(1..^𝑅) ¬ (𝑃‘𝑗) = (𝑃‘𝐼) ↔ ¬ ∃𝑗 ∈ (1..^𝑅)(𝑃‘𝑗) = (𝑃‘𝐼)) | 
| 56 | 54, 55 | sylib 218 | . . 3
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → ¬ ∃𝑗 ∈ (1..^𝑅)(𝑃‘𝑗) = (𝑃‘𝐼)) | 
| 57 |  | pthd.p | . . . . . 6
⊢ (𝜑 → 𝑃 ∈ Word V) | 
| 58 |  | wrdf 14558 | . . . . . 6
⊢ (𝑃 ∈ Word V → 𝑃:(0..^(♯‘𝑃))⟶V) | 
| 59 |  | ffun 6738 | . . . . . 6
⊢ (𝑃:(0..^(♯‘𝑃))⟶V → Fun 𝑃) | 
| 60 | 57, 58, 59 | 3syl 18 | . . . . 5
⊢ (𝜑 → Fun 𝑃) | 
| 61 | 60 | 3ad2ant1 1133 | . . . 4
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → Fun 𝑃) | 
| 62 |  | fvelima 6973 | . . . . 5
⊢ ((Fun
𝑃 ∧ (𝑃‘𝐼) ∈ (𝑃 “ (1..^𝑅))) → ∃𝑗 ∈ (1..^𝑅)(𝑃‘𝑗) = (𝑃‘𝐼)) | 
| 63 | 62 | ex 412 | . . . 4
⊢ (Fun
𝑃 → ((𝑃‘𝐼) ∈ (𝑃 “ (1..^𝑅)) → ∃𝑗 ∈ (1..^𝑅)(𝑃‘𝑗) = (𝑃‘𝐼))) | 
| 64 | 61, 63 | syl 17 | . . 3
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → ((𝑃‘𝐼) ∈ (𝑃 “ (1..^𝑅)) → ∃𝑗 ∈ (1..^𝑅)(𝑃‘𝑗) = (𝑃‘𝐼))) | 
| 65 | 56, 64 | mtod 198 | . 2
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → ¬ (𝑃‘𝐼) ∈ (𝑃 “ (1..^𝑅))) | 
| 66 |  | df-nel 3046 | . 2
⊢ ((𝑃‘𝐼) ∉ (𝑃 “ (1..^𝑅)) ↔ ¬ (𝑃‘𝐼) ∈ (𝑃 “ (1..^𝑅))) | 
| 67 | 65, 66 | sylibr 234 | 1
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → (𝑃‘𝐼) ∉ (𝑃 “ (1..^𝑅))) |