Proof of Theorem 3wlkdlem5
Step | Hyp | Ref
| Expression |
1 | | 3wlkd.n |
. . . 4
⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) |
2 | | simpl 483 |
. . . . 5
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → 𝐴 ≠ 𝐵) |
3 | | simpl 483 |
. . . . 5
⊢ ((𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) → 𝐵 ≠ 𝐶) |
4 | | id 22 |
. . . . 5
⊢ (𝐶 ≠ 𝐷 → 𝐶 ≠ 𝐷) |
5 | 2, 3, 4 | 3anim123i 1150 |
. . . 4
⊢ (((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷) → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐷)) |
6 | 1, 5 | syl 17 |
. . 3
⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐷)) |
7 | | 3wlkd.p |
. . . . 5
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 |
8 | | 3wlkd.f |
. . . . 5
⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 |
9 | | 3wlkd.s |
. . . . 5
⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) |
10 | 7, 8, 9 | 3wlkdlem3 28525 |
. . . 4
⊢ (𝜑 → (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷))) |
11 | | simpl 483 |
. . . . . . 7
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) → (𝑃‘0) = 𝐴) |
12 | | simpr 485 |
. . . . . . 7
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) → (𝑃‘1) = 𝐵) |
13 | 11, 12 | neeq12d 3005 |
. . . . . 6
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) → ((𝑃‘0) ≠ (𝑃‘1) ↔ 𝐴 ≠ 𝐵)) |
14 | 13 | adantr 481 |
. . . . 5
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → ((𝑃‘0) ≠ (𝑃‘1) ↔ 𝐴 ≠ 𝐵)) |
15 | 12 | adantr 481 |
. . . . . 6
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → (𝑃‘1) = 𝐵) |
16 | | simpl 483 |
. . . . . . 7
⊢ (((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷) → (𝑃‘2) = 𝐶) |
17 | 16 | adantl 482 |
. . . . . 6
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → (𝑃‘2) = 𝐶) |
18 | 15, 17 | neeq12d 3005 |
. . . . 5
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → ((𝑃‘1) ≠ (𝑃‘2) ↔ 𝐵 ≠ 𝐶)) |
19 | | simpr 485 |
. . . . . . 7
⊢ (((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷) → (𝑃‘3) = 𝐷) |
20 | 16, 19 | neeq12d 3005 |
. . . . . 6
⊢ (((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷) → ((𝑃‘2) ≠ (𝑃‘3) ↔ 𝐶 ≠ 𝐷)) |
21 | 20 | adantl 482 |
. . . . 5
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → ((𝑃‘2) ≠ (𝑃‘3) ↔ 𝐶 ≠ 𝐷)) |
22 | 14, 18, 21 | 3anbi123d 1435 |
. . . 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 256 |
. 2
⊢ (𝜑 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘3))) |
25 | 7, 8 | 3wlkdlem2 28524 |
. . . 4
⊢
(0..^(♯‘𝐹)) = {0, 1, 2} |
26 | 25 | raleqi 3346 |
. . 3
⊢
(∀𝑘 ∈
(0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ↔ ∀𝑘 ∈ {0, 1, 2} (𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))) |
27 | | c0ex 10969 |
. . . 4
⊢ 0 ∈
V |
28 | | 1ex 10971 |
. . . 4
⊢ 1 ∈
V |
29 | | 2ex 12050 |
. . . 4
⊢ 2 ∈
V |
30 | | fveq2 6774 |
. . . . 5
⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0)) |
31 | | fv0p1e1 12096 |
. . . . 5
⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1)) |
32 | 30, 31 | neeq12d 3005 |
. . . 4
⊢ (𝑘 = 0 → ((𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ↔ (𝑃‘0) ≠ (𝑃‘1))) |
33 | | fveq2 6774 |
. . . . 5
⊢ (𝑘 = 1 → (𝑃‘𝑘) = (𝑃‘1)) |
34 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1)) |
35 | | 1p1e2 12098 |
. . . . . . 7
⊢ (1 + 1) =
2 |
36 | 34, 35 | eqtrdi 2794 |
. . . . . 6
⊢ (𝑘 = 1 → (𝑘 + 1) = 2) |
37 | 36 | fveq2d 6778 |
. . . . 5
⊢ (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2)) |
38 | 33, 37 | neeq12d 3005 |
. . . 4
⊢ (𝑘 = 1 → ((𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ↔ (𝑃‘1) ≠ (𝑃‘2))) |
39 | | fveq2 6774 |
. . . . 5
⊢ (𝑘 = 2 → (𝑃‘𝑘) = (𝑃‘2)) |
40 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑘 = 2 → (𝑘 + 1) = (2 + 1)) |
41 | | 2p1e3 12115 |
. . . . . . 7
⊢ (2 + 1) =
3 |
42 | 40, 41 | eqtrdi 2794 |
. . . . . 6
⊢ (𝑘 = 2 → (𝑘 + 1) = 3) |
43 | 42 | fveq2d 6778 |
. . . . 5
⊢ (𝑘 = 2 → (𝑃‘(𝑘 + 1)) = (𝑃‘3)) |
44 | 39, 43 | neeq12d 3005 |
. . . 4
⊢ (𝑘 = 2 → ((𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ↔ (𝑃‘2) ≠ (𝑃‘3))) |
45 | 27, 28, 29, 32, 38, 44 | raltp 4641 |
. . 3
⊢
(∀𝑘 ∈
{0, 1, 2} (𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘3))) |
46 | 26, 45 | bitri 274 |
. 2
⊢
(∀𝑘 ∈
(0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘3))) |
47 | 24, 46 | sylibr 233 |
1
⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))) |