Metamath Proof Explorer

Theorem 2wlkdlem4

Description: Lemma 4 for 2wlkd . (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
Assertion 2wlkdlem4 ⊢ φ → ∀ k ∈ 0 … F P ⁡ k ∈ V

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 1 2 3 2wlkdlem3 ⊢ φ → P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C
5 simp1 ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C → P ⁡ 0 = A
6 5 eleq1d ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C → P ⁡ 0 ∈ V ↔ A ∈ V
7 simp2 ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C → P ⁡ 1 = B
8 7 eleq1d ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C → P ⁡ 1 ∈ V ↔ B ∈ V
9 simp3 ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C → P ⁡ 2 = C
10 9 eleq1d ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C → P ⁡ 2 ∈ V ↔ C ∈ V
11 6 8 10 3anbi123d ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C → P ⁡ 0 ∈ V ∧ P ⁡ 1 ∈ V ∧ P ⁡ 2 ∈ V ↔ A ∈ V ∧ B ∈ V ∧ C ∈ V
12 11 bicomd ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C → A ∈ V ∧ B ∈ V ∧ C ∈ V ↔ P ⁡ 0 ∈ V ∧ P ⁡ 1 ∈ V ∧ P ⁡ 2 ∈ V
13 4 12 syl ⊢ φ → A ∈ V ∧ B ∈ V ∧ C ∈ V ↔ P ⁡ 0 ∈ V ∧ P ⁡ 1 ∈ V ∧ P ⁡ 2 ∈ V
14 3 13 mpbid ⊢ φ → P ⁡ 0 ∈ V ∧ P ⁡ 1 ∈ V ∧ P ⁡ 2 ∈ V
15 2 fveq2i ⊢ F = ⟨“ JK ”⟩
16 s2len ⊢ ⟨“ JK ”⟩ = 2
17 15 16 eqtri ⊢ F = 2
18 17 oveq2i ⊢ 0 … F = 0 … 2
19 fz0tp ⊢ 0 … 2 = 0 1 2
20 18 19 eqtri ⊢ 0 … F = 0 1 2
21 20 raleqi ⊢ ∀ k ∈ 0 … F P ⁡ k ∈ V ↔ ∀ k ∈ 0 1 2 P ⁡ k ∈ V
22 c0ex ⊢ 0 ∈ V
23 1ex ⊢ 1 ∈ V
24 2ex ⊢ 2 ∈ V
25 fveq2 ⊢ k = 0 → P ⁡ k = P ⁡ 0
26 25 eleq1d ⊢ k = 0 → P ⁡ k ∈ V ↔ P ⁡ 0 ∈ V
27 fveq2 ⊢ k = 1 → P ⁡ k = P ⁡ 1
28 27 eleq1d ⊢ k = 1 → P ⁡ k ∈ V ↔ P ⁡ 1 ∈ V
29 fveq2 ⊢ k = 2 → P ⁡ k = P ⁡ 2
30 29 eleq1d ⊢ k = 2 → P ⁡ k ∈ V ↔ P ⁡ 2 ∈ V
31 22 23 24 26 28 30 raltp ⊢ ∀ k ∈ 0 1 2 P ⁡ k ∈ V ↔ P ⁡ 0 ∈ V ∧ P ⁡ 1 ∈ V ∧ P ⁡ 2 ∈ V
32 21 31 bitri ⊢ ∀ k ∈ 0 … F P ⁡ k ∈ V ↔ P ⁡ 0 ∈ V ∧ P ⁡ 1 ∈ V ∧ P ⁡ 2 ∈ V
33 14 32 sylibr ⊢ φ → ∀ k ∈ 0 … F P ⁡ k ∈ V