Metamath Proof Explorer

Theorem 2wlkdlem10

Description: Lemma 10 for 3wlkd . (Contributed by AV, 14-Feb-2021)

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

Proof

Step Hyp Ref Expression
1 2wlkd.p ⊢ P = ⟨“ ABC ”⟩
2 2wlkd.f ⊢ F = ⟨“ JK ”⟩
3 2wlkd.s ⊢ φ → A ∈ V ∧ B ∈ V ∧ C ∈ V
4 2wlkd.n ⊢ φ → A ≠ B ∧ B ≠ C
5 2wlkd.e ⊢ φ → A B ⊆ I ⁡ J ∧ B C ⊆ I ⁡ K
6 1 2 3 4 5 2wlkdlem9 ⊢ φ → A B ⊆ I ⁡ F ⁡ 0 ∧ B C ⊆ I ⁡ F ⁡ 1
7 1 2 3 2wlkdlem3 ⊢ φ → P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C
8 preq12 ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B → P ⁡ 0 P ⁡ 1 = A B
9 8 3adant3 ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C → P ⁡ 0 P ⁡ 1 = A B
10 9 sseq1d ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C → P ⁡ 0 P ⁡ 1 ⊆ I ⁡ F ⁡ 0 ↔ A B ⊆ I ⁡ F ⁡ 0
11 preq12 ⊢ P ⁡ 1 = B ∧ P ⁡ 2 = C → P ⁡ 1 P ⁡ 2 = B C
12 11 3adant1 ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C → P ⁡ 1 P ⁡ 2 = B C
13 12 sseq1d ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C → P ⁡ 1 P ⁡ 2 ⊆ I ⁡ F ⁡ 1 ↔ B C ⊆ I ⁡ F ⁡ 1
14 10 13 anbi12d ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C → P ⁡ 0 P ⁡ 1 ⊆ I ⁡ F ⁡ 0 ∧ P ⁡ 1 P ⁡ 2 ⊆ I ⁡ F ⁡ 1 ↔ A B ⊆ I ⁡ F ⁡ 0 ∧ B C ⊆ I ⁡ F ⁡ 1
15 7 14 syl ⊢ φ → P ⁡ 0 P ⁡ 1 ⊆ I ⁡ F ⁡ 0 ∧ P ⁡ 1 P ⁡ 2 ⊆ I ⁡ F ⁡ 1 ↔ A B ⊆ I ⁡ F ⁡ 0 ∧ B C ⊆ I ⁡ F ⁡ 1
16 6 15 mpbird ⊢ φ → P ⁡ 0 P ⁡ 1 ⊆ I ⁡ F ⁡ 0 ∧ P ⁡ 1 P ⁡ 2 ⊆ I ⁡ F ⁡ 1
17 1 2 2wlkdlem2 ⊢ 0 ..^ F = 0 1
18 17 raleqi ⊢ ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ↔ ∀ k ∈ 0 1 P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
19 c0ex ⊢ 0 ∈ V
20 1ex ⊢ 1 ∈ V
21 fveq2 ⊢ k = 0 → P ⁡ k = P ⁡ 0
22 fv0p1e1 ⊢ k = 0 → P ⁡ k + 1 = P ⁡ 1
23 21 22 preq12d ⊢ k = 0 → P ⁡ k P ⁡ k + 1 = P ⁡ 0 P ⁡ 1
24 2fveq3 ⊢ k = 0 → I ⁡ F ⁡ k = I ⁡ F ⁡ 0
25 23 24 sseq12d ⊢ k = 0 → P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ↔ P ⁡ 0 P ⁡ 1 ⊆ I ⁡ F ⁡ 0
26 fveq2 ⊢ k = 1 → P ⁡ k = P ⁡ 1
27 oveq1 ⊢ k = 1 → k + 1 = 1 + 1
28 1p1e2 ⊢ 1 + 1 = 2
29 27 28 eqtrdi ⊢ k = 1 → k + 1 = 2
30 29 fveq2d ⊢ k = 1 → P ⁡ k + 1 = P ⁡ 2
31 26 30 preq12d ⊢ k = 1 → P ⁡ k P ⁡ k + 1 = P ⁡ 1 P ⁡ 2
32 2fveq3 ⊢ k = 1 → I ⁡ F ⁡ k = I ⁡ F ⁡ 1
33 31 32 sseq12d ⊢ k = 1 → P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ↔ P ⁡ 1 P ⁡ 2 ⊆ I ⁡ F ⁡ 1
34 19 20 25 33 ralpr ⊢ ∀ k ∈ 0 1 P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ↔ P ⁡ 0 P ⁡ 1 ⊆ I ⁡ F ⁡ 0 ∧ P ⁡ 1 P ⁡ 2 ⊆ I ⁡ F ⁡ 1
35 18 34 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
36 16 35 sylibr ⊢ φ → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k