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 30187 | . . 3
⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘(𝐹‘0)) ∧ {𝐵, 𝐶} ⊆ (𝐼‘(𝐹‘1)) ∧ {𝐶, 𝐷} ⊆ (𝐼‘(𝐹‘2)))) | 
| 7 | 1, 2, 3 | 3wlkdlem3 30180 | . . . 4
⊢ (𝜑 → (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷))) | 
| 8 |  | preq12 4735 | . . . . . . 7
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) → {(𝑃‘0), (𝑃‘1)} = {𝐴, 𝐵}) | 
| 9 | 8 | adantr 480 | . . . . . 6
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → {(𝑃‘0), (𝑃‘1)} = {𝐴, 𝐵}) | 
| 10 | 9 | sseq1d 4015 | . . . . 5
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → ({(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)) ↔ {𝐴, 𝐵} ⊆ (𝐼‘(𝐹‘0)))) | 
| 11 |  | simplr 769 | . . . . . . 7
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → (𝑃‘1) = 𝐵) | 
| 12 |  | simprl 771 | . . . . . . 7
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → (𝑃‘2) = 𝐶) | 
| 13 | 11, 12 | preq12d 4741 | . . . . . 6
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → {(𝑃‘1), (𝑃‘2)} = {𝐵, 𝐶}) | 
| 14 | 13 | sseq1d 4015 | . . . . 5
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → ({(𝑃‘1), (𝑃‘2)} ⊆ (𝐼‘(𝐹‘1)) ↔ {𝐵, 𝐶} ⊆ (𝐼‘(𝐹‘1)))) | 
| 15 |  | preq12 4735 | . . . . . . 7
⊢ (((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷) → {(𝑃‘2), (𝑃‘3)} = {𝐶, 𝐷}) | 
| 16 | 15 | adantl 481 | . . . . . 6
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → {(𝑃‘2), (𝑃‘3)} = {𝐶, 𝐷}) | 
| 17 | 16 | sseq1d 4015 | . . . . 5
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)) → ({(𝑃‘2), (𝑃‘3)} ⊆ (𝐼‘(𝐹‘2)) ↔ {𝐶, 𝐷} ⊆ (𝐼‘(𝐹‘2)))) | 
| 18 | 10, 14, 17 | 3anbi123d 1438 | . . . 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 257 | . 2
⊢ (𝜑 → ({(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)) ∧ {(𝑃‘1), (𝑃‘2)} ⊆ (𝐼‘(𝐹‘1)) ∧ {(𝑃‘2), (𝑃‘3)} ⊆ (𝐼‘(𝐹‘2)))) | 
| 21 | 1, 2 | 3wlkdlem2 30179 | . . . 4
⊢
(0..^(♯‘𝐹)) = {0, 1, 2} | 
| 22 | 21 | raleqi 3324 | . . 3
⊢
(∀𝑘 ∈
(0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)) ↔ ∀𝑘 ∈ {0, 1, 2} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) | 
| 23 |  | c0ex 11255 | . . . 4
⊢ 0 ∈
V | 
| 24 |  | 1ex 11257 | . . . 4
⊢ 1 ∈
V | 
| 25 |  | 2ex 12343 | . . . 4
⊢ 2 ∈
V | 
| 26 |  | fveq2 6906 | . . . . . 6
⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0)) | 
| 27 |  | fv0p1e1 12389 | . . . . . 6
⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1)) | 
| 28 | 26, 27 | preq12d 4741 | . . . . 5
⊢ (𝑘 = 0 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)}) | 
| 29 |  | 2fveq3 6911 | . . . . 5
⊢ (𝑘 = 0 → (𝐼‘(𝐹‘𝑘)) = (𝐼‘(𝐹‘0))) | 
| 30 | 28, 29 | sseq12d 4017 | . . . 4
⊢ (𝑘 = 0 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)) ↔ {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)))) | 
| 31 |  | fveq2 6906 | . . . . . 6
⊢ (𝑘 = 1 → (𝑃‘𝑘) = (𝑃‘1)) | 
| 32 |  | oveq1 7438 | . . . . . . . 8
⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1)) | 
| 33 |  | 1p1e2 12391 | . . . . . . . 8
⊢ (1 + 1) =
2 | 
| 34 | 32, 33 | eqtrdi 2793 | . . . . . . 7
⊢ (𝑘 = 1 → (𝑘 + 1) = 2) | 
| 35 | 34 | fveq2d 6910 | . . . . . 6
⊢ (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2)) | 
| 36 | 31, 35 | preq12d 4741 | . . . . 5
⊢ (𝑘 = 1 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘1), (𝑃‘2)}) | 
| 37 |  | 2fveq3 6911 | . . . . 5
⊢ (𝑘 = 1 → (𝐼‘(𝐹‘𝑘)) = (𝐼‘(𝐹‘1))) | 
| 38 | 36, 37 | sseq12d 4017 | . . . 4
⊢ (𝑘 = 1 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)) ↔ {(𝑃‘1), (𝑃‘2)} ⊆ (𝐼‘(𝐹‘1)))) | 
| 39 |  | fveq2 6906 | . . . . . 6
⊢ (𝑘 = 2 → (𝑃‘𝑘) = (𝑃‘2)) | 
| 40 |  | oveq1 7438 | . . . . . . . 8
⊢ (𝑘 = 2 → (𝑘 + 1) = (2 + 1)) | 
| 41 |  | 2p1e3 12408 | . . . . . . . 8
⊢ (2 + 1) =
3 | 
| 42 | 40, 41 | eqtrdi 2793 | . . . . . . 7
⊢ (𝑘 = 2 → (𝑘 + 1) = 3) | 
| 43 | 42 | fveq2d 6910 | . . . . . 6
⊢ (𝑘 = 2 → (𝑃‘(𝑘 + 1)) = (𝑃‘3)) | 
| 44 | 39, 43 | preq12d 4741 | . . . . 5
⊢ (𝑘 = 2 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘2), (𝑃‘3)}) | 
| 45 |  | 2fveq3 6911 | . . . . 5
⊢ (𝑘 = 2 → (𝐼‘(𝐹‘𝑘)) = (𝐼‘(𝐹‘2))) | 
| 46 | 44, 45 | sseq12d 4017 | . . . 4
⊢ (𝑘 = 2 → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)) ↔ {(𝑃‘2), (𝑃‘3)} ⊆ (𝐼‘(𝐹‘2)))) | 
| 47 | 23, 24, 25, 30, 38, 46 | raltp 4705 | . . 3
⊢
(∀𝑘 ∈
{0, 1, 2} {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)) ↔ ({(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)) ∧ {(𝑃‘1), (𝑃‘2)} ⊆ (𝐼‘(𝐹‘1)) ∧ {(𝑃‘2), (𝑃‘3)} ⊆ (𝐼‘(𝐹‘2)))) | 
| 48 | 22, 47 | bitri 275 | . 2
⊢
(∀𝑘 ∈
(0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)) ↔ ({(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)) ∧ {(𝑃‘1), (𝑃‘2)} ⊆ (𝐼‘(𝐹‘1)) ∧ {(𝑃‘2), (𝑃‘3)} ⊆ (𝐼‘(𝐹‘2)))) | 
| 49 | 20, 48 | sylibr 234 | 1
⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) |