Theorem 1pthdlem2

Description: Lemma 2 for 1pthd . (Contributed by Alexander van der Vekens, 4-Dec-2017) (Revised by AV, 22-Jan-2021)

	Ref	Expression
Hypotheses	1wlkd.p	|- P = <" X Y ">
	1wlkd.f	|- F = <" J ">
Assertion	1pthdlem2	|- ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/)

Proof

Step	Hyp	Ref	Expression
1		1wlkd.p	|- P = <" X Y ">
2		1wlkd.f	|- F = <" J ">
3	2	fveq2i	|- ( # ` F ) = ( # ` <" J "> )
4		s1len	|- ( # ` <" J "> ) = 1
5	3 4	eqtri	|- ( # ` F ) = 1
6	5	oveq2i	|- ( 1 ..^ ( # ` F ) ) = ( 1 ..^ 1 )
7		fzo0	|- ( 1 ..^ 1 ) = (/)
8	6 7	eqtri	|- ( 1 ..^ ( # ` F ) ) = (/)
9	8	imaeq2i	|- ( P " ( 1 ..^ ( # ` F ) ) ) = ( P " (/) )
10	9	ineq2i	|- ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = ( ( P " { 0 , ( # ` F ) } ) i^i ( P " (/) ) )
11		ima0	|- ( P " (/) ) = (/)
12	11	ineq2i	|- ( ( P " { 0 , ( # ` F ) } ) i^i ( P " (/) ) ) = ( ( P " { 0 , ( # ` F ) } ) i^i (/) )
13		in0	|- ( ( P " { 0 , ( # ` F ) } ) i^i (/) ) = (/)
14	12 13	eqtri	|- ( ( P " { 0 , ( # ` F ) } ) i^i ( P " (/) ) ) = (/)
15	10 14	eqtri	|- ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/)