Metamath Proof Explorer

Theorem efgsfo

Description: For any word, there is a sequence of extensions starting at a reduced word and ending at the target word, such that each word in the chain is an extension of the previous (inserting an element and its inverse at adjacent indices somewhere in the sequence). (Contributed by Mario Carneiro, 27-Sep-2015)

Ref Expression
Hypotheses efgval.w 
|- W = ( _I ` Word ( I X. 2o ) )
efgval.r 
|- .~ = ( ~FG ` I )
efgval2.m 
|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
efgval2.t 
|- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
efgred.d 
|- D = ( W \ U_ x e. W ran ( T ` x ) )
efgred.s 
|- S = ( m e. { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )
Assertion efgsfo 
|- S : dom S -onto-> W

Proof

Step Hyp Ref Expression
1 efgval.w 
 |-  W = ( _I ` Word ( I X. 2o ) )
2 efgval.r 
 |-  .~ = ( ~FG ` I )
3 efgval2.m 
 |-  M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
4 efgval2.t 
 |-  T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
5 efgred.d 
 |-  D = ( W \ U_ x e. W ran ( T ` x ) )
6 efgred.s 
 |-  S = ( m e. { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )
7 1 2 3 4 5 6 efgsf 
 |-  S : { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } --> W
8 7 fdmi 
 |-  dom S = { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) }
9 8 feq2i 
 |-  ( S : dom S --> W <-> S : { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } --> W )
10 7 9 mpbir 
 |-  S : dom S --> W
11 frn 
 |-  ( S : dom S --> W -> ran S C_ W )
12 10 11 ax-mp 
 |-  ran S C_ W
13 fviss 
 |-  ( _I ` Word ( I X. 2o ) ) C_ Word ( I X. 2o )
14 1 13 eqsstri 
 |-  W C_ Word ( I X. 2o )
15 14 sseli 
 |-  ( c e. W -> c e. Word ( I X. 2o ) )
16 lencl 
 |-  ( c e. Word ( I X. 2o ) -> ( # ` c ) e. NN0 )
17 15 16 syl 
 |-  ( c e. W -> ( # ` c ) e. NN0 )
18 peano2nn0 
 |-  ( ( # ` c ) e. NN0 -> ( ( # ` c ) + 1 ) e. NN0 )
19 14 sseli 
 |-  ( a e. W -> a e. Word ( I X. 2o ) )
20 lencl 
 |-  ( a e. Word ( I X. 2o ) -> ( # ` a ) e. NN0 )
21 19 20 syl 
 |-  ( a e. W -> ( # ` a ) e. NN0 )
22 nn0nlt0 
 |-  ( ( # ` a ) e. NN0 -> -. ( # ` a ) < 0 )
23 breq2 
 |-  ( b = 0 -> ( ( # ` a ) < b <-> ( # ` a ) < 0 ) )
24 23 notbid 
 |-  ( b = 0 -> ( -. ( # ` a ) < b <-> -. ( # ` a ) < 0 ) )
25 22 24 syl5ibr 
 |-  ( b = 0 -> ( ( # ` a ) e. NN0 -> -. ( # ` a ) < b ) )
26 21 25 syl5 
 |-  ( b = 0 -> ( a e. W -> -. ( # ` a ) < b ) )
27 26 ralrimiv 
 |-  ( b = 0 -> A. a e. W -. ( # ` a ) < b )
28 rabeq0 
 |-  ( { a e. W | ( # ` a ) < b } = (/) <-> A. a e. W -. ( # ` a ) < b )
29 27 28 sylibr 
 |-  ( b = 0 -> { a e. W | ( # ` a ) < b } = (/) )
30 29 sseq1d 
 |-  ( b = 0 -> ( { a e. W | ( # ` a ) < b } C_ ran S <-> (/) C_ ran S ) )
31 breq2 
 |-  ( b = d -> ( ( # ` a ) < b <-> ( # ` a ) < d ) )
32 31 rabbidv 
 |-  ( b = d -> { a e. W | ( # ` a ) < b } = { a e. W | ( # ` a ) < d } )
33 32 sseq1d 
 |-  ( b = d -> ( { a e. W | ( # ` a ) < b } C_ ran S <-> { a e. W | ( # ` a ) < d } C_ ran S ) )
34 breq2 
 |-  ( b = ( d + 1 ) -> ( ( # ` a ) < b <-> ( # ` a ) < ( d + 1 ) ) )
35 34 rabbidv 
 |-  ( b = ( d + 1 ) -> { a e. W | ( # ` a ) < b } = { a e. W | ( # ` a ) < ( d + 1 ) } )
36 35 sseq1d 
 |-  ( b = ( d + 1 ) -> ( { a e. W | ( # ` a ) < b } C_ ran S <-> { a e. W | ( # ` a ) < ( d + 1 ) } C_ ran S ) )
37 breq2 
 |-  ( b = ( ( # ` c ) + 1 ) -> ( ( # ` a ) < b <-> ( # ` a ) < ( ( # ` c ) + 1 ) ) )
38 37 rabbidv 
 |-  ( b = ( ( # ` c ) + 1 ) -> { a e. W | ( # ` a ) < b } = { a e. W | ( # ` a ) < ( ( # ` c ) + 1 ) } )
39 38 sseq1d 
 |-  ( b = ( ( # ` c ) + 1 ) -> ( { a e. W | ( # ` a ) < b } C_ ran S <-> { a e. W | ( # ` a ) < ( ( # ` c ) + 1 ) } C_ ran S ) )
40 0ss 
 |-  (/) C_ ran S
41 simpr 
 |-  ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) -> { a e. W | ( # ` a ) < d } C_ ran S )
42 fveqeq2 
 |-  ( a = c -> ( ( # ` a ) = d <-> ( # ` c ) = d ) )
43 42 cbvrabv 
 |-  { a e. W | ( # ` a ) = d } = { c e. W | ( # ` c ) = d }
44 eliun 
 |-  ( c e. U_ x e. W ran ( T ` x ) <-> E. x e. W c e. ran ( T ` x ) )
45 fveq2 
 |-  ( x = b -> ( T ` x ) = ( T ` b ) )
46 45 rneqd 
 |-  ( x = b -> ran ( T ` x ) = ran ( T ` b ) )
47 46 eleq2d 
 |-  ( x = b -> ( c e. ran ( T ` x ) <-> c e. ran ( T ` b ) ) )
48 47 cbvrexvw 
 |-  ( E. x e. W c e. ran ( T ` x ) <-> E. b e. W c e. ran ( T ` b ) )
49 44 48 bitri 
 |-  ( c e. U_ x e. W ran ( T ` x ) <-> E. b e. W c e. ran ( T ` b ) )
50 simpl1r 
 |-  ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( b e. W /\ c e. ran ( T ` b ) ) ) -> { a e. W | ( # ` a ) < d } C_ ran S )
51 fveq2 
 |-  ( a = b -> ( # ` a ) = ( # ` b ) )
52 51 breq1d 
 |-  ( a = b -> ( ( # ` a ) < d <-> ( # ` b ) < d ) )
53 simprl 
 |-  ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( b e. W /\ c e. ran ( T ` b ) ) ) -> b e. W )
54 14 53 sseldi 
 |-  ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( b e. W /\ c e. ran ( T ` b ) ) ) -> b e. Word ( I X. 2o ) )
55 lencl 
 |-  ( b e. Word ( I X. 2o ) -> ( # ` b ) e. NN0 )
56 54 55 syl 
 |-  ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( b e. W /\ c e. ran ( T ` b ) ) ) -> ( # ` b ) e. NN0 )
57 56 nn0red 
 |-  ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( b e. W /\ c e. ran ( T ` b ) ) ) -> ( # ` b ) e. RR )
58 2rp 
 |-  2 e. RR+
59 ltaddrp 
 |-  ( ( ( # ` b ) e. RR /\ 2 e. RR+ ) -> ( # ` b ) < ( ( # ` b ) + 2 ) )
60 57 58 59 sylancl 
 |-  ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( b e. W /\ c e. ran ( T ` b ) ) ) -> ( # ` b ) < ( ( # ` b ) + 2 ) )
61 1 2 3 4 efgtlen 
 |-  ( ( b e. W /\ c e. ran ( T ` b ) ) -> ( # ` c ) = ( ( # ` b ) + 2 ) )
62 61 adantl 
 |-  ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( b e. W /\ c e. ran ( T ` b ) ) ) -> ( # ` c ) = ( ( # ` b ) + 2 ) )
63 simpl3 
 |-  ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( b e. W /\ c e. ran ( T ` b ) ) ) -> ( # ` c ) = d )
64 62 63 eqtr3d 
 |-  ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( b e. W /\ c e. ran ( T ` b ) ) ) -> ( ( # ` b ) + 2 ) = d )
65 60 64 breqtrd 
 |-  ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( b e. W /\ c e. ran ( T ` b ) ) ) -> ( # ` b ) < d )
66 52 53 65 elrabd 
 |-  ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( b e. W /\ c e. ran ( T ` b ) ) ) -> b e. { a e. W | ( # ` a ) < d } )
67 50 66 sseldd 
 |-  ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( b e. W /\ c e. ran ( T ` b ) ) ) -> b e. ran S )
68 ffn 
 |-  ( S : dom S --> W -> S Fn dom S )
69 10 68 ax-mp 
 |-  S Fn dom S
70 fvelrnb 
 |-  ( S Fn dom S -> ( b e. ran S <-> E. o e. dom S ( S ` o ) = b ) )
71 69 70 ax-mp 
 |-  ( b e. ran S <-> E. o e. dom S ( S ` o ) = b )
72 67 71 sylib 
 |-  ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( b e. W /\ c e. ran ( T ` b ) ) ) -> E. o e. dom S ( S ` o ) = b )
73 simprrl 
 |-  ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( ( b e. W /\ c e. ran ( T ` b ) ) /\ ( o e. dom S /\ ( S ` o ) = b ) ) ) -> o e. dom S )
74 1 2 3 4 5 6 efgsdm 
 |-  ( o e. dom S <-> ( o e. ( Word W \ { (/) } ) /\ ( o ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` o ) ) ( o ` i ) e. ran ( T ` ( o ` ( i - 1 ) ) ) ) )
75 74 simp1bi 
 |-  ( o e. dom S -> o e. ( Word W \ { (/) } ) )
76 eldifi 
 |-  ( o e. ( Word W \ { (/) } ) -> o e. Word W )
77 73 75 76 3syl 
 |-  ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( ( b e. W /\ c e. ran ( T ` b ) ) /\ ( o e. dom S /\ ( S ` o ) = b ) ) ) -> o e. Word W )
78 simpl2 
 |-  ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( ( b e. W /\ c e. ran ( T ` b ) ) /\ ( o e. dom S /\ ( S ` o ) = b ) ) ) -> c e. W )
79 simprlr 
 |-  ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( ( b e. W /\ c e. ran ( T ` b ) ) /\ ( o e. dom S /\ ( S ` o ) = b ) ) ) -> c e. ran ( T ` b ) )
80 simprrr 
 |-  ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( ( b e. W /\ c e. ran ( T ` b ) ) /\ ( o e. dom S /\ ( S ` o ) = b ) ) ) -> ( S ` o ) = b )
81 80 fveq2d 
 |-  ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( ( b e. W /\ c e. ran ( T ` b ) ) /\ ( o e. dom S /\ ( S ` o ) = b ) ) ) -> ( T ` ( S ` o ) ) = ( T ` b ) )
82 81 rneqd 
 |-  ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( ( b e. W /\ c e. ran ( T ` b ) ) /\ ( o e. dom S /\ ( S ` o ) = b ) ) ) -> ran ( T ` ( S ` o ) ) = ran ( T ` b ) )
83 79 82 eleqtrrd 
 |-  ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( ( b e. W /\ c e. ran ( T ` b ) ) /\ ( o e. dom S /\ ( S ` o ) = b ) ) ) -> c e. ran ( T ` ( S ` o ) ) )
84 1 2 3 4 5 6 efgsp1 
 |-  ( ( o e. dom S /\ c e. ran ( T ` ( S ` o ) ) ) -> ( o ++ <" c "> ) e. dom S )
85 73 83 84 syl2anc 
 |-  ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( ( b e. W /\ c e. ran ( T ` b ) ) /\ ( o e. dom S /\ ( S ` o ) = b ) ) ) -> ( o ++ <" c "> ) e. dom S )
86 1 2 3 4 5 6 efgsval2 
 |-  ( ( o e. Word W /\ c e. W /\ ( o ++ <" c "> ) e. dom S ) -> ( S ` ( o ++ <" c "> ) ) = c )
87 77 78 85 86 syl3anc 
 |-  ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( ( b e. W /\ c e. ran ( T ` b ) ) /\ ( o e. dom S /\ ( S ` o ) = b ) ) ) -> ( S ` ( o ++ <" c "> ) ) = c )
88 fnfvelrn 
 |-  ( ( S Fn dom S /\ ( o ++ <" c "> ) e. dom S ) -> ( S ` ( o ++ <" c "> ) ) e. ran S )
89 69 85 88 sylancr 
 |-  ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( ( b e. W /\ c e. ran ( T ` b ) ) /\ ( o e. dom S /\ ( S ` o ) = b ) ) ) -> ( S ` ( o ++ <" c "> ) ) e. ran S )
90 87 89 eqeltrrd 
 |-  ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( ( b e. W /\ c e. ran ( T ` b ) ) /\ ( o e. dom S /\ ( S ` o ) = b ) ) ) -> c e. ran S )
91 90 anassrs 
 |-  ( ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( b e. W /\ c e. ran ( T ` b ) ) ) /\ ( o e. dom S /\ ( S ` o ) = b ) ) -> c e. ran S )
92 72 91 rexlimddv 
 |-  ( ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) /\ ( b e. W /\ c e. ran ( T ` b ) ) ) -> c e. ran S )
93 92 rexlimdvaa 
 |-  ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) -> ( E. b e. W c e. ran ( T ` b ) -> c e. ran S ) )
94 49 93 syl5bi 
 |-  ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) -> ( c e. U_ x e. W ran ( T ` x ) -> c e. ran S ) )
95 eldif 
 |-  ( c e. ( W \ U_ x e. W ran ( T ` x ) ) <-> ( c e. W /\ -. c e. U_ x e. W ran ( T ` x ) ) )
96 5 eleq2i 
 |-  ( c e. D <-> c e. ( W \ U_ x e. W ran ( T ` x ) ) )
97 1 2 3 4 5 6 efgs1 
 |-  ( c e. D -> <" c "> e. dom S )
98 96 97 sylbir 
 |-  ( c e. ( W \ U_ x e. W ran ( T ` x ) ) -> <" c "> e. dom S )
99 95 98 sylbir 
 |-  ( ( c e. W /\ -. c e. U_ x e. W ran ( T ` x ) ) -> <" c "> e. dom S )
100 1 2 3 4 5 6 efgsval 
 |-  ( <" c "> e. dom S -> ( S ` <" c "> ) = ( <" c "> ` ( ( # ` <" c "> ) - 1 ) ) )
101 99 100 syl 
 |-  ( ( c e. W /\ -. c e. U_ x e. W ran ( T ` x ) ) -> ( S ` <" c "> ) = ( <" c "> ` ( ( # ` <" c "> ) - 1 ) ) )
102 s1len 
 |-  ( # ` <" c "> ) = 1
103 102 oveq1i 
 |-  ( ( # ` <" c "> ) - 1 ) = ( 1 - 1 )
104 1m1e0 
 |-  ( 1 - 1 ) = 0
105 103 104 eqtri 
 |-  ( ( # ` <" c "> ) - 1 ) = 0
106 105 fveq2i 
 |-  ( <" c "> ` ( ( # ` <" c "> ) - 1 ) ) = ( <" c "> ` 0 )
107 106 a1i 
 |-  ( ( c e. W /\ -. c e. U_ x e. W ran ( T ` x ) ) -> ( <" c "> ` ( ( # ` <" c "> ) - 1 ) ) = ( <" c "> ` 0 ) )
108 s1fv 
 |-  ( c e. W -> ( <" c "> ` 0 ) = c )
109 108 adantr 
 |-  ( ( c e. W /\ -. c e. U_ x e. W ran ( T ` x ) ) -> ( <" c "> ` 0 ) = c )
110 101 107 109 3eqtrd 
 |-  ( ( c e. W /\ -. c e. U_ x e. W ran ( T ` x ) ) -> ( S ` <" c "> ) = c )
111 fnfvelrn 
 |-  ( ( S Fn dom S /\ <" c "> e. dom S ) -> ( S ` <" c "> ) e. ran S )
112 69 99 111 sylancr 
 |-  ( ( c e. W /\ -. c e. U_ x e. W ran ( T ` x ) ) -> ( S ` <" c "> ) e. ran S )
113 110 112 eqeltrrd 
 |-  ( ( c e. W /\ -. c e. U_ x e. W ran ( T ` x ) ) -> c e. ran S )
114 113 ex 
 |-  ( c e. W -> ( -. c e. U_ x e. W ran ( T ` x ) -> c e. ran S ) )
115 114 3ad2ant2 
 |-  ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) -> ( -. c e. U_ x e. W ran ( T ` x ) -> c e. ran S ) )
116 94 115 pm2.61d 
 |-  ( ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) /\ c e. W /\ ( # ` c ) = d ) -> c e. ran S )
117 116 rabssdv 
 |-  ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) -> { c e. W | ( # ` c ) = d } C_ ran S )
118 43 117 eqsstrid 
 |-  ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) -> { a e. W | ( # ` a ) = d } C_ ran S )
119 41 118 unssd 
 |-  ( ( d e. NN0 /\ { a e. W | ( # ` a ) < d } C_ ran S ) -> ( { a e. W | ( # ` a ) < d } u. { a e. W | ( # ` a ) = d } ) C_ ran S )
120 119 ex 
 |-  ( d e. NN0 -> ( { a e. W | ( # ` a ) < d } C_ ran S -> ( { a e. W | ( # ` a ) < d } u. { a e. W | ( # ` a ) = d } ) C_ ran S ) )
121 id 
 |-  ( d e. NN0 -> d e. NN0 )
122 nn0leltp1 
 |-  ( ( ( # ` a ) e. NN0 /\ d e. NN0 ) -> ( ( # ` a ) <_ d <-> ( # ` a ) < ( d + 1 ) ) )
123 21 121 122 syl2anr 
 |-  ( ( d e. NN0 /\ a e. W ) -> ( ( # ` a ) <_ d <-> ( # ` a ) < ( d + 1 ) ) )
124 21 nn0red 
 |-  ( a e. W -> ( # ` a ) e. RR )
125 nn0re 
 |-  ( d e. NN0 -> d e. RR )
126 leloe 
 |-  ( ( ( # ` a ) e. RR /\ d e. RR ) -> ( ( # ` a ) <_ d <-> ( ( # ` a ) < d \/ ( # ` a ) = d ) ) )
127 124 125 126 syl2anr 
 |-  ( ( d e. NN0 /\ a e. W ) -> ( ( # ` a ) <_ d <-> ( ( # ` a ) < d \/ ( # ` a ) = d ) ) )
128 123 127 bitr3d 
 |-  ( ( d e. NN0 /\ a e. W ) -> ( ( # ` a ) < ( d + 1 ) <-> ( ( # ` a ) < d \/ ( # ` a ) = d ) ) )
129 128 rabbidva 
 |-  ( d e. NN0 -> { a e. W | ( # ` a ) < ( d + 1 ) } = { a e. W | ( ( # ` a ) < d \/ ( # ` a ) = d ) } )
130 unrab 
 |-  ( { a e. W | ( # ` a ) < d } u. { a e. W | ( # ` a ) = d } ) = { a e. W | ( ( # ` a ) < d \/ ( # ` a ) = d ) }
131 129 130 eqtr4di 
 |-  ( d e. NN0 -> { a e. W | ( # ` a ) < ( d + 1 ) } = ( { a e. W | ( # ` a ) < d } u. { a e. W | ( # ` a ) = d } ) )
132 131 sseq1d 
 |-  ( d e. NN0 -> ( { a e. W | ( # ` a ) < ( d + 1 ) } C_ ran S <-> ( { a e. W | ( # ` a ) < d } u. { a e. W | ( # ` a ) = d } ) C_ ran S ) )
133 120 132 sylibrd 
 |-  ( d e. NN0 -> ( { a e. W | ( # ` a ) < d } C_ ran S -> { a e. W | ( # ` a ) < ( d + 1 ) } C_ ran S ) )
134 30 33 36 39 40 133 nn0ind 
 |-  ( ( ( # ` c ) + 1 ) e. NN0 -> { a e. W | ( # ` a ) < ( ( # ` c ) + 1 ) } C_ ran S )
135 17 18 134 3syl 
 |-  ( c e. W -> { a e. W | ( # ` a ) < ( ( # ` c ) + 1 ) } C_ ran S )
136 fveq2 
 |-  ( a = c -> ( # ` a ) = ( # ` c ) )
137 136 breq1d 
 |-  ( a = c -> ( ( # ` a ) < ( ( # ` c ) + 1 ) <-> ( # ` c ) < ( ( # ` c ) + 1 ) ) )
138 id 
 |-  ( c e. W -> c e. W )
139 17 nn0red 
 |-  ( c e. W -> ( # ` c ) e. RR )
140 139 ltp1d 
 |-  ( c e. W -> ( # ` c ) < ( ( # ` c ) + 1 ) )
141 137 138 140 elrabd 
 |-  ( c e. W -> c e. { a e. W | ( # ` a ) < ( ( # ` c ) + 1 ) } )
142 135 141 sseldd 
 |-  ( c e. W -> c e. ran S )
143 142 ssriv 
 |-  W C_ ran S
144 12 143 eqssi 
 |-  ran S = W
145 dffo2 
 |-  ( S : dom S -onto-> W <-> ( S : dom S --> W /\ ran S = W ) )
146 10 144 145 mpbir2an 
 |-  S : dom S -onto-> W