Proof of Theorem 3wlkdlem5
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 3wlkd.n | . . . 4
⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) | 
| 2 |  | simpl 482 | . . . . 5
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → 𝐴 ≠ 𝐵) | 
| 3 |  | simpl 482 | . . . . 5
⊢ ((𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) → 𝐵 ≠ 𝐶) | 
| 4 |  | id 22 | . . . . 5
⊢ (𝐶 ≠ 𝐷 → 𝐶 ≠ 𝐷) | 
| 5 | 2, 3, 4 | 3anim123i 1152 | . . . 4
⊢ (((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷) → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐷)) | 
| 6 | 1, 5 | syl 17 | . . 3
⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐷)) | 
| 7 |  | 3wlkd.p | . . . . 5
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 | 
| 8 |  | 3wlkd.f | . . . . 5
⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 | 
| 9 |  | 3wlkd.s | . . . . 5
⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) | 
| 10 | 7, 8, 9 | 3wlkdlem3 30180 | . . . 4
⊢ (𝜑 → (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷))) | 
| 11 |  | simpl 482 | . . . . . . 7
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) → (𝑃‘0) = 𝐴) | 
| 12 |  | simpr 484 | . . . . . . 7
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) → (𝑃‘1) = 𝐵) | 
| 13 | 11, 12 | neeq12d 3002 | . . . . . 6
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) → ((𝑃‘0) ≠ (𝑃‘1) ↔ 𝐴 ≠ 𝐵)) | 
| 14 | 13 | adantr 480 | . . . . 5
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → ((𝑃‘0) ≠ (𝑃‘1) ↔ 𝐴 ≠ 𝐵)) | 
| 15 | 12 | adantr 480 | . . . . . 6
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → (𝑃‘1) = 𝐵) | 
| 16 |  | simpl 482 | . . . . . . 7
⊢ (((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷) → (𝑃‘2) = 𝐶) | 
| 17 | 16 | adantl 481 | . . . . . 6
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → (𝑃‘2) = 𝐶) | 
| 18 | 15, 17 | neeq12d 3002 | . . . . 5
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → ((𝑃‘1) ≠ (𝑃‘2) ↔ 𝐵 ≠ 𝐶)) | 
| 19 |  | simpr 484 | . . . . . . 7
⊢ (((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷) → (𝑃‘3) = 𝐷) | 
| 20 | 16, 19 | neeq12d 3002 | . . . . . 6
⊢ (((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷) → ((𝑃‘2) ≠ (𝑃‘3) ↔ 𝐶 ≠ 𝐷)) | 
| 21 | 20 | adantl 481 | . . . . 5
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → ((𝑃‘2) ≠ (𝑃‘3) ↔ 𝐶 ≠ 𝐷)) | 
| 22 | 14, 18, 21 | 3anbi123d 1438 | . . . 4
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘3)) ↔ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐷))) | 
| 23 | 10, 22 | syl 17 | . . 3
⊢ (𝜑 → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘3)) ↔ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐷))) | 
| 24 | 6, 23 | mpbird 257 | . 2
⊢ (𝜑 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘3))) | 
| 25 | 7, 8 | 3wlkdlem2 30179 | . . . 4
⊢
(0..^(♯‘𝐹)) = {0, 1, 2} | 
| 26 | 25 | raleqi 3324 | . . 3
⊢
(∀𝑘 ∈
(0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ↔ ∀𝑘 ∈ {0, 1, 2} (𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))) | 
| 27 |  | c0ex 11255 | . . . 4
⊢ 0 ∈
V | 
| 28 |  | 1ex 11257 | . . . 4
⊢ 1 ∈
V | 
| 29 |  | 2ex 12343 | . . . 4
⊢ 2 ∈
V | 
| 30 |  | fveq2 6906 | . . . . 5
⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0)) | 
| 31 |  | fv0p1e1 12389 | . . . . 5
⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1)) | 
| 32 | 30, 31 | neeq12d 3002 | . . . 4
⊢ (𝑘 = 0 → ((𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ↔ (𝑃‘0) ≠ (𝑃‘1))) | 
| 33 |  | fveq2 6906 | . . . . 5
⊢ (𝑘 = 1 → (𝑃‘𝑘) = (𝑃‘1)) | 
| 34 |  | oveq1 7438 | . . . . . . 7
⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1)) | 
| 35 |  | 1p1e2 12391 | . . . . . . 7
⊢ (1 + 1) =
2 | 
| 36 | 34, 35 | eqtrdi 2793 | . . . . . 6
⊢ (𝑘 = 1 → (𝑘 + 1) = 2) | 
| 37 | 36 | fveq2d 6910 | . . . . 5
⊢ (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2)) | 
| 38 | 33, 37 | neeq12d 3002 | . . . 4
⊢ (𝑘 = 1 → ((𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ↔ (𝑃‘1) ≠ (𝑃‘2))) | 
| 39 |  | fveq2 6906 | . . . . 5
⊢ (𝑘 = 2 → (𝑃‘𝑘) = (𝑃‘2)) | 
| 40 |  | oveq1 7438 | . . . . . . 7
⊢ (𝑘 = 2 → (𝑘 + 1) = (2 + 1)) | 
| 41 |  | 2p1e3 12408 | . . . . . . 7
⊢ (2 + 1) =
3 | 
| 42 | 40, 41 | eqtrdi 2793 | . . . . . 6
⊢ (𝑘 = 2 → (𝑘 + 1) = 3) | 
| 43 | 42 | fveq2d 6910 | . . . . 5
⊢ (𝑘 = 2 → (𝑃‘(𝑘 + 1)) = (𝑃‘3)) | 
| 44 | 39, 43 | neeq12d 3002 | . . . 4
⊢ (𝑘 = 2 → ((𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ↔ (𝑃‘2) ≠ (𝑃‘3))) | 
| 45 | 27, 28, 29, 32, 38, 44 | raltp 4705 | . . 3
⊢
(∀𝑘 ∈
{0, 1, 2} (𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘3))) | 
| 46 | 26, 45 | bitri 275 | . 2
⊢
(∀𝑘 ∈
(0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘3))) | 
| 47 | 24, 46 | sylibr 234 | 1
⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))) |