Metamath Proof Explorer

Theorem wwlktovf

Description: Lemma 1 for wrd2f1tovbij . (Contributed by Alexander van der Vekens, 27-Jul-2018)

Ref Expression
Hypotheses wwlktovf1o.d 
|- D = { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) }
wwlktovf1o.r 
|- R = { n e. V | { P , n } e. X }
wwlktovf1o.f 
|- F = ( t e. D |-> ( t ` 1 ) )
Assertion wwlktovf 
|- F : D --> R

Proof

Step Hyp Ref Expression
1 wwlktovf1o.d 
 |-  D = { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) }
2 wwlktovf1o.r 
 |-  R = { n e. V | { P , n } e. X }
3 wwlktovf1o.f 
 |-  F = ( t e. D |-> ( t ` 1 ) )
4 wrdf 
 |-  ( t e. Word V -> t : ( 0 ..^ ( # ` t ) ) --> V )
5 oveq2 
 |-  ( ( # ` t ) = 2 -> ( 0 ..^ ( # ` t ) ) = ( 0 ..^ 2 ) )
6 5 feq2d 
 |-  ( ( # ` t ) = 2 -> ( t : ( 0 ..^ ( # ` t ) ) --> V <-> t : ( 0 ..^ 2 ) --> V ) )
7 1nn0 
 |-  1 e. NN0
8 2nn 
 |-  2 e. NN
9 1lt2 
 |-  1 < 2
10 elfzo0 
 |-  ( 1 e. ( 0 ..^ 2 ) <-> ( 1 e. NN0 /\ 2 e. NN /\ 1 < 2 ) )
11 7 8 9 10 mpbir3an 
 |-  1 e. ( 0 ..^ 2 )
12 ffvelrn 
 |-  ( ( t : ( 0 ..^ 2 ) --> V /\ 1 e. ( 0 ..^ 2 ) ) -> ( t ` 1 ) e. V )
13 11 12 mpan2 
 |-  ( t : ( 0 ..^ 2 ) --> V -> ( t ` 1 ) e. V )
14 6 13 syl6bi 
 |-  ( ( # ` t ) = 2 -> ( t : ( 0 ..^ ( # ` t ) ) --> V -> ( t ` 1 ) e. V ) )
15 14 3ad2ant1 
 |-  ( ( ( # ` t ) = 2 /\ ( t ` 0 ) = P /\ { ( t ` 0 ) , ( t ` 1 ) } e. X ) -> ( t : ( 0 ..^ ( # ` t ) ) --> V -> ( t ` 1 ) e. V ) )
16 4 15 mpan9 
 |-  ( ( t e. Word V /\ ( ( # ` t ) = 2 /\ ( t ` 0 ) = P /\ { ( t ` 0 ) , ( t ` 1 ) } e. X ) ) -> ( t ` 1 ) e. V )
17 preq1 
 |-  ( ( t ` 0 ) = P -> { ( t ` 0 ) , ( t ` 1 ) } = { P , ( t ` 1 ) } )
18 17 eleq1d 
 |-  ( ( t ` 0 ) = P -> ( { ( t ` 0 ) , ( t ` 1 ) } e. X <-> { P , ( t ` 1 ) } e. X ) )
19 18 biimpa 
 |-  ( ( ( t ` 0 ) = P /\ { ( t ` 0 ) , ( t ` 1 ) } e. X ) -> { P , ( t ` 1 ) } e. X )
20 19 3adant1 
 |-  ( ( ( # ` t ) = 2 /\ ( t ` 0 ) = P /\ { ( t ` 0 ) , ( t ` 1 ) } e. X ) -> { P , ( t ` 1 ) } e. X )
21 20 adantl 
 |-  ( ( t e. Word V /\ ( ( # ` t ) = 2 /\ ( t ` 0 ) = P /\ { ( t ` 0 ) , ( t ` 1 ) } e. X ) ) -> { P , ( t ` 1 ) } e. X )
22 16 21 jca 
 |-  ( ( t e. Word V /\ ( ( # ` t ) = 2 /\ ( t ` 0 ) = P /\ { ( t ` 0 ) , ( t ` 1 ) } e. X ) ) -> ( ( t ` 1 ) e. V /\ { P , ( t ` 1 ) } e. X ) )
23 fveqeq2 
 |-  ( w = t -> ( ( # ` w ) = 2 <-> ( # ` t ) = 2 ) )
24 fveq1 
 |-  ( w = t -> ( w ` 0 ) = ( t ` 0 ) )
25 24 eqeq1d 
 |-  ( w = t -> ( ( w ` 0 ) = P <-> ( t ` 0 ) = P ) )
26 fveq1 
 |-  ( w = t -> ( w ` 1 ) = ( t ` 1 ) )
27 24 26 preq12d 
 |-  ( w = t -> { ( w ` 0 ) , ( w ` 1 ) } = { ( t ` 0 ) , ( t ` 1 ) } )
28 27 eleq1d 
 |-  ( w = t -> ( { ( w ` 0 ) , ( w ` 1 ) } e. X <-> { ( t ` 0 ) , ( t ` 1 ) } e. X ) )
29 23 25 28 3anbi123d 
 |-  ( w = t -> ( ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) <-> ( ( # ` t ) = 2 /\ ( t ` 0 ) = P /\ { ( t ` 0 ) , ( t ` 1 ) } e. X ) ) )
30 29 1 elrab2 
 |-  ( t e. D <-> ( t e. Word V /\ ( ( # ` t ) = 2 /\ ( t ` 0 ) = P /\ { ( t ` 0 ) , ( t ` 1 ) } e. X ) ) )
31 preq2 
 |-  ( n = ( t ` 1 ) -> { P , n } = { P , ( t ` 1 ) } )
32 31 eleq1d 
 |-  ( n = ( t ` 1 ) -> ( { P , n } e. X <-> { P , ( t ` 1 ) } e. X ) )
33 32 2 elrab2 
 |-  ( ( t ` 1 ) e. R <-> ( ( t ` 1 ) e. V /\ { P , ( t ` 1 ) } e. X ) )
34 22 30 33 3imtr4i 
 |-  ( t e. D -> ( t ` 1 ) e. R )
35 3 34 fmpti 
 |-  F : D --> R