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 ⊢φ→AB⊆I⁡J∧BC⊆I⁡K
Assertion 2wlkdlem10 ⊢φ→∀k∈0..^FP⁡kP⁡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 ⊢φ→AB⊆I⁡J∧BC⊆I⁡K
6 1 2 3 4 5 2wlkdlem9 ⊢φ→AB⊆I⁡F⁡0∧BC⊆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⁡0P⁡1=AB
9 8 3adant3 ⊢P⁡0=A∧P⁡1=B∧P⁡2=C→P⁡0P⁡1=AB
10 9 sseq1d ⊢P⁡0=A∧P⁡1=B∧P⁡2=C→P⁡0P⁡1⊆I⁡F⁡0↔AB⊆I⁡F⁡0
11 preq12 ⊢P⁡1=B∧P⁡2=C→P⁡1P⁡2=BC
12 11 3adant1 ⊢P⁡0=A∧P⁡1=B∧P⁡2=C→P⁡1P⁡2=BC
13 12 sseq1d ⊢P⁡0=A∧P⁡1=B∧P⁡2=C→P⁡1P⁡2⊆I⁡F⁡1↔BC⊆I⁡F⁡1
14 10 13 anbi12d ⊢P⁡0=A∧P⁡1=B∧P⁡2=C→P⁡0P⁡1⊆I⁡F⁡0∧P⁡1P⁡2⊆I⁡F⁡1↔AB⊆I⁡F⁡0∧BC⊆I⁡F⁡1
15 7 14 syl ⊢φ→P⁡0P⁡1⊆I⁡F⁡0∧P⁡1P⁡2⊆I⁡F⁡1↔AB⊆I⁡F⁡0∧BC⊆I⁡F⁡1
16 6 15 mpbird ⊢φ→P⁡0P⁡1⊆I⁡F⁡0∧P⁡1P⁡2⊆I⁡F⁡1
17 1 2 2wlkdlem2 ⊢0..^F=01
18 17 raleqi ⊢∀k∈0..^FP⁡kP⁡k+1⊆I⁡F⁡k↔∀k∈01P⁡kP⁡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⁡kP⁡k+1=P⁡0P⁡1
24 2fveq3 ⊢k=0→I⁡F⁡k=I⁡F⁡0
25 23 24 sseq12d ⊢k=0→P⁡kP⁡k+1⊆I⁡F⁡k↔P⁡0P⁡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⁡kP⁡k+1=P⁡1P⁡2
32 2fveq3 ⊢k=1→I⁡F⁡k=I⁡F⁡1
33 31 32 sseq12d ⊢k=1→P⁡kP⁡k+1⊆I⁡F⁡k↔P⁡1P⁡2⊆I⁡F⁡1
34 19 20 25 33 ralpr ⊢∀k∈01P⁡kP⁡k+1⊆I⁡F⁡k↔P⁡0P⁡1⊆I⁡F⁡0∧P⁡1P⁡2⊆I⁡F⁡1
35 18 34 bitri ⊢∀k∈0..^FP⁡kP⁡k+1⊆I⁡F⁡k↔P⁡0P⁡1⊆I⁡F⁡0∧P⁡1P⁡2⊆I⁡F⁡1
36 16 35 sylibr ⊢φ→∀k∈0..^FP⁡kP⁡k+1⊆I⁡F⁡k