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…FP⁡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=012
20 18 19 eqtri ⊢0…F=012
21 20 raleqi ⊢∀k∈0…FP⁡k∈V↔∀k∈012P⁡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∈012P⁡k∈V↔P⁡0∈V∧P⁡1∈V∧P⁡2∈V
32 21 31 bitri ⊢∀k∈0…FP⁡k∈V↔P⁡0∈V∧P⁡1∈V∧P⁡2∈V
33 14 32 sylibr ⊢φ→∀k∈0…FP⁡k∈V