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 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 wwlktovfo 
|- ( P e. V -> F : D -onto-> 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 4 a1i 
 |-  ( P e. V -> F : D --> R )
6 preq2 
 |-  ( n = p -> { P , n } = { P , p } )
7 6 eleq1d 
 |-  ( n = p -> ( { P , n } e. X <-> { P , p } e. X ) )
8 7 2 elrab2 
 |-  ( p e. R <-> ( p e. V /\ { P , p } e. X ) )
9 simpl 
 |-  ( ( p e. V /\ { P , p } e. X ) -> p e. V )
10 9 anim2i 
 |-  ( ( P e. V /\ ( p e. V /\ { P , p } e. X ) ) -> ( P e. V /\ p e. V ) )
11 eqidd 
 |-  ( ( P e. V /\ ( p e. V /\ { P , p } e. X ) ) -> { <. 0 , P >. , <. 1 , p >. } = { <. 0 , P >. , <. 1 , p >. } )
12 wrdlen2i 
 |-  ( ( P e. V /\ p e. V ) -> ( { <. 0 , P >. , <. 1 , p >. } = { <. 0 , P >. , <. 1 , p >. } -> ( ( { <. 0 , P >. , <. 1 , p >. } e. 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 e. V /\ ( p e. V /\ { P , p } e. X ) ) -> ( ( { <. 0 , P >. , <. 1 , p >. } e. 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 >. } e. _V
15 14 a1i 
 |-  ( ( P e. V /\ ( p e. V /\ { P , p } e. X ) ) -> { <. 0 , P >. , <. 1 , p >. } e. _V )
16 eleq1 
 |-  ( { <. 0 , P >. , <. 1 , p >. } = u -> ( { <. 0 , P >. , <. 1 , p >. } e. Word V <-> u e. Word V ) )
17 16 biimpd 
 |-  ( { <. 0 , P >. , <. 1 , p >. } = u -> ( { <. 0 , P >. , <. 1 , p >. } e. Word V -> u e. Word V ) )
18 17 adantr 
 |-  ( ( { <. 0 , P >. , <. 1 , p >. } = u /\ ( P e. V /\ ( p e. V /\ { P , p } e. X ) ) ) -> ( { <. 0 , P >. , <. 1 , p >. } e. Word V -> u e. Word V ) )
19 18 com12 
 |-  ( { <. 0 , P >. , <. 1 , p >. } e. Word V -> ( ( { <. 0 , P >. , <. 1 , p >. } = u /\ ( P e. V /\ ( p e. V /\ { P , p } e. X ) ) ) -> u e. Word V ) )
20 19 adantr 
 |-  ( ( { <. 0 , P >. , <. 1 , p >. } e. Word V /\ ( # ` { <. 0 , P >. , <. 1 , p >. } ) = 2 ) -> ( ( { <. 0 , P >. , <. 1 , p >. } = u /\ ( P e. V /\ ( p e. V /\ { P , p } e. X ) ) ) -> u e. Word V ) )
21 20 adantr 
 |-  ( ( ( { <. 0 , P >. , <. 1 , p >. } e. 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 e. V /\ ( p e. V /\ { P , p } e. X ) ) ) -> u e. Word V ) )
22 21 impcom 
 |-  ( ( ( { <. 0 , P >. , <. 1 , p >. } = u /\ ( P e. V /\ ( p e. V /\ { P , p } e. X ) ) ) /\ ( ( { <. 0 , P >. , <. 1 , p >. } e. Word V /\ ( # ` { <. 0 , P >. , <. 1 , p >. } ) = 2 ) /\ ( ( { <. 0 , P >. , <. 1 , p >. } ` 0 ) = P /\ ( { <. 0 , P >. , <. 1 , p >. } ` 1 ) = p ) ) ) -> u e. 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 e. V /\ ( p e. V /\ { P , p } e. X ) ) ) -> ( ( # ` { <. 0 , P >. , <. 1 , p >. } ) = 2 -> ( # ` u ) = 2 ) )
26 25 com12 
 |-  ( ( # ` { <. 0 , P >. , <. 1 , p >. } ) = 2 -> ( ( { <. 0 , P >. , <. 1 , p >. } = u /\ ( P e. V /\ ( p e. V /\ { P , p } e. X ) ) ) -> ( # ` u ) = 2 ) )
27 26 adantl 
 |-  ( ( { <. 0 , P >. , <. 1 , p >. } e. Word V /\ ( # ` { <. 0 , P >. , <. 1 , p >. } ) = 2 ) -> ( ( { <. 0 , P >. , <. 1 , p >. } = u /\ ( P e. V /\ ( p e. V /\ { P , p } e. X ) ) ) -> ( # ` u ) = 2 ) )
28 27 adantr 
 |-  ( ( ( { <. 0 , P >. , <. 1 , p >. } e. 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 e. V /\ ( p e. V /\ { P , p } e. X ) ) ) -> ( # ` u ) = 2 ) )
29 28 impcom 
 |-  ( ( ( { <. 0 , P >. , <. 1 , p >. } = u /\ ( P e. V /\ ( p e. V /\ { P , p } e. X ) ) ) /\ ( ( { <. 0 , P >. , <. 1 , p >. } e. 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 e. V /\ ( p e. V /\ { P , p } e. 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 e. V /\ ( p e. V /\ { P , p } e. 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 e. V /\ ( p e. V /\ { P , p } e. X ) ) ) -> ( u ` 0 ) = P ) )
36 35 adantl 
 |-  ( ( ( { <. 0 , P >. , <. 1 , p >. } e. 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 e. V /\ ( p e. V /\ { P , p } e. X ) ) ) -> ( u ` 0 ) = P ) )
37 36 impcom 
 |-  ( ( ( { <. 0 , P >. , <. 1 , p >. } = u /\ ( P e. V /\ ( p e. V /\ { P , p } e. X ) ) ) /\ ( ( { <. 0 , P >. , <. 1 , p >. } e. 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 } e. X <-> { ( u ` 0 ) , ( u ` 1 ) } e. X ) )
44 43 biimpd 
 |-  ( ( ( u ` 0 ) = P /\ ( u ` 1 ) = p ) -> ( { P , p } e. X -> { ( u ` 0 ) , ( u ` 1 ) } e. X ) )
45 40 44 biimtrdi 
 |-  ( { <. 0 , P >. , <. 1 , p >. } = u -> ( ( ( { <. 0 , P >. , <. 1 , p >. } ` 0 ) = P /\ ( { <. 0 , P >. , <. 1 , p >. } ` 1 ) = p ) -> ( { P , p } e. X -> { ( u ` 0 ) , ( u ` 1 ) } e. X ) ) )
46 45 com12 
 |-  ( ( ( { <. 0 , P >. , <. 1 , p >. } ` 0 ) = P /\ ( { <. 0 , P >. , <. 1 , p >. } ` 1 ) = p ) -> ( { <. 0 , P >. , <. 1 , p >. } = u -> ( { P , p } e. X -> { ( u ` 0 ) , ( u ` 1 ) } e. X ) ) )
47 46 adantl 
 |-  ( ( ( { <. 0 , P >. , <. 1 , p >. } e. 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 } e. X -> { ( u ` 0 ) , ( u ` 1 ) } e. X ) ) )
48 47 com13 
 |-  ( { P , p } e. X -> ( { <. 0 , P >. , <. 1 , p >. } = u -> ( ( ( { <. 0 , P >. , <. 1 , p >. } e. Word V /\ ( # ` { <. 0 , P >. , <. 1 , p >. } ) = 2 ) /\ ( ( { <. 0 , P >. , <. 1 , p >. } ` 0 ) = P /\ ( { <. 0 , P >. , <. 1 , p >. } ` 1 ) = p ) ) -> { ( u ` 0 ) , ( u ` 1 ) } e. X ) ) )
49 48 ad2antll 
 |-  ( ( P e. V /\ ( p e. V /\ { P , p } e. X ) ) -> ( { <. 0 , P >. , <. 1 , p >. } = u -> ( ( ( { <. 0 , P >. , <. 1 , p >. } e. Word V /\ ( # ` { <. 0 , P >. , <. 1 , p >. } ) = 2 ) /\ ( ( { <. 0 , P >. , <. 1 , p >. } ` 0 ) = P /\ ( { <. 0 , P >. , <. 1 , p >. } ` 1 ) = p ) ) -> { ( u ` 0 ) , ( u ` 1 ) } e. X ) ) )
50 49 impcom 
 |-  ( ( { <. 0 , P >. , <. 1 , p >. } = u /\ ( P e. V /\ ( p e. V /\ { P , p } e. X ) ) ) -> ( ( ( { <. 0 , P >. , <. 1 , p >. } e. Word V /\ ( # ` { <. 0 , P >. , <. 1 , p >. } ) = 2 ) /\ ( ( { <. 0 , P >. , <. 1 , p >. } ` 0 ) = P /\ ( { <. 0 , P >. , <. 1 , p >. } ` 1 ) = p ) ) -> { ( u ` 0 ) , ( u ` 1 ) } e. X ) )
51 50 imp 
 |-  ( ( ( { <. 0 , P >. , <. 1 , p >. } = u /\ ( P e. V /\ ( p e. V /\ { P , p } e. X ) ) ) /\ ( ( { <. 0 , P >. , <. 1 , p >. } e. Word V /\ ( # ` { <. 0 , P >. , <. 1 , p >. } ) = 2 ) /\ ( ( { <. 0 , P >. , <. 1 , p >. } ` 0 ) = P /\ ( { <. 0 , P >. , <. 1 , p >. } ` 1 ) = p ) ) ) -> { ( u ` 0 ) , ( u ` 1 ) } e. X )
52 29 37 51 3jca 
 |-  ( ( ( { <. 0 , P >. , <. 1 , p >. } = u /\ ( P e. V /\ ( p e. V /\ { P , p } e. X ) ) ) /\ ( ( { <. 0 , P >. , <. 1 , p >. } e. 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 ) } e. 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 biimtrid 
 |-  ( { <. 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 >. } e. 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 >. } e. 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 e. V /\ ( p e. V /\ { P , p } e. X ) ) ) -> ( ( ( { <. 0 , P >. , <. 1 , p >. } e. 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 e. V /\ ( p e. V /\ { P , p } e. X ) ) ) /\ ( ( { <. 0 , P >. , <. 1 , p >. } e. 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 e. V /\ ( p e. V /\ { P , p } e. X ) ) ) /\ ( ( { <. 0 , P >. , <. 1 , p >. } e. Word V /\ ( # ` { <. 0 , P >. , <. 1 , p >. } ) = 2 ) /\ ( ( { <. 0 , P >. , <. 1 , p >. } ` 0 ) = P /\ ( { <. 0 , P >. , <. 1 , p >. } ` 1 ) = p ) ) ) -> ( ( u e. Word V /\ ( ( # ` u ) = 2 /\ ( u ` 0 ) = P /\ { ( u ` 0 ) , ( u ` 1 ) } e. X ) ) /\ p = ( u ` 1 ) ) )
63 62 exp31 
 |-  ( { <. 0 , P >. , <. 1 , p >. } = u -> ( ( P e. V /\ ( p e. V /\ { P , p } e. X ) ) -> ( ( ( { <. 0 , P >. , <. 1 , p >. } e. Word V /\ ( # ` { <. 0 , P >. , <. 1 , p >. } ) = 2 ) /\ ( ( { <. 0 , P >. , <. 1 , p >. } ` 0 ) = P /\ ( { <. 0 , P >. , <. 1 , p >. } ` 1 ) = p ) ) -> ( ( u e. Word V /\ ( ( # ` u ) = 2 /\ ( u ` 0 ) = P /\ { ( u ` 0 ) , ( u ` 1 ) } e. X ) ) /\ p = ( u ` 1 ) ) ) ) )
64 63 eqcoms 
 |-  ( u = { <. 0 , P >. , <. 1 , p >. } -> ( ( P e. V /\ ( p e. V /\ { P , p } e. X ) ) -> ( ( ( { <. 0 , P >. , <. 1 , p >. } e. Word V /\ ( # ` { <. 0 , P >. , <. 1 , p >. } ) = 2 ) /\ ( ( { <. 0 , P >. , <. 1 , p >. } ` 0 ) = P /\ ( { <. 0 , P >. , <. 1 , p >. } ` 1 ) = p ) ) -> ( ( u e. Word V /\ ( ( # ` u ) = 2 /\ ( u ` 0 ) = P /\ { ( u ` 0 ) , ( u ` 1 ) } e. X ) ) /\ p = ( u ` 1 ) ) ) ) )
65 64 impcom 
 |-  ( ( ( P e. V /\ ( p e. V /\ { P , p } e. X ) ) /\ u = { <. 0 , P >. , <. 1 , p >. } ) -> ( ( ( { <. 0 , P >. , <. 1 , p >. } e. Word V /\ ( # ` { <. 0 , P >. , <. 1 , p >. } ) = 2 ) /\ ( ( { <. 0 , P >. , <. 1 , p >. } ` 0 ) = P /\ ( { <. 0 , P >. , <. 1 , p >. } ` 1 ) = p ) ) -> ( ( u e. Word V /\ ( ( # ` u ) = 2 /\ ( u ` 0 ) = P /\ { ( u ` 0 ) , ( u ` 1 ) } e. X ) ) /\ p = ( u ` 1 ) ) ) )
66 15 65 spcimedv 
 |-  ( ( P e. V /\ ( p e. V /\ { P , p } e. X ) ) -> ( ( ( { <. 0 , P >. , <. 1 , p >. } e. Word V /\ ( # ` { <. 0 , P >. , <. 1 , p >. } ) = 2 ) /\ ( ( { <. 0 , P >. , <. 1 , p >. } ` 0 ) = P /\ ( { <. 0 , P >. , <. 1 , p >. } ` 1 ) = p ) ) -> E. u ( ( u e. Word V /\ ( ( # ` u ) = 2 /\ ( u ` 0 ) = P /\ { ( u ` 0 ) , ( u ` 1 ) } e. X ) ) /\ p = ( u ` 1 ) ) ) )
67 13 66 mpd 
 |-  ( ( P e. V /\ ( p e. V /\ { P , p } e. X ) ) -> E. u ( ( u e. Word V /\ ( ( # ` u ) = 2 /\ ( u ` 0 ) = P /\ { ( u ` 0 ) , ( u ` 1 ) } e. 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 ) } e. X <-> { ( u ` 0 ) , ( u ` 1 ) } e. X ) )
74 68 70 73 3anbi123d 
 |-  ( w = u -> ( ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) <-> ( ( # ` u ) = 2 /\ ( u ` 0 ) = P /\ { ( u ` 0 ) , ( u ` 1 ) } e. X ) ) )
75 74 elrab 
 |-  ( u e. { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) } <-> ( u e. Word V /\ ( ( # ` u ) = 2 /\ ( u ` 0 ) = P /\ { ( u ` 0 ) , ( u ` 1 ) } e. X ) ) )
76 75 anbi1i 
 |-  ( ( u e. { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) } /\ p = ( u ` 1 ) ) <-> ( ( u e. Word V /\ ( ( # ` u ) = 2 /\ ( u ` 0 ) = P /\ { ( u ` 0 ) , ( u ` 1 ) } e. X ) ) /\ p = ( u ` 1 ) ) )
77 76 exbii 
 |-  ( E. u ( u e. { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) } /\ p = ( u ` 1 ) ) <-> E. u ( ( u e. Word V /\ ( ( # ` u ) = 2 /\ ( u ` 0 ) = P /\ { ( u ` 0 ) , ( u ` 1 ) } e. X ) ) /\ p = ( u ` 1 ) ) )
78 67 77 sylibr 
 |-  ( ( P e. V /\ ( p e. V /\ { P , p } e. X ) ) -> E. u ( u e. { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) } /\ p = ( u ` 1 ) ) )
79 df-rex 
 |-  ( E. u e. { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) } p = ( u ` 1 ) <-> E. u ( u e. { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) } /\ p = ( u ` 1 ) ) )
80 78 79 sylibr 
 |-  ( ( P e. V /\ ( p e. V /\ { P , p } e. X ) ) -> E. u e. { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) } p = ( u ` 1 ) )
81 1 rexeqi 
 |-  ( E. u e. D p = ( u ` 1 ) <-> E. u e. { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) } p = ( u ` 1 ) )
82 80 81 sylibr 
 |-  ( ( P e. V /\ ( p e. V /\ { P , p } e. X ) ) -> E. u e. D p = ( u ` 1 ) )
83 fveq1 
 |-  ( t = u -> ( t ` 1 ) = ( u ` 1 ) )
84 fvex 
 |-  ( u ` 1 ) e. _V
85 83 3 84 fvmpt 
 |-  ( u e. D -> ( F ` u ) = ( u ` 1 ) )
86 85 eqeq2d 
 |-  ( u e. D -> ( p = ( F ` u ) <-> p = ( u ` 1 ) ) )
87 86 rexbiia 
 |-  ( E. u e. D p = ( F ` u ) <-> E. u e. D p = ( u ` 1 ) )
88 82 87 sylibr 
 |-  ( ( P e. V /\ ( p e. V /\ { P , p } e. X ) ) -> E. u e. D p = ( F ` u ) )
89 8 88 sylan2b 
 |-  ( ( P e. V /\ p e. R ) -> E. u e. D p = ( F ` u ) )
90 89 ralrimiva 
 |-  ( P e. V -> A. p e. R E. u e. D p = ( F ` u ) )
91 dffo3 
 |-  ( F : D -onto-> R <-> ( F : D --> R /\ A. p e. R E. u e. D p = ( F ` u ) ) )
92 5 90 91 sylanbrc 
 |-  ( P e. V -> F : D -onto-> R )