Metamath Proof Explorer


Theorem wwlktovfo

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

Ref Expression
Hypotheses wwlktovf1o.d D = w Word V | w = 2 w 0 = P w 0 w 1 X
wwlktovf1o.r R = n V | P n X
wwlktovf1o.f F = t D t 1
Assertion wwlktovfo P V F : D onto R

Proof

Step Hyp Ref Expression
1 wwlktovf1o.d D = w Word V | w = 2 w 0 = P w 0 w 1 X
2 wwlktovf1o.r R = n V | P n X
3 wwlktovf1o.f F = t D t 1
4 1 2 3 wwlktovf F : D R
5 4 a1i P V F : D R
6 preq2 n = p P n = P p
7 6 eleq1d n = p P n X P p X
8 7 2 elrab2 p R p V P p X
9 simpl p V P p X p V
10 9 anim2i P V p V P p X P V p V
11 eqidd P V p V P p X 0 P 1 p = 0 P 1 p
12 wrdlen2i P V p V 0 P 1 p = 0 P 1 p 0 P 1 p Word V 0 P 1 p = 2 0 P 1 p 0 = P 0 P 1 p 1 = p
13 10 11 12 sylc P V p V P p X 0 P 1 p Word V 0 P 1 p = 2 0 P 1 p 0 = P 0 P 1 p 1 = p
14 prex 0 P 1 p V
15 14 a1i P V p V P p X 0 P 1 p V
16 eleq1 0 P 1 p = u 0 P 1 p Word V u Word V
17 16 biimpd 0 P 1 p = u 0 P 1 p Word V u Word V
18 17 adantr 0 P 1 p = u P V p V P p X 0 P 1 p Word V u Word V
19 18 com12 0 P 1 p Word V 0 P 1 p = u P V p V P p X u Word V
20 19 adantr 0 P 1 p Word V 0 P 1 p = 2 0 P 1 p = u P V p V P p X u Word V
21 20 adantr 0 P 1 p Word V 0 P 1 p = 2 0 P 1 p 0 = P 0 P 1 p 1 = p 0 P 1 p = u P V p V P p X u Word V
22 21 impcom 0 P 1 p = u P V p V P p X 0 P 1 p Word V 0 P 1 p = 2 0 P 1 p 0 = P 0 P 1 p 1 = p u Word V
23 fveqeq2 0 P 1 p = u 0 P 1 p = 2 u = 2
24 23 biimpd 0 P 1 p = u 0 P 1 p = 2 u = 2
25 24 adantr 0 P 1 p = u P V p V P p X 0 P 1 p = 2 u = 2
26 25 com12 0 P 1 p = 2 0 P 1 p = u P V p V P p X u = 2
27 26 adantl 0 P 1 p Word V 0 P 1 p = 2 0 P 1 p = u P V p V P p X u = 2
28 27 adantr 0 P 1 p Word V 0 P 1 p = 2 0 P 1 p 0 = P 0 P 1 p 1 = p 0 P 1 p = u P V p V P p X u = 2
29 28 impcom 0 P 1 p = u P V p V P p X 0 P 1 p Word V 0 P 1 p = 2 0 P 1 p 0 = P 0 P 1 p 1 = p u = 2
30 fveq1 0 P 1 p = u 0 P 1 p 0 = u 0
31 30 eqeq1d 0 P 1 p = u 0 P 1 p 0 = P u 0 = P
32 31 biimpd 0 P 1 p = u 0 P 1 p 0 = P u 0 = P
33 32 adantr 0 P 1 p = u P V p V P p X 0 P 1 p 0 = P u 0 = P
34 33 com12 0 P 1 p 0 = P 0 P 1 p = u P V p V P p X u 0 = P
35 34 adantr 0 P 1 p 0 = P 0 P 1 p 1 = p 0 P 1 p = u P V p V P p X u 0 = P
36 35 adantl 0 P 1 p Word V 0 P 1 p = 2 0 P 1 p 0 = P 0 P 1 p 1 = p 0 P 1 p = u P V p V P p X u 0 = P
37 36 impcom 0 P 1 p = u P V p V P p X 0 P 1 p Word V 0 P 1 p = 2 0 P 1 p 0 = P 0 P 1 p 1 = p u 0 = P
38 fveq1 0 P 1 p = u 0 P 1 p 1 = u 1
39 38 eqeq1d 0 P 1 p = u 0 P 1 p 1 = p u 1 = p
40 31 39 anbi12d 0 P 1 p = u 0 P 1 p 0 = P 0 P 1 p 1 = p u 0 = P u 1 = p
41 preq12 u 0 = P u 1 = p u 0 u 1 = P p
42 41 eqcomd u 0 = P u 1 = p P p = u 0 u 1
43 42 eleq1d u 0 = P u 1 = p P p X u 0 u 1 X
44 43 biimpd u 0 = P u 1 = p P p X u 0 u 1 X
45 40 44 syl6bi 0 P 1 p = u 0 P 1 p 0 = P 0 P 1 p 1 = p P p X u 0 u 1 X
46 45 com12 0 P 1 p 0 = P 0 P 1 p 1 = p 0 P 1 p = u P p X u 0 u 1 X
47 46 adantl 0 P 1 p Word V 0 P 1 p = 2 0 P 1 p 0 = P 0 P 1 p 1 = p 0 P 1 p = u P p X u 0 u 1 X
48 47 com13 P p X 0 P 1 p = u 0 P 1 p Word V 0 P 1 p = 2 0 P 1 p 0 = P 0 P 1 p 1 = p u 0 u 1 X
49 48 ad2antll P V p V P p X 0 P 1 p = u 0 P 1 p Word V 0 P 1 p = 2 0 P 1 p 0 = P 0 P 1 p 1 = p u 0 u 1 X
50 49 impcom 0 P 1 p = u P V p V P p X 0 P 1 p Word V 0 P 1 p = 2 0 P 1 p 0 = P 0 P 1 p 1 = p u 0 u 1 X
51 50 imp 0 P 1 p = u P V p V P p X 0 P 1 p Word V 0 P 1 p = 2 0 P 1 p 0 = P 0 P 1 p 1 = p u 0 u 1 X
52 29 37 51 3jca 0 P 1 p = u P V p V P p X 0 P 1 p Word V 0 P 1 p = 2 0 P 1 p 0 = P 0 P 1 p 1 = p u = 2 u 0 = P u 0 u 1 X
53 eqcom 0 P 1 p 1 = p p = 0 P 1 p 1
54 38 eqeq2d 0 P 1 p = u p = 0 P 1 p 1 p = u 1
55 54 biimpd 0 P 1 p = u p = 0 P 1 p 1 p = u 1
56 53 55 syl5bi 0 P 1 p = u 0 P 1 p 1 = p p = u 1
57 56 com12 0 P 1 p 1 = p 0 P 1 p = u p = u 1
58 57 ad2antll 0 P 1 p Word V 0 P 1 p = 2 0 P 1 p 0 = P 0 P 1 p 1 = p 0 P 1 p = u p = u 1
59 58 com12 0 P 1 p = u 0 P 1 p Word V 0 P 1 p = 2 0 P 1 p 0 = P 0 P 1 p 1 = p p = u 1
60 59 adantr 0 P 1 p = u P V p V P p X 0 P 1 p Word V 0 P 1 p = 2 0 P 1 p 0 = P 0 P 1 p 1 = p p = u 1
61 60 imp 0 P 1 p = u P V p V P p X 0 P 1 p Word V 0 P 1 p = 2 0 P 1 p 0 = P 0 P 1 p 1 = p p = u 1
62 22 52 61 jca31 0 P 1 p = u P V p V P p X 0 P 1 p Word V 0 P 1 p = 2 0 P 1 p 0 = P 0 P 1 p 1 = p u Word V u = 2 u 0 = P u 0 u 1 X p = u 1
63 62 exp31 0 P 1 p = u P V p V P p X 0 P 1 p Word V 0 P 1 p = 2 0 P 1 p 0 = P 0 P 1 p 1 = p u Word V u = 2 u 0 = P u 0 u 1 X p = u 1
64 63 eqcoms u = 0 P 1 p P V p V P p X 0 P 1 p Word V 0 P 1 p = 2 0 P 1 p 0 = P 0 P 1 p 1 = p u Word V u = 2 u 0 = P u 0 u 1 X p = u 1
65 64 impcom P V p V P p X u = 0 P 1 p 0 P 1 p Word V 0 P 1 p = 2 0 P 1 p 0 = P 0 P 1 p 1 = p u Word V u = 2 u 0 = P u 0 u 1 X p = u 1
66 15 65 spcimedv P V p V P p X 0 P 1 p Word V 0 P 1 p = 2 0 P 1 p 0 = P 0 P 1 p 1 = p u u Word V u = 2 u 0 = P u 0 u 1 X p = u 1
67 13 66 mpd P V p V P p X u u Word V u = 2 u 0 = P u 0 u 1 X p = u 1
68 fveqeq2 w = u w = 2 u = 2
69 fveq1 w = u w 0 = u 0
70 69 eqeq1d w = u w 0 = P u 0 = P
71 fveq1 w = u w 1 = u 1
72 69 71 preq12d w = u w 0 w 1 = u 0 u 1
73 72 eleq1d w = u w 0 w 1 X u 0 u 1 X
74 68 70 73 3anbi123d w = u w = 2 w 0 = P w 0 w 1 X u = 2 u 0 = P u 0 u 1 X
75 74 elrab u w Word V | w = 2 w 0 = P w 0 w 1 X u Word V u = 2 u 0 = P u 0 u 1 X
76 75 anbi1i u w Word V | w = 2 w 0 = P w 0 w 1 X p = u 1 u Word V u = 2 u 0 = P u 0 u 1 X p = u 1
77 76 exbii u u w Word V | w = 2 w 0 = P w 0 w 1 X p = u 1 u u Word V u = 2 u 0 = P u 0 u 1 X p = u 1
78 67 77 sylibr P V p V P p X u u w Word V | w = 2 w 0 = P w 0 w 1 X p = u 1
79 df-rex u w Word V | w = 2 w 0 = P w 0 w 1 X p = u 1 u u w Word V | w = 2 w 0 = P w 0 w 1 X p = u 1
80 78 79 sylibr P V p V P p X u w Word V | w = 2 w 0 = P w 0 w 1 X p = u 1
81 1 rexeqi u D p = u 1 u w Word V | w = 2 w 0 = P w 0 w 1 X p = u 1
82 80 81 sylibr P V p V P p X u D p = u 1
83 fveq1 t = u t 1 = u 1
84 fvex u 1 V
85 83 3 84 fvmpt u D F u = u 1
86 85 eqeq2d u D p = F u p = u 1
87 86 rexbiia u D p = F u u D p = u 1
88 82 87 sylibr P V p V P p X u D p = F u
89 8 88 sylan2b P V p R u D p = F u
90 89 ralrimiva P V p R u D p = F u
91 dffo3 F : D onto R F : D R p R u D p = F u
92 5 90 91 sylanbrc P V F : D onto R