Metamath Proof Explorer

Theorem wwlktovf1

Description: Lemma 2 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 wwlktovf1 
|- F : D -1-1-> 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 1 2 3 wwlktovf 
 |-  F : D --> R
5 fveq1 
 |-  ( t = x -> ( t ` 1 ) = ( x ` 1 ) )
6 fvex 
 |-  ( x ` 1 ) e. _V
7 5 3 6 fvmpt 
 |-  ( x e. D -> ( F ` x ) = ( x ` 1 ) )
8 fveq1 
 |-  ( t = y -> ( t ` 1 ) = ( y ` 1 ) )
9 fvex 
 |-  ( y ` 1 ) e. _V
10 8 3 9 fvmpt 
 |-  ( y e. D -> ( F ` y ) = ( y ` 1 ) )
11 7 10 eqeqan12d 
 |-  ( ( x e. D /\ y e. D ) -> ( ( F ` x ) = ( F ` y ) <-> ( x ` 1 ) = ( y ` 1 ) ) )
12 fveqeq2 
 |-  ( w = x -> ( ( # ` w ) = 2 <-> ( # ` x ) = 2 ) )
13 fveq1 
 |-  ( w = x -> ( w ` 0 ) = ( x ` 0 ) )
14 13 eqeq1d 
 |-  ( w = x -> ( ( w ` 0 ) = P <-> ( x ` 0 ) = P ) )
15 fveq1 
 |-  ( w = x -> ( w ` 1 ) = ( x ` 1 ) )
16 13 15 preq12d 
 |-  ( w = x -> { ( w ` 0 ) , ( w ` 1 ) } = { ( x ` 0 ) , ( x ` 1 ) } )
17 16 eleq1d 
 |-  ( w = x -> ( { ( w ` 0 ) , ( w ` 1 ) } e. X <-> { ( x ` 0 ) , ( x ` 1 ) } e. X ) )
18 12 14 17 3anbi123d 
 |-  ( w = x -> ( ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) <-> ( ( # ` x ) = 2 /\ ( x ` 0 ) = P /\ { ( x ` 0 ) , ( x ` 1 ) } e. X ) ) )
19 18 1 elrab2 
 |-  ( x e. D <-> ( x e. Word V /\ ( ( # ` x ) = 2 /\ ( x ` 0 ) = P /\ { ( x ` 0 ) , ( x ` 1 ) } e. X ) ) )
20 fveqeq2 
 |-  ( w = y -> ( ( # ` w ) = 2 <-> ( # ` y ) = 2 ) )
21 fveq1 
 |-  ( w = y -> ( w ` 0 ) = ( y ` 0 ) )
22 21 eqeq1d 
 |-  ( w = y -> ( ( w ` 0 ) = P <-> ( y ` 0 ) = P ) )
23 fveq1 
 |-  ( w = y -> ( w ` 1 ) = ( y ` 1 ) )
24 21 23 preq12d 
 |-  ( w = y -> { ( w ` 0 ) , ( w ` 1 ) } = { ( y ` 0 ) , ( y ` 1 ) } )
25 24 eleq1d 
 |-  ( w = y -> ( { ( w ` 0 ) , ( w ` 1 ) } e. X <-> { ( y ` 0 ) , ( y ` 1 ) } e. X ) )
26 20 22 25 3anbi123d 
 |-  ( w = y -> ( ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) <-> ( ( # ` y ) = 2 /\ ( y ` 0 ) = P /\ { ( y ` 0 ) , ( y ` 1 ) } e. X ) ) )
27 26 1 elrab2 
 |-  ( y e. D <-> ( y e. Word V /\ ( ( # ` y ) = 2 /\ ( y ` 0 ) = P /\ { ( y ` 0 ) , ( y ` 1 ) } e. X ) ) )
28 simpr1 
 |-  ( ( x e. Word V /\ ( ( # ` x ) = 2 /\ ( x ` 0 ) = P /\ { ( x ` 0 ) , ( x ` 1 ) } e. X ) ) -> ( # ` x ) = 2 )
29 simpr1 
 |-  ( ( y e. Word V /\ ( ( # ` y ) = 2 /\ ( y ` 0 ) = P /\ { ( y ` 0 ) , ( y ` 1 ) } e. X ) ) -> ( # ` y ) = 2 )
30 29 eqcomd 
 |-  ( ( y e. Word V /\ ( ( # ` y ) = 2 /\ ( y ` 0 ) = P /\ { ( y ` 0 ) , ( y ` 1 ) } e. X ) ) -> 2 = ( # ` y ) )
31 28 30 sylan9eq 
 |-  ( ( ( x e. Word V /\ ( ( # ` x ) = 2 /\ ( x ` 0 ) = P /\ { ( x ` 0 ) , ( x ` 1 ) } e. X ) ) /\ ( y e. Word V /\ ( ( # ` y ) = 2 /\ ( y ` 0 ) = P /\ { ( y ` 0 ) , ( y ` 1 ) } e. X ) ) ) -> ( # ` x ) = ( # ` y ) )
32 31 adantr 
 |-  ( ( ( ( x e. Word V /\ ( ( # ` x ) = 2 /\ ( x ` 0 ) = P /\ { ( x ` 0 ) , ( x ` 1 ) } e. X ) ) /\ ( y e. Word V /\ ( ( # ` y ) = 2 /\ ( y ` 0 ) = P /\ { ( y ` 0 ) , ( y ` 1 ) } e. X ) ) ) /\ ( x ` 1 ) = ( y ` 1 ) ) -> ( # ` x ) = ( # ` y ) )
33 simpr2 
 |-  ( ( x e. Word V /\ ( ( # ` x ) = 2 /\ ( x ` 0 ) = P /\ { ( x ` 0 ) , ( x ` 1 ) } e. X ) ) -> ( x ` 0 ) = P )
34 simpr2 
 |-  ( ( y e. Word V /\ ( ( # ` y ) = 2 /\ ( y ` 0 ) = P /\ { ( y ` 0 ) , ( y ` 1 ) } e. X ) ) -> ( y ` 0 ) = P )
35 34 eqcomd 
 |-  ( ( y e. Word V /\ ( ( # ` y ) = 2 /\ ( y ` 0 ) = P /\ { ( y ` 0 ) , ( y ` 1 ) } e. X ) ) -> P = ( y ` 0 ) )
36 33 35 sylan9eq 
 |-  ( ( ( x e. Word V /\ ( ( # ` x ) = 2 /\ ( x ` 0 ) = P /\ { ( x ` 0 ) , ( x ` 1 ) } e. X ) ) /\ ( y e. Word V /\ ( ( # ` y ) = 2 /\ ( y ` 0 ) = P /\ { ( y ` 0 ) , ( y ` 1 ) } e. X ) ) ) -> ( x ` 0 ) = ( y ` 0 ) )
37 36 adantr 
 |-  ( ( ( ( x e. Word V /\ ( ( # ` x ) = 2 /\ ( x ` 0 ) = P /\ { ( x ` 0 ) , ( x ` 1 ) } e. X ) ) /\ ( y e. Word V /\ ( ( # ` y ) = 2 /\ ( y ` 0 ) = P /\ { ( y ` 0 ) , ( y ` 1 ) } e. X ) ) ) /\ ( x ` 1 ) = ( y ` 1 ) ) -> ( x ` 0 ) = ( y ` 0 ) )
38 simpr 
 |-  ( ( ( ( x e. Word V /\ ( ( # ` x ) = 2 /\ ( x ` 0 ) = P /\ { ( x ` 0 ) , ( x ` 1 ) } e. X ) ) /\ ( y e. Word V /\ ( ( # ` y ) = 2 /\ ( y ` 0 ) = P /\ { ( y ` 0 ) , ( y ` 1 ) } e. X ) ) ) /\ ( x ` 1 ) = ( y ` 1 ) ) -> ( x ` 1 ) = ( y ` 1 ) )
39 oveq2 
 |-  ( ( # ` x ) = 2 -> ( 0 ..^ ( # ` x ) ) = ( 0 ..^ 2 ) )
40 fzo0to2pr 
 |-  ( 0 ..^ 2 ) = { 0 , 1 }
41 39 40 eqtrdi 
 |-  ( ( # ` x ) = 2 -> ( 0 ..^ ( # ` x ) ) = { 0 , 1 } )
42 41 raleqdv 
 |-  ( ( # ` x ) = 2 -> ( A. i e. ( 0 ..^ ( # ` x ) ) ( x ` i ) = ( y ` i ) <-> A. i e. { 0 , 1 } ( x ` i ) = ( y ` i ) ) )
43 c0ex 
 |-  0 e. _V
44 1ex 
 |-  1 e. _V
45 fveq2 
 |-  ( i = 0 -> ( x ` i ) = ( x ` 0 ) )
46 fveq2 
 |-  ( i = 0 -> ( y ` i ) = ( y ` 0 ) )
47 45 46 eqeq12d 
 |-  ( i = 0 -> ( ( x ` i ) = ( y ` i ) <-> ( x ` 0 ) = ( y ` 0 ) ) )
48 fveq2 
 |-  ( i = 1 -> ( x ` i ) = ( x ` 1 ) )
49 fveq2 
 |-  ( i = 1 -> ( y ` i ) = ( y ` 1 ) )
50 48 49 eqeq12d 
 |-  ( i = 1 -> ( ( x ` i ) = ( y ` i ) <-> ( x ` 1 ) = ( y ` 1 ) ) )
51 43 44 47 50 ralpr 
 |-  ( A. i e. { 0 , 1 } ( x ` i ) = ( y ` i ) <-> ( ( x ` 0 ) = ( y ` 0 ) /\ ( x ` 1 ) = ( y ` 1 ) ) )
52 42 51 bitrdi 
 |-  ( ( # ` x ) = 2 -> ( A. i e. ( 0 ..^ ( # ` x ) ) ( x ` i ) = ( y ` i ) <-> ( ( x ` 0 ) = ( y ` 0 ) /\ ( x ` 1 ) = ( y ` 1 ) ) ) )
53 52 3ad2ant1 
 |-  ( ( ( # ` x ) = 2 /\ ( x ` 0 ) = P /\ { ( x ` 0 ) , ( x ` 1 ) } e. X ) -> ( A. i e. ( 0 ..^ ( # ` x ) ) ( x ` i ) = ( y ` i ) <-> ( ( x ` 0 ) = ( y ` 0 ) /\ ( x ` 1 ) = ( y ` 1 ) ) ) )
54 53 ad3antlr 
 |-  ( ( ( ( x e. Word V /\ ( ( # ` x ) = 2 /\ ( x ` 0 ) = P /\ { ( x ` 0 ) , ( x ` 1 ) } e. X ) ) /\ ( y e. Word V /\ ( ( # ` y ) = 2 /\ ( y ` 0 ) = P /\ { ( y ` 0 ) , ( y ` 1 ) } e. X ) ) ) /\ ( x ` 1 ) = ( y ` 1 ) ) -> ( A. i e. ( 0 ..^ ( # ` x ) ) ( x ` i ) = ( y ` i ) <-> ( ( x ` 0 ) = ( y ` 0 ) /\ ( x ` 1 ) = ( y ` 1 ) ) ) )
55 37 38 54 mpbir2and 
 |-  ( ( ( ( x e. Word V /\ ( ( # ` x ) = 2 /\ ( x ` 0 ) = P /\ { ( x ` 0 ) , ( x ` 1 ) } e. X ) ) /\ ( y e. Word V /\ ( ( # ` y ) = 2 /\ ( y ` 0 ) = P /\ { ( y ` 0 ) , ( y ` 1 ) } e. X ) ) ) /\ ( x ` 1 ) = ( y ` 1 ) ) -> A. i e. ( 0 ..^ ( # ` x ) ) ( x ` i ) = ( y ` i ) )
56 eqwrd 
 |-  ( ( x e. Word V /\ y e. Word V ) -> ( x = y <-> ( ( # ` x ) = ( # ` y ) /\ A. i e. ( 0 ..^ ( # ` x ) ) ( x ` i ) = ( y ` i ) ) ) )
57 56 ad2ant2r 
 |-  ( ( ( x e. Word V /\ ( ( # ` x ) = 2 /\ ( x ` 0 ) = P /\ { ( x ` 0 ) , ( x ` 1 ) } e. X ) ) /\ ( y e. Word V /\ ( ( # ` y ) = 2 /\ ( y ` 0 ) = P /\ { ( y ` 0 ) , ( y ` 1 ) } e. X ) ) ) -> ( x = y <-> ( ( # ` x ) = ( # ` y ) /\ A. i e. ( 0 ..^ ( # ` x ) ) ( x ` i ) = ( y ` i ) ) ) )
58 57 adantr 
 |-  ( ( ( ( x e. Word V /\ ( ( # ` x ) = 2 /\ ( x ` 0 ) = P /\ { ( x ` 0 ) , ( x ` 1 ) } e. X ) ) /\ ( y e. Word V /\ ( ( # ` y ) = 2 /\ ( y ` 0 ) = P /\ { ( y ` 0 ) , ( y ` 1 ) } e. X ) ) ) /\ ( x ` 1 ) = ( y ` 1 ) ) -> ( x = y <-> ( ( # ` x ) = ( # ` y ) /\ A. i e. ( 0 ..^ ( # ` x ) ) ( x ` i ) = ( y ` i ) ) ) )
59 32 55 58 mpbir2and 
 |-  ( ( ( ( x e. Word V /\ ( ( # ` x ) = 2 /\ ( x ` 0 ) = P /\ { ( x ` 0 ) , ( x ` 1 ) } e. X ) ) /\ ( y e. Word V /\ ( ( # ` y ) = 2 /\ ( y ` 0 ) = P /\ { ( y ` 0 ) , ( y ` 1 ) } e. X ) ) ) /\ ( x ` 1 ) = ( y ` 1 ) ) -> x = y )
60 59 ex 
 |-  ( ( ( x e. Word V /\ ( ( # ` x ) = 2 /\ ( x ` 0 ) = P /\ { ( x ` 0 ) , ( x ` 1 ) } e. X ) ) /\ ( y e. Word V /\ ( ( # ` y ) = 2 /\ ( y ` 0 ) = P /\ { ( y ` 0 ) , ( y ` 1 ) } e. X ) ) ) -> ( ( x ` 1 ) = ( y ` 1 ) -> x = y ) )
61 19 27 60 syl2anb 
 |-  ( ( x e. D /\ y e. D ) -> ( ( x ` 1 ) = ( y ` 1 ) -> x = y ) )
62 11 61 sylbid 
 |-  ( ( x e. D /\ y e. D ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
63 62 rgen2 
 |-  A. x e. D A. y e. D ( ( F ` x ) = ( F ` y ) -> x = y )
64 dff13 
 |-  ( F : D -1-1-> R <-> ( F : D --> R /\ A. x e. D A. y e. D ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
65 4 63 64 mpbir2an 
 |-  F : D -1-1-> R