Proof of Theorem 3wlkdlem10
Step | Hyp | Ref
| Expression |
1 | | 3wlkd.p |
. . . 4
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 |
2 | | 3wlkd.f |
. . . 4
⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 |
3 | | 3wlkd.s |
. . . 4
⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) |
4 | | 3wlkd.n |
. . . 4
⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) |
5 | | 3wlkd.e |
. . . 4
⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) |
6 | 1, 2, 3, 4, 5 | 3wlkdlem9 28532 |
. . 3
⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘(𝐹‘0)) ∧ {𝐵, 𝐶} ⊆ (𝐼‘(𝐹‘1)) ∧ {𝐶, 𝐷} ⊆ (𝐼‘(𝐹‘2)))) |
7 | 1, 2, 3 | 3wlkdlem3 28525 |
. . . 4
⊢ (𝜑 → (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷))) |
8 | | preq12 4671 |
. . . . . . 7
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) → {(𝑃‘0), (𝑃‘1)} = {𝐴, 𝐵}) |
9 | 8 | adantr 481 |
. . . . . 6
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → {(𝑃‘0), (𝑃‘1)} = {𝐴, 𝐵}) |
10 | 9 | sseq1d 3952 |
. . . . 5
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → ({(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)) ↔ {𝐴, 𝐵} ⊆ (𝐼‘(𝐹‘0)))) |
11 | | simplr 766 |
. . . . . . 7
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → (𝑃‘1) = 𝐵) |
12 | | simprl 768 |
. . . . . . 7
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → (𝑃‘2) = 𝐶) |
13 | 11, 12 | preq12d 4677 |
. . . . . 6
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → {(𝑃‘1), (𝑃‘2)} = {𝐵, 𝐶}) |
14 | 13 | sseq1d 3952 |
. . . . 5
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → ({(𝑃‘1), (𝑃‘2)} ⊆ (𝐼‘(𝐹‘1)) ↔ {𝐵, 𝐶} ⊆ (𝐼‘(𝐹‘1)))) |
15 | | preq12 4671 |
. . . . . . 7
⊢ (((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷) → {(𝑃‘2), (𝑃‘3)} = {𝐶, 𝐷}) |
16 | 15 | adantl 482 |
. . . . . 6
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → {(𝑃‘2), (𝑃‘3)} = {𝐶, 𝐷}) |
17 | 16 | sseq1d 3952 |
. . . . 5
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → ({(𝑃‘2), (𝑃‘3)} ⊆ (𝐼‘(𝐹‘2)) ↔ {𝐶, 𝐷} ⊆ (𝐼‘(𝐹‘2)))) |
18 | 10, 14, 17 | 3anbi123d 1435 |
. . . 4
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → (({(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)) ∧ {(𝑃‘1), (𝑃‘2)} ⊆ (𝐼‘(𝐹‘1)) ∧ {(𝑃‘2), (𝑃‘3)} ⊆ (𝐼‘(𝐹‘2))) ↔ ({𝐴, 𝐵} ⊆ (𝐼‘(𝐹‘0)) ∧ {𝐵, 𝐶} ⊆ (𝐼‘(𝐹‘1)) ∧ {𝐶, 𝐷} ⊆ (𝐼‘(𝐹‘2))))) |
19 | 7, 18 | syl 17 |
. . 3
⊢ (𝜑 → (({(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)) ∧ {(𝑃‘1), (𝑃‘2)} ⊆ (𝐼‘(𝐹‘1)) ∧ {(𝑃‘2), (𝑃‘3)} ⊆ (𝐼‘(𝐹‘2))) ↔ ({𝐴, 𝐵} ⊆ (𝐼‘(𝐹‘0)) ∧ {𝐵, 𝐶} ⊆ (𝐼‘(𝐹‘1)) ∧ {𝐶, 𝐷} ⊆ (𝐼‘(𝐹‘2))))) |
20 | 6, 19 | mpbird 256 |
. 2
⊢ (𝜑 → ({(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)) ∧ {(𝑃‘1), (𝑃‘2)} ⊆ (𝐼‘(𝐹‘1)) ∧ {(𝑃‘2), (𝑃‘3)} ⊆ (𝐼‘(𝐹‘2)))) |
21 | 1, 2 | 3wlkdlem2 28524 |
. . . 4
⊢
(0..^(♯‘𝐹)) = {0, 1, 2} |
22 | 21 | raleqi 3346 |
. . 3
⊢
(∀𝑘 ∈
(0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)) ↔ ∀𝑘 ∈ {0, 1, 2} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) |
23 | | c0ex 10969 |
. . . 4
⊢ 0 ∈
V |
24 | | 1ex 10971 |
. . . 4
⊢ 1 ∈
V |
25 | | 2ex 12050 |
. . . 4
⊢ 2 ∈
V |
26 | | fveq2 6774 |
. . . . . 6
⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0)) |
27 | | fv0p1e1 12096 |
. . . . . 6
⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1)) |
28 | 26, 27 | preq12d 4677 |
. . . . 5
⊢ (𝑘 = 0 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)}) |
29 | | 2fveq3 6779 |
. . . . 5
⊢ (𝑘 = 0 → (𝐼‘(𝐹‘𝑘)) = (𝐼‘(𝐹‘0))) |
30 | 28, 29 | sseq12d 3954 |
. . . 4
⊢ (𝑘 = 0 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)) ↔ {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)))) |
31 | | fveq2 6774 |
. . . . . 6
⊢ (𝑘 = 1 → (𝑃‘𝑘) = (𝑃‘1)) |
32 | | oveq1 7282 |
. . . . . . . 8
⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1)) |
33 | | 1p1e2 12098 |
. . . . . . . 8
⊢ (1 + 1) =
2 |
34 | 32, 33 | eqtrdi 2794 |
. . . . . . 7
⊢ (𝑘 = 1 → (𝑘 + 1) = 2) |
35 | 34 | fveq2d 6778 |
. . . . . 6
⊢ (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2)) |
36 | 31, 35 | preq12d 4677 |
. . . . 5
⊢ (𝑘 = 1 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘1), (𝑃‘2)}) |
37 | | 2fveq3 6779 |
. . . . 5
⊢ (𝑘 = 1 → (𝐼‘(𝐹‘𝑘)) = (𝐼‘(𝐹‘1))) |
38 | 36, 37 | sseq12d 3954 |
. . . 4
⊢ (𝑘 = 1 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)) ↔ {(𝑃‘1), (𝑃‘2)} ⊆ (𝐼‘(𝐹‘1)))) |
39 | | fveq2 6774 |
. . . . . 6
⊢ (𝑘 = 2 → (𝑃‘𝑘) = (𝑃‘2)) |
40 | | oveq1 7282 |
. . . . . . . 8
⊢ (𝑘 = 2 → (𝑘 + 1) = (2 + 1)) |
41 | | 2p1e3 12115 |
. . . . . . . 8
⊢ (2 + 1) =
3 |
42 | 40, 41 | eqtrdi 2794 |
. . . . . . 7
⊢ (𝑘 = 2 → (𝑘 + 1) = 3) |
43 | 42 | fveq2d 6778 |
. . . . . 6
⊢ (𝑘 = 2 → (𝑃‘(𝑘 + 1)) = (𝑃‘3)) |
44 | 39, 43 | preq12d 4677 |
. . . . 5
⊢ (𝑘 = 2 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘2), (𝑃‘3)}) |
45 | | 2fveq3 6779 |
. . . . 5
⊢ (𝑘 = 2 → (𝐼‘(𝐹‘𝑘)) = (𝐼‘(𝐹‘2))) |
46 | 44, 45 | sseq12d 3954 |
. . . 4
⊢ (𝑘 = 2 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)) ↔ {(𝑃‘2), (𝑃‘3)} ⊆ (𝐼‘(𝐹‘2)))) |
47 | 23, 24, 25, 30, 38, 46 | raltp 4641 |
. . 3
⊢
(∀𝑘 ∈
{0, 1, 2} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)) ↔ ({(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)) ∧ {(𝑃‘1), (𝑃‘2)} ⊆ (𝐼‘(𝐹‘1)) ∧ {(𝑃‘2), (𝑃‘3)} ⊆ (𝐼‘(𝐹‘2)))) |
48 | 22, 47 | bitri 274 |
. 2
⊢
(∀𝑘 ∈
(0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)) ↔ ({(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)) ∧ {(𝑃‘1), (𝑃‘2)} ⊆ (𝐼‘(𝐹‘1)) ∧ {(𝑃‘2), (𝑃‘3)} ⊆ (𝐼‘(𝐹‘2)))) |
49 | 20, 48 | sylibr 233 |
1
⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) |