2wlkdlem4

	Ref	Expression
Hypotheses	2wlkd.p	\|- P = <" A B C ">
	2wlkd.f	\|- F = <" J K ">
	2wlkd.s	\|- ( ph -> ( A e. V /\ B e. V /\ C e. V ) )
Assertion	2wlkdlem4	\|- ( ph -> A. k e. ( 0 ... ( # ` F ) ) ( P ` k ) e. V )

Proof

Step	Hyp	Ref	Expression
1		2wlkd.p	\|- P = <" A B C ">
2		2wlkd.f	\|- F = <" J K ">
3		2wlkd.s	\|- ( ph -> ( A e. V /\ B e. V /\ C e. V ) )
4	1 2 3	2wlkdlem3	\|- ( ph -> ( ( 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 ) e. V <-> A e. 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 ) e. V <-> B e. 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 ) e. V <-> C e. V ) )
11	6 8 10	3anbi123d	\|- ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) -> ( ( ( P ` 0 ) e. V /\ ( P ` 1 ) e. V /\ ( P ` 2 ) e. V ) <-> ( A e. V /\ B e. V /\ C e. V ) ) )
12	11	bicomd	\|- ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) -> ( ( A e. V /\ B e. V /\ C e. V ) <-> ( ( P ` 0 ) e. V /\ ( P ` 1 ) e. V /\ ( P ` 2 ) e. V ) ) )
13	4 12	syl	\|- ( ph -> ( ( A e. V /\ B e. V /\ C e. V ) <-> ( ( P ` 0 ) e. V /\ ( P ` 1 ) e. V /\ ( P ` 2 ) e. V ) ) )
14	3 13	mpbid	\|- ( ph -> ( ( P ` 0 ) e. V /\ ( P ` 1 ) e. V /\ ( P ` 2 ) e. V ) )
15	2	fveq2i	\|- ( # ` F ) = ( # ` <" J K "> )
16		s2len	\|- ( # ` <" J K "> ) = 2
17	15 16	eqtri	\|- ( # ` F ) = 2
18	17	oveq2i	\|- ( 0 ... ( # ` F ) ) = ( 0 ... 2 )
19		fz0tp	\|- ( 0 ... 2 ) = { 0 , 1 , 2 }
20	18 19	eqtri	\|- ( 0 ... ( # ` F ) ) = { 0 , 1 , 2 }
21	20	raleqi	\|- ( A. k e. ( 0 ... ( # ` F ) ) ( P ` k ) e. V <-> A. k e. { 0 , 1 , 2 } ( P ` k ) e. V )
22		c0ex	\|- 0 e. _V
23		1ex	\|- 1 e. _V
24		2ex	\|- 2 e. _V
25		fveq2	\|- ( k = 0 -> ( P ` k ) = ( P ` 0 ) )
26	25	eleq1d	\|- ( k = 0 -> ( ( P ` k ) e. V <-> ( P ` 0 ) e. V ) )
27		fveq2	\|- ( k = 1 -> ( P ` k ) = ( P ` 1 ) )
28	27	eleq1d	\|- ( k = 1 -> ( ( P ` k ) e. V <-> ( P ` 1 ) e. V ) )
29		fveq2	\|- ( k = 2 -> ( P ` k ) = ( P ` 2 ) )
30	29	eleq1d	\|- ( k = 2 -> ( ( P ` k ) e. V <-> ( P ` 2 ) e. V ) )
31	22 23 24 26 28 30	raltp	\|- ( A. k e. { 0 , 1 , 2 } ( P ` k ) e. V <-> ( ( P ` 0 ) e. V /\ ( P ` 1 ) e. V /\ ( P ` 2 ) e. V ) )
32	21 31	bitri	\|- ( A. k e. ( 0 ... ( # ` F ) ) ( P ` k ) e. V <-> ( ( P ` 0 ) e. V /\ ( P ` 1 ) e. V /\ ( P ` 2 ) e. V ) )
33	14 32	sylibr	\|- ( ph -> A. k e. ( 0 ... ( # ` F ) ) ( P ` k ) e. V )

Metamath Proof Explorer

Theorem 2wlkdlem4

Proof