This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = <" A B C D ">
3wlkd.f 
|- F = <" J K L ">
3wlkd.s 
|- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )
Assertion 3wlkdlem4 
|- ( ph -> A. k e. ( 0 ... ( # ` F ) ) ( P ` k ) e. V )

Proof

Step Hyp Ref Expression
1 3wlkd.p 
 |-  P = <" A B C D ">
2 3wlkd.f 
 |-  F = <" J K L ">
3 3wlkd.s 
 |-  ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )
4 1 2 3 3wlkdlem3 
 |-  ( ph -> ( ( ( 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 ) e. V <-> A e. V ) )
7 simpr 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) -> ( P ` 1 ) = B )
8 7 eleq1d 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) -> ( ( P ` 1 ) e. V <-> B e. V ) )
9 6 8 anbi12d 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) -> ( ( ( P ` 0 ) e. V /\ ( P ` 1 ) e. V ) <-> ( A e. V /\ B e. V ) ) )
10 9 biimparc 
 |-  ( ( ( A e. V /\ B e. V ) /\ ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) ) -> ( ( P ` 0 ) e. V /\ ( P ` 1 ) e. V ) )
11 c0ex 
 |-  0 e. _V
12 1ex 
 |-  1 e. _V
13 11 12 pm3.2i 
 |-  ( 0 e. _V /\ 1 e. _V )
14 fveq2 
 |-  ( k = 0 -> ( P ` k ) = ( P ` 0 ) )
15 14 eleq1d 
 |-  ( k = 0 -> ( ( P ` k ) e. V <-> ( P ` 0 ) e. V ) )
16 fveq2 
 |-  ( k = 1 -> ( P ` k ) = ( P ` 1 ) )
17 16 eleq1d 
 |-  ( k = 1 -> ( ( P ` k ) e. V <-> ( P ` 1 ) e. V ) )
18 15 17 ralprg 
 |-  ( ( 0 e. _V /\ 1 e. _V ) -> ( A. k e. { 0 , 1 } ( P ` k ) e. V <-> ( ( P ` 0 ) e. V /\ ( P ` 1 ) e. V ) ) )
19 13 18 mp1i 
 |-  ( ( ( A e. V /\ B e. V ) /\ ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) ) -> ( A. k e. { 0 , 1 } ( P ` k ) e. V <-> ( ( P ` 0 ) e. V /\ ( P ` 1 ) e. V ) ) )
20 10 19 mpbird 
 |-  ( ( ( A e. V /\ B e. V ) /\ ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) ) -> A. k e. { 0 , 1 } ( P ` k ) e. V )
21 20 ex 
 |-  ( ( A e. V /\ B e. V ) -> ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) -> A. k e. { 0 , 1 } ( P ` k ) e. V ) )
22 simpl 
 |-  ( ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) -> ( P ` 2 ) = C )
23 22 eleq1d 
 |-  ( ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) -> ( ( P ` 2 ) e. V <-> C e. V ) )
24 simpr 
 |-  ( ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) -> ( P ` 3 ) = D )
25 24 eleq1d 
 |-  ( ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) -> ( ( P ` 3 ) e. V <-> D e. V ) )
26 23 25 anbi12d 
 |-  ( ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) -> ( ( ( P ` 2 ) e. V /\ ( P ` 3 ) e. V ) <-> ( C e. V /\ D e. V ) ) )
27 26 biimparc 
 |-  ( ( ( C e. V /\ D e. V ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> ( ( P ` 2 ) e. V /\ ( P ` 3 ) e. V ) )
28 2ex 
 |-  2 e. _V
29 3ex 
 |-  3 e. _V
30 28 29 pm3.2i 
 |-  ( 2 e. _V /\ 3 e. _V )
31 fveq2 
 |-  ( k = 2 -> ( P ` k ) = ( P ` 2 ) )
32 31 eleq1d 
 |-  ( k = 2 -> ( ( P ` k ) e. V <-> ( P ` 2 ) e. V ) )
33 fveq2 
 |-  ( k = 3 -> ( P ` k ) = ( P ` 3 ) )
34 33 eleq1d 
 |-  ( k = 3 -> ( ( P ` k ) e. V <-> ( P ` 3 ) e. V ) )
35 32 34 ralprg 
 |-  ( ( 2 e. _V /\ 3 e. _V ) -> ( A. k e. { 2 , 3 } ( P ` k ) e. V <-> ( ( P ` 2 ) e. V /\ ( P ` 3 ) e. V ) ) )
36 30 35 mp1i 
 |-  ( ( ( C e. V /\ D e. V ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> ( A. k e. { 2 , 3 } ( P ` k ) e. V <-> ( ( P ` 2 ) e. V /\ ( P ` 3 ) e. V ) ) )
37 27 36 mpbird 
 |-  ( ( ( C e. V /\ D e. V ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> A. k e. { 2 , 3 } ( P ` k ) e. V )
38 37 ex 
 |-  ( ( C e. V /\ D e. V ) -> ( ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) -> A. k e. { 2 , 3 } ( P ` k ) e. V ) )
39 21 38 im2anan9 
 |-  ( ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> ( A. k e. { 0 , 1 } ( P ` k ) e. V /\ A. k e. { 2 , 3 } ( P ` k ) e. V ) ) )
40 3 4 39 sylc 
 |-  ( ph -> ( A. k e. { 0 , 1 } ( P ` k ) e. V /\ A. k e. { 2 , 3 } ( P ` k ) e. V ) )
41 2 fveq2i 
 |-  ( # ` F ) = ( # ` <" J K L "> )
42 s3len 
 |-  ( # ` <" J K L "> ) = 3
43 41 42 eqtri 
 |-  ( # ` F ) = 3
44 43 oveq2i 
 |-  ( 0 ... ( # ` F ) ) = ( 0 ... 3 )
45 fz0to3un2pr 
 |-  ( 0 ... 3 ) = ( { 0 , 1 } u. { 2 , 3 } )
46 44 45 eqtri 
 |-  ( 0 ... ( # ` F ) ) = ( { 0 , 1 } u. { 2 , 3 } )
47 46 raleqi 
 |-  ( A. k e. ( 0 ... ( # ` F ) ) ( P ` k ) e. V <-> A. k e. ( { 0 , 1 } u. { 2 , 3 } ) ( P ` k ) e. V )
48 ralunb 
 |-  ( A. k e. ( { 0 , 1 } u. { 2 , 3 } ) ( P ` k ) e. V <-> ( A. k e. { 0 , 1 } ( P ` k ) e. V /\ A. k e. { 2 , 3 } ( P ` k ) e. V ) )
49 47 48 bitri 
 |-  ( A. k e. ( 0 ... ( # ` F ) ) ( P ` k ) e. V <-> ( A. k e. { 0 , 1 } ( P ` k ) e. V /\ A. k e. { 2 , 3 } ( P ` k ) e. V ) )
50 40 49 sylibr 
 |-  ( ph -> A. k e. ( 0 ... ( # ` F ) ) ( P ` k ) e. V )