Metamath Proof Explorer

Theorem 1pthdlem1

Description: Lemma 1 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 1pthdlem1 
|- Fun `' ( P |` ( 1 ..^ ( # ` F ) ) )

Proof

Step Hyp Ref Expression
1 1wlkd.p 
 |-  P = <" X Y ">
2 1wlkd.f 
 |-  F = <" J ">
3 fun0 
 |-  Fun (/)
4 2 fveq2i 
 |-  ( # ` F ) = ( # ` <" J "> )
5 s1len 
 |-  ( # ` <" J "> ) = 1
6 4 5 eqtri 
 |-  ( # ` F ) = 1
7 6 oveq2i 
 |-  ( 1 ..^ ( # ` F ) ) = ( 1 ..^ 1 )
8 fzo0 
 |-  ( 1 ..^ 1 ) = (/)
9 7 8 eqtri 
 |-  ( 1 ..^ ( # ` F ) ) = (/)
10 9 reseq2i 
 |-  ( P |` ( 1 ..^ ( # ` F ) ) ) = ( P |` (/) )
11 res0 
 |-  ( P |` (/) ) = (/)
12 10 11 eqtri 
 |-  ( P |` ( 1 ..^ ( # ` F ) ) ) = (/)
13 12 cnveqi 
 |-  `' ( P |` ( 1 ..^ ( # ` F ) ) ) = `' (/)
14 cnv0 
 |-  `' (/) = (/)
15 13 14 eqtri 
 |-  `' ( P |` ( 1 ..^ ( # ` F ) ) ) = (/)
16 15 funeqi 
 |-  ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) <-> Fun (/) )
17 3 16 mpbir 
 |-  Fun `' ( P |` ( 1 ..^ ( # ` F ) ) )