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∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈X
wwlktovf1o.r ⊢R=n∈V|Pn∈X
wwlktovf1o.f ⊢F=t∈D⟼t⁡1
Assertion wwlktovfo ⊢P∈V→F:D⟶ontoR

Proof

Step Hyp Ref Expression
1 wwlktovf1o.d ⊢D=w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈X
2 wwlktovf1o.r ⊢R=n∈V|Pn∈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→Pn=Pp
7 6 eleq1d ⊢n=p→Pn∈X↔Pp∈X
8 7 2 elrab2 ⊢p∈R↔p∈V∧Pp∈X
9 simpl ⊢p∈V∧Pp∈X→p∈V
10 9 anim2i ⊢P∈V∧p∈V∧Pp∈X→P∈V∧p∈V
11 eqidd ⊢P∈V∧p∈V∧Pp∈X→0P1p=0P1p
12 wrdlen2i ⊢P∈V∧p∈V→0P1p=0P1p→0P1p∈WordV∧0P1p=2∧0P1p⁡0=P∧0P1p⁡1=p
13 10 11 12 sylc ⊢P∈V∧p∈V∧Pp∈X→0P1p∈WordV∧0P1p=2∧0P1p⁡0=P∧0P1p⁡1=p
14 prex ⊢0P1p∈V
15 14 a1i ⊢P∈V∧p∈V∧Pp∈X→0P1p∈V
16 eleq1 ⊢0P1p=u→0P1p∈WordV↔u∈WordV
17 16 biimpd ⊢0P1p=u→0P1p∈WordV→u∈WordV
18 17 adantr ⊢0P1p=u∧P∈V∧p∈V∧Pp∈X→0P1p∈WordV→u∈WordV
19 18 com12 ⊢0P1p∈WordV→0P1p=u∧P∈V∧p∈V∧Pp∈X→u∈WordV
20 19 adantr ⊢0P1p∈WordV∧0P1p=2→0P1p=u∧P∈V∧p∈V∧Pp∈X→u∈WordV
21 20 adantr ⊢0P1p∈WordV∧0P1p=2∧0P1p⁡0=P∧0P1p⁡1=p→0P1p=u∧P∈V∧p∈V∧Pp∈X→u∈WordV
22 21 impcom ⊢0P1p=u∧P∈V∧p∈V∧Pp∈X∧0P1p∈WordV∧0P1p=2∧0P1p⁡0=P∧0P1p⁡1=p→u∈WordV
23 fveqeq2 ⊢0P1p=u→0P1p=2↔u=2
24 23 biimpd ⊢0P1p=u→0P1p=2→u=2
25 24 adantr ⊢0P1p=u∧P∈V∧p∈V∧Pp∈X→0P1p=2→u=2
26 25 com12 ⊢0P1p=2→0P1p=u∧P∈V∧p∈V∧Pp∈X→u=2
27 26 adantl ⊢0P1p∈WordV∧0P1p=2→0P1p=u∧P∈V∧p∈V∧Pp∈X→u=2
28 27 adantr ⊢0P1p∈WordV∧0P1p=2∧0P1p⁡0=P∧0P1p⁡1=p→0P1p=u∧P∈V∧p∈V∧Pp∈X→u=2
29 28 impcom ⊢0P1p=u∧P∈V∧p∈V∧Pp∈X∧0P1p∈WordV∧0P1p=2∧0P1p⁡0=P∧0P1p⁡1=p→u=2
30 fveq1 ⊢0P1p=u→0P1p⁡0=u⁡0
31 30 eqeq1d ⊢0P1p=u→0P1p⁡0=P↔u⁡0=P
32 31 biimpd ⊢0P1p=u→0P1p⁡0=P→u⁡0=P
33 32 adantr ⊢0P1p=u∧P∈V∧p∈V∧Pp∈X→0P1p⁡0=P→u⁡0=P
34 33 com12 ⊢0P1p⁡0=P→0P1p=u∧P∈V∧p∈V∧Pp∈X→u⁡0=P
35 34 adantr ⊢0P1p⁡0=P∧0P1p⁡1=p→0P1p=u∧P∈V∧p∈V∧Pp∈X→u⁡0=P
36 35 adantl ⊢0P1p∈WordV∧0P1p=2∧0P1p⁡0=P∧0P1p⁡1=p→0P1p=u∧P∈V∧p∈V∧Pp∈X→u⁡0=P
37 36 impcom ⊢0P1p=u∧P∈V∧p∈V∧Pp∈X∧0P1p∈WordV∧0P1p=2∧0P1p⁡0=P∧0P1p⁡1=p→u⁡0=P
38 fveq1 ⊢0P1p=u→0P1p⁡1=u⁡1
39 38 eqeq1d ⊢0P1p=u→0P1p⁡1=p↔u⁡1=p
40 31 39 anbi12d ⊢0P1p=u→0P1p⁡0=P∧0P1p⁡1=p↔u⁡0=P∧u⁡1=p
41 preq12 ⊢u⁡0=P∧u⁡1=p→u⁡0u⁡1=Pp
42 41 eqcomd ⊢u⁡0=P∧u⁡1=p→Pp=u⁡0u⁡1
43 42 eleq1d ⊢u⁡0=P∧u⁡1=p→Pp∈X↔u⁡0u⁡1∈X
44 43 biimpd ⊢u⁡0=P∧u⁡1=p→Pp∈X→u⁡0u⁡1∈X
45 40 44 syl6bi ⊢0P1p=u→0P1p⁡0=P∧0P1p⁡1=p→Pp∈X→u⁡0u⁡1∈X
46 45 com12 ⊢0P1p⁡0=P∧0P1p⁡1=p→0P1p=u→Pp∈X→u⁡0u⁡1∈X
47 46 adantl ⊢0P1p∈WordV∧0P1p=2∧0P1p⁡0=P∧0P1p⁡1=p→0P1p=u→Pp∈X→u⁡0u⁡1∈X
48 47 com13 ⊢Pp∈X→0P1p=u→0P1p∈WordV∧0P1p=2∧0P1p⁡0=P∧0P1p⁡1=p→u⁡0u⁡1∈X
49 48 ad2antll ⊢P∈V∧p∈V∧Pp∈X→0P1p=u→0P1p∈WordV∧0P1p=2∧0P1p⁡0=P∧0P1p⁡1=p→u⁡0u⁡1∈X
50 49 impcom ⊢0P1p=u∧P∈V∧p∈V∧Pp∈X→0P1p∈WordV∧0P1p=2∧0P1p⁡0=P∧0P1p⁡1=p→u⁡0u⁡1∈X
51 50 imp ⊢0P1p=u∧P∈V∧p∈V∧Pp∈X∧0P1p∈WordV∧0P1p=2∧0P1p⁡0=P∧0P1p⁡1=p→u⁡0u⁡1∈X
52 29 37 51 3jca ⊢0P1p=u∧P∈V∧p∈V∧Pp∈X∧0P1p∈WordV∧0P1p=2∧0P1p⁡0=P∧0P1p⁡1=p→u=2∧u⁡0=P∧u⁡0u⁡1∈X
53 eqcom ⊢0P1p⁡1=p↔p=0P1p⁡1
54 38 eqeq2d ⊢0P1p=u→p=0P1p⁡1↔p=u⁡1
55 54 biimpd ⊢0P1p=u→p=0P1p⁡1→p=u⁡1
56 53 55 biimtrid ⊢0P1p=u→0P1p⁡1=p→p=u⁡1
57 56 com12 ⊢0P1p⁡1=p→0P1p=u→p=u⁡1
58 57 ad2antll ⊢0P1p∈WordV∧0P1p=2∧0P1p⁡0=P∧0P1p⁡1=p→0P1p=u→p=u⁡1
59 58 com12 ⊢0P1p=u→0P1p∈WordV∧0P1p=2∧0P1p⁡0=P∧0P1p⁡1=p→p=u⁡1
60 59 adantr ⊢0P1p=u∧P∈V∧p∈V∧Pp∈X→0P1p∈WordV∧0P1p=2∧0P1p⁡0=P∧0P1p⁡1=p→p=u⁡1
61 60 imp ⊢0P1p=u∧P∈V∧p∈V∧Pp∈X∧0P1p∈WordV∧0P1p=2∧0P1p⁡0=P∧0P1p⁡1=p→p=u⁡1
62 22 52 61 jca31 ⊢0P1p=u∧P∈V∧p∈V∧Pp∈X∧0P1p∈WordV∧0P1p=2∧0P1p⁡0=P∧0P1p⁡1=p→u∈WordV∧u=2∧u⁡0=P∧u⁡0u⁡1∈X∧p=u⁡1
63 62 exp31 ⊢0P1p=u→P∈V∧p∈V∧Pp∈X→0P1p∈WordV∧0P1p=2∧0P1p⁡0=P∧0P1p⁡1=p→u∈WordV∧u=2∧u⁡0=P∧u⁡0u⁡1∈X∧p=u⁡1
64 63 eqcoms ⊢u=0P1p→P∈V∧p∈V∧Pp∈X→0P1p∈WordV∧0P1p=2∧0P1p⁡0=P∧0P1p⁡1=p→u∈WordV∧u=2∧u⁡0=P∧u⁡0u⁡1∈X∧p=u⁡1
65 64 impcom ⊢P∈V∧p∈V∧Pp∈X∧u=0P1p→0P1p∈WordV∧0P1p=2∧0P1p⁡0=P∧0P1p⁡1=p→u∈WordV∧u=2∧u⁡0=P∧u⁡0u⁡1∈X∧p=u⁡1
66 15 65 spcimedv ⊢P∈V∧p∈V∧Pp∈X→0P1p∈WordV∧0P1p=2∧0P1p⁡0=P∧0P1p⁡1=p→∃uu∈WordV∧u=2∧u⁡0=P∧u⁡0u⁡1∈X∧p=u⁡1
67 13 66 mpd ⊢P∈V∧p∈V∧Pp∈X→∃uu∈WordV∧u=2∧u⁡0=P∧u⁡0u⁡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⁡0w⁡1=u⁡0u⁡1
73 72 eleq1d ⊢w=u→w⁡0w⁡1∈X↔u⁡0u⁡1∈X
74 68 70 73 3anbi123d ⊢w=u→w=2∧w⁡0=P∧w⁡0w⁡1∈X↔u=2∧u⁡0=P∧u⁡0u⁡1∈X
75 74 elrab ⊢u∈w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈X↔u∈WordV∧u=2∧u⁡0=P∧u⁡0u⁡1∈X
76 75 anbi1i ⊢u∈w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈X∧p=u⁡1↔u∈WordV∧u=2∧u⁡0=P∧u⁡0u⁡1∈X∧p=u⁡1
77 76 exbii ⊢∃uu∈w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈X∧p=u⁡1↔∃uu∈WordV∧u=2∧u⁡0=P∧u⁡0u⁡1∈X∧p=u⁡1
78 67 77 sylibr ⊢P∈V∧p∈V∧Pp∈X→∃uu∈w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈X∧p=u⁡1
79 df-rex ⊢∃u∈w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈Xp=u⁡1↔∃uu∈w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈X∧p=u⁡1
80 78 79 sylibr ⊢P∈V∧p∈V∧Pp∈X→∃u∈w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈Xp=u⁡1
81 1 rexeqi ⊢∃u∈Dp=u⁡1↔∃u∈w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈Xp=u⁡1
82 80 81 sylibr ⊢P∈V∧p∈V∧Pp∈X→∃u∈Dp=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∈Dp=F⁡u↔∃u∈Dp=u⁡1
88 82 87 sylibr ⊢P∈V∧p∈V∧Pp∈X→∃u∈Dp=F⁡u
89 8 88 sylan2b ⊢P∈V∧p∈R→∃u∈Dp=F⁡u
90 89 ralrimiva ⊢P∈V→∀p∈R∃u∈Dp=F⁡u
91 dffo3 ⊢F:D⟶ontoR↔F:D⟶R∧∀p∈R∃u∈Dp=F⁡u
92 5 90 91 sylanbrc ⊢P∈V→F:D⟶ontoR