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…FP⁡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∈01P⁡k∈V↔P⁡0∈V∧P⁡1∈V
19 13 18 mp1i ⊢A∈V∧B∈V∧P⁡0=A∧P⁡1=B→∀k∈01P⁡k∈V↔P⁡0∈V∧P⁡1∈V
20 10 19 mpbird ⊢A∈V∧B∈V∧P⁡0=A∧P⁡1=B→∀k∈01P⁡k∈V
21 20 ex ⊢A∈V∧B∈V→P⁡0=A∧P⁡1=B→∀k∈01P⁡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∈23P⁡k∈V↔P⁡2∈V∧P⁡3∈V
36 30 35 mp1i ⊢C∈V∧D∈V∧P⁡2=C∧P⁡3=D→∀k∈23P⁡k∈V↔P⁡2∈V∧P⁡3∈V
37 27 36 mpbird ⊢C∈V∧D∈V∧P⁡2=C∧P⁡3=D→∀k∈23P⁡k∈V
38 37 ex ⊢C∈V∧D∈V→P⁡2=C∧P⁡3=D→∀k∈23P⁡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∈01P⁡k∈V∧∀k∈23P⁡k∈V
40 3 4 39 sylc ⊢φ→∀k∈01P⁡k∈V∧∀k∈23P⁡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=01∪23
46 44 45 eqtri ⊢0…F=01∪23
47 46 raleqi ⊢∀k∈0…FP⁡k∈V↔∀k∈01∪23P⁡k∈V
48 ralunb ⊢∀k∈01∪23P⁡k∈V↔∀k∈01P⁡k∈V∧∀k∈23P⁡k∈V
49 47 48 bitri ⊢∀k∈0…FP⁡k∈V↔∀k∈01P⁡k∈V∧∀k∈23P⁡k∈V
50 40 49 sylibr ⊢φ→∀k∈0…FP⁡k∈V