Metamath Proof Explorer

Theorem 3wlkdlem4

Description: Lemma 4 for 3wlkd . (Contributed by Alexander van der Vekens, 11-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
Assertion 3wlkdlem4 ⊢ φ → ∀ k ∈ 0 … F P ⁡ k ∈ V

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 1 2 3 3wlkdlem3 ⊢ φ → P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D
5 simpl ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B → P ⁡ 0 = A
6 5 eleq1d ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B → P ⁡ 0 ∈ V ↔ A ∈ V
7 simpr ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B → P ⁡ 1 = B
8 7 eleq1d ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B → P ⁡ 1 ∈ V ↔ B ∈ V
9 6 8 anbi12d ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B → P ⁡ 0 ∈ V ∧ P ⁡ 1 ∈ V ↔ A ∈ V ∧ B ∈ V
10 9 biimparc ⊢ A ∈ V ∧ B ∈ V ∧ P ⁡ 0 = A ∧ P ⁡ 1 = B → P ⁡ 0 ∈ V ∧ P ⁡ 1 ∈ V
11 c0ex ⊢ 0 ∈ V
12 1ex ⊢ 1 ∈ V
13 11 12 pm3.2i ⊢ 0 ∈ V ∧ 1 ∈ V
14 fveq2 ⊢ k = 0 → P ⁡ k = P ⁡ 0
15 14 eleq1d ⊢ k = 0 → P ⁡ k ∈ V ↔ P ⁡ 0 ∈ V
16 fveq2 ⊢ k = 1 → P ⁡ k = P ⁡ 1
17 16 eleq1d ⊢ k = 1 → P ⁡ k ∈ V ↔ P ⁡ 1 ∈ V
18 15 17 ralprg ⊢ 0 ∈ V ∧ 1 ∈ V → ∀ k ∈ 0 1 P ⁡ k ∈ V ↔ P ⁡ 0 ∈ V ∧ P ⁡ 1 ∈ V
19 13 18 mp1i ⊢ A ∈ V ∧ B ∈ V ∧ P ⁡ 0 = A ∧ P ⁡ 1 = B → ∀ k ∈ 0 1 P ⁡ k ∈ V ↔ P ⁡ 0 ∈ V ∧ P ⁡ 1 ∈ V
20 10 19 mpbird ⊢ A ∈ V ∧ B ∈ V ∧ P ⁡ 0 = A ∧ P ⁡ 1 = B → ∀ k ∈ 0 1 P ⁡ k ∈ V
21 20 ex ⊢ A ∈ V ∧ B ∈ V → P ⁡ 0 = A ∧ P ⁡ 1 = B → ∀ k ∈ 0 1 P ⁡ k ∈ V
22 simpl ⊢ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 2 = C
23 22 eleq1d ⊢ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 2 ∈ V ↔ C ∈ V
24 simpr ⊢ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 3 = D
25 24 eleq1d ⊢ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 3 ∈ V ↔ D ∈ V
26 23 25 anbi12d ⊢ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 2 ∈ V ∧ P ⁡ 3 ∈ V ↔ C ∈ V ∧ D ∈ V
27 26 biimparc ⊢ C ∈ V ∧ D ∈ V ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 2 ∈ V ∧ P ⁡ 3 ∈ V
28 2ex ⊢ 2 ∈ V
29 3ex ⊢ 3 ∈ V
30 28 29 pm3.2i ⊢ 2 ∈ V ∧ 3 ∈ V
31 fveq2 ⊢ k = 2 → P ⁡ k = P ⁡ 2
32 31 eleq1d ⊢ k = 2 → P ⁡ k ∈ V ↔ P ⁡ 2 ∈ V
33 fveq2 ⊢ k = 3 → P ⁡ k = P ⁡ 3
34 33 eleq1d ⊢ k = 3 → P ⁡ k ∈ V ↔ P ⁡ 3 ∈ V
35 32 34 ralprg ⊢ 2 ∈ V ∧ 3 ∈ V → ∀ k ∈ 2 3 P ⁡ k ∈ V ↔ P ⁡ 2 ∈ V ∧ P ⁡ 3 ∈ V
36 30 35 mp1i ⊢ C ∈ V ∧ D ∈ V ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D → ∀ k ∈ 2 3 P ⁡ k ∈ V ↔ P ⁡ 2 ∈ V ∧ P ⁡ 3 ∈ V
37 27 36 mpbird ⊢ C ∈ V ∧ D ∈ V ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D → ∀ k ∈ 2 3 P ⁡ k ∈ V
38 37 ex ⊢ C ∈ V ∧ D ∈ V → P ⁡ 2 = C ∧ P ⁡ 3 = D → ∀ k ∈ 2 3 P ⁡ k ∈ V
39 21 38 im2anan9 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D → ∀ k ∈ 0 1 P ⁡ k ∈ V ∧ ∀ k ∈ 2 3 P ⁡ k ∈ V
40 3 4 39 sylc ⊢ φ → ∀ k ∈ 0 1 P ⁡ k ∈ V ∧ ∀ k ∈ 2 3 P ⁡ k ∈ V
41 2 fveq2i ⊢ F = ⟨“ JKL ”⟩
42 s3len ⊢ ⟨“ JKL ”⟩ = 3
43 41 42 eqtri ⊢ F = 3
44 43 oveq2i ⊢ 0 … F = 0 … 3
45 fz0to3un2pr ⊢ 0 … 3 = 0 1 ∪ 2 3
46 44 45 eqtri ⊢ 0 … F = 0 1 ∪ 2 3
47 46 raleqi ⊢ ∀ k ∈ 0 … F P ⁡ k ∈ V ↔ ∀ k ∈ 0 1 ∪ 2 3 P ⁡ k ∈ V
48 ralunb ⊢ ∀ k ∈ 0 1 ∪ 2 3 P ⁡ k ∈ V ↔ ∀ k ∈ 0 1 P ⁡ k ∈ V ∧ ∀ k ∈ 2 3 P ⁡ k ∈ V
49 47 48 bitri ⊢ ∀ k ∈ 0 … F P ⁡ k ∈ V ↔ ∀ k ∈ 0 1 P ⁡ k ∈ V ∧ ∀ k ∈ 2 3 P ⁡ k ∈ V
50 40 49 sylibr ⊢ φ → ∀ k ∈ 0 … F P ⁡ k ∈ V