Metamath Proof Explorer

Theorem 3wlkdlem10

Description: Lemma 10 for 3wlkd . (Contributed by Alexander van der Vekens, 12-Nov-2017) (Revised by AV, 7-Feb-2021)

Ref Expression
Hypotheses 3wlkd.p ⊢ P = ⟨“ ABCD ”⟩
3wlkd.f ⊢ F = ⟨“ JKL ”⟩
3wlkd.s ⊢ φ → A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V
3wlkd.n ⊢ φ → A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ B ≠ D ∧ C ≠ D
3wlkd.e ⊢ φ → A B ⊆ I ⁡ J ∧ B C ⊆ I ⁡ K ∧ C D ⊆ I ⁡ L
Assertion 3wlkdlem10 ⊢ φ → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k

Proof

Step Hyp Ref Expression
1 3wlkd.p ⊢ P = ⟨“ ABCD ”⟩
2 3wlkd.f ⊢ F = ⟨“ JKL ”⟩
3 3wlkd.s ⊢ φ → A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V
4 3wlkd.n ⊢ φ → A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ B ≠ D ∧ C ≠ D
5 3wlkd.e ⊢ φ → A B ⊆ I ⁡ J ∧ B C ⊆ I ⁡ K ∧ C D ⊆ I ⁡ L
6 1 2 3 4 5 3wlkdlem9 ⊢ φ → A B ⊆ I ⁡ F ⁡ 0 ∧ B C ⊆ I ⁡ F ⁡ 1 ∧ C D ⊆ I ⁡ F ⁡ 2
7 1 2 3 3wlkdlem3 ⊢ φ → P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D
8 preq12 ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B → P ⁡ 0 P ⁡ 1 = A B
9 8 adantr ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 0 P ⁡ 1 = A B
10 9 sseq1d ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 0 P ⁡ 1 ⊆ I ⁡ F ⁡ 0 ↔ A B ⊆ I ⁡ F ⁡ 0
11 simplr ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 1 = B
12 simprl ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 2 = C
13 11 12 preq12d ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 1 P ⁡ 2 = B C
14 13 sseq1d ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 1 P ⁡ 2 ⊆ I ⁡ F ⁡ 1 ↔ B C ⊆ I ⁡ F ⁡ 1
15 preq12 ⊢ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 2 P ⁡ 3 = C D
16 15 adantl ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 2 P ⁡ 3 = C D
17 16 sseq1d ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 2 P ⁡ 3 ⊆ I ⁡ F ⁡ 2 ↔ C D ⊆ I ⁡ F ⁡ 2
18 10 14 17 3anbi123d ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 0 P ⁡ 1 ⊆ I ⁡ F ⁡ 0 ∧ P ⁡ 1 P ⁡ 2 ⊆ I ⁡ F ⁡ 1 ∧ P ⁡ 2 P ⁡ 3 ⊆ I ⁡ F ⁡ 2 ↔ A B ⊆ I ⁡ F ⁡ 0 ∧ B C ⊆ I ⁡ F ⁡ 1 ∧ C D ⊆ I ⁡ F ⁡ 2
19 7 18 syl ⊢ φ → P ⁡ 0 P ⁡ 1 ⊆ I ⁡ F ⁡ 0 ∧ P ⁡ 1 P ⁡ 2 ⊆ I ⁡ F ⁡ 1 ∧ P ⁡ 2 P ⁡ 3 ⊆ I ⁡ F ⁡ 2 ↔ A B ⊆ I ⁡ F ⁡ 0 ∧ B C ⊆ I ⁡ F ⁡ 1 ∧ C D ⊆ I ⁡ F ⁡ 2
20 6 19 mpbird ⊢ φ → P ⁡ 0 P ⁡ 1 ⊆ I ⁡ F ⁡ 0 ∧ P ⁡ 1 P ⁡ 2 ⊆ I ⁡ F ⁡ 1 ∧ P ⁡ 2 P ⁡ 3 ⊆ I ⁡ F ⁡ 2
21 1 2 3wlkdlem2 ⊢ 0 ..^ F = 0 1 2
22 21 raleqi ⊢ ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ↔ ∀ k ∈ 0 1 2 P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
23 c0ex ⊢ 0 ∈ V
24 1ex ⊢ 1 ∈ V
25 2ex ⊢ 2 ∈ V
26 fveq2 ⊢ k = 0 → P ⁡ k = P ⁡ 0
27 fv0p1e1 ⊢ k = 0 → P ⁡ k + 1 = P ⁡ 1
28 26 27 preq12d ⊢ k = 0 → P ⁡ k P ⁡ k + 1 = P ⁡ 0 P ⁡ 1
29 2fveq3 ⊢ k = 0 → I ⁡ F ⁡ k = I ⁡ F ⁡ 0
30 28 29 sseq12d ⊢ k = 0 → P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ↔ P ⁡ 0 P ⁡ 1 ⊆ I ⁡ F ⁡ 0
31 fveq2 ⊢ k = 1 → P ⁡ k = P ⁡ 1
32 oveq1 ⊢ k = 1 → k + 1 = 1 + 1
33 1p1e2 ⊢ 1 + 1 = 2
34 32 33 eqtrdi ⊢ k = 1 → k + 1 = 2
35 34 fveq2d ⊢ k = 1 → P ⁡ k + 1 = P ⁡ 2
36 31 35 preq12d ⊢ k = 1 → P ⁡ k P ⁡ k + 1 = P ⁡ 1 P ⁡ 2
37 2fveq3 ⊢ k = 1 → I ⁡ F ⁡ k = I ⁡ F ⁡ 1
38 36 37 sseq12d ⊢ k = 1 → P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ↔ P ⁡ 1 P ⁡ 2 ⊆ I ⁡ F ⁡ 1
39 fveq2 ⊢ k = 2 → P ⁡ k = P ⁡ 2
40 oveq1 ⊢ k = 2 → k + 1 = 2 + 1
41 2p1e3 ⊢ 2 + 1 = 3
42 40 41 eqtrdi ⊢ k = 2 → k + 1 = 3
43 42 fveq2d ⊢ k = 2 → P ⁡ k + 1 = P ⁡ 3
44 39 43 preq12d ⊢ k = 2 → P ⁡ k P ⁡ k + 1 = P ⁡ 2 P ⁡ 3
45 2fveq3 ⊢ k = 2 → I ⁡ F ⁡ k = I ⁡ F ⁡ 2
46 44 45 sseq12d ⊢ k = 2 → P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ↔ P ⁡ 2 P ⁡ 3 ⊆ I ⁡ F ⁡ 2
47 23 24 25 30 38 46 raltp ⊢ ∀ k ∈ 0 1 2 P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ↔ P ⁡ 0 P ⁡ 1 ⊆ I ⁡ F ⁡ 0 ∧ P ⁡ 1 P ⁡ 2 ⊆ I ⁡ F ⁡ 1 ∧ P ⁡ 2 P ⁡ 3 ⊆ I ⁡ F ⁡ 2
48 22 47 bitri ⊢ ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ↔ P ⁡ 0 P ⁡ 1 ⊆ I ⁡ F ⁡ 0 ∧ P ⁡ 1 P ⁡ 2 ⊆ I ⁡ F ⁡ 1 ∧ P ⁡ 2 P ⁡ 3 ⊆ I ⁡ F ⁡ 2
49 20 48 sylibr ⊢ φ → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k