This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem vitalilem2

Description: Lemma for vitali . (Contributed by Mario Carneiro, 16-Jun-2014)

Ref Expression
Hypotheses vitali.1 
|- .~ = { <. x , y >. | ( ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) /\ ( x - y ) e. QQ ) }
vitali.2 
|- S = ( ( 0 [,] 1 ) /. .~ )
vitali.3 
|- ( ph -> F Fn S )
vitali.4 
|- ( ph -> A. z e. S ( z =/= (/) -> ( F ` z ) e. z ) )
vitali.5 
|- ( ph -> G : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) )
vitali.6 
|- T = ( n e. NN |-> { s e. RR | ( s - ( G ` n ) ) e. ran F } )
vitali.7 
|- ( ph -> -. ran F e. ( ~P RR \ dom vol ) )
Assertion vitalilem2 
|- ( ph -> ( ran F C_ ( 0 [,] 1 ) /\ ( 0 [,] 1 ) C_ U_ m e. NN ( T ` m ) /\ U_ m e. NN ( T ` m ) C_ ( -u 1 [,] 2 ) ) )

Proof

Step Hyp Ref Expression
1 vitali.1 
 |-  .~ = { <. x , y >. | ( ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) /\ ( x - y ) e. QQ ) }
2 vitali.2 
 |-  S = ( ( 0 [,] 1 ) /. .~ )
3 vitali.3 
 |-  ( ph -> F Fn S )
4 vitali.4 
 |-  ( ph -> A. z e. S ( z =/= (/) -> ( F ` z ) e. z ) )
5 vitali.5 
 |-  ( ph -> G : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) )
6 vitali.6 
 |-  T = ( n e. NN |-> { s e. RR | ( s - ( G ` n ) ) e. ran F } )
7 vitali.7 
 |-  ( ph -> -. ran F e. ( ~P RR \ dom vol ) )
8 neeq1 
 |-  ( [ v ] .~ = z -> ( [ v ] .~ =/= (/) <-> z =/= (/) ) )
9 1 vitalilem1 
 |-  .~ Er ( 0 [,] 1 )
10 erdm 
 |-  ( .~ Er ( 0 [,] 1 ) -> dom .~ = ( 0 [,] 1 ) )
11 9 10 ax-mp 
 |-  dom .~ = ( 0 [,] 1 )
12 11 eleq2i 
 |-  ( v e. dom .~ <-> v e. ( 0 [,] 1 ) )
13 ecdmn0 
 |-  ( v e. dom .~ <-> [ v ] .~ =/= (/) )
14 12 13 bitr3i 
 |-  ( v e. ( 0 [,] 1 ) <-> [ v ] .~ =/= (/) )
15 14 biimpi 
 |-  ( v e. ( 0 [,] 1 ) -> [ v ] .~ =/= (/) )
16 2 8 15 ectocl 
 |-  ( z e. S -> z =/= (/) )
17 16 adantl 
 |-  ( ( ph /\ z e. S ) -> z =/= (/) )
18 sseq1 
 |-  ( [ w ] .~ = z -> ( [ w ] .~ C_ ( 0 [,] 1 ) <-> z C_ ( 0 [,] 1 ) ) )
19 9 a1i 
 |-  ( w e. ( 0 [,] 1 ) -> .~ Er ( 0 [,] 1 ) )
20 19 ecss 
 |-  ( w e. ( 0 [,] 1 ) -> [ w ] .~ C_ ( 0 [,] 1 ) )
21 2 18 20 ectocl 
 |-  ( z e. S -> z C_ ( 0 [,] 1 ) )
22 21 adantl 
 |-  ( ( ph /\ z e. S ) -> z C_ ( 0 [,] 1 ) )
23 22 sseld 
 |-  ( ( ph /\ z e. S ) -> ( ( F ` z ) e. z -> ( F ` z ) e. ( 0 [,] 1 ) ) )
24 17 23 embantd 
 |-  ( ( ph /\ z e. S ) -> ( ( z =/= (/) -> ( F ` z ) e. z ) -> ( F ` z ) e. ( 0 [,] 1 ) ) )
25 24 ralimdva 
 |-  ( ph -> ( A. z e. S ( z =/= (/) -> ( F ` z ) e. z ) -> A. z e. S ( F ` z ) e. ( 0 [,] 1 ) ) )
26 4 25 mpd 
 |-  ( ph -> A. z e. S ( F ` z ) e. ( 0 [,] 1 ) )
27 ffnfv 
 |-  ( F : S --> ( 0 [,] 1 ) <-> ( F Fn S /\ A. z e. S ( F ` z ) e. ( 0 [,] 1 ) ) )
28 3 26 27 sylanbrc 
 |-  ( ph -> F : S --> ( 0 [,] 1 ) )
29 28 frnd 
 |-  ( ph -> ran F C_ ( 0 [,] 1 ) )
30 5 adantr 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> G : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) )
31 f1ocnv 
 |-  ( G : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) -> `' G : ( QQ i^i ( -u 1 [,] 1 ) ) -1-1-onto-> NN )
32 f1of 
 |-  ( `' G : ( QQ i^i ( -u 1 [,] 1 ) ) -1-1-onto-> NN -> `' G : ( QQ i^i ( -u 1 [,] 1 ) ) --> NN )
33 30 31 32 3syl 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> `' G : ( QQ i^i ( -u 1 [,] 1 ) ) --> NN )
34 simpr 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> v e. ( 0 [,] 1 ) )
35 34 14 sylib 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> [ v ] .~ =/= (/) )
36 neeq1 
 |-  ( z = [ v ] .~ -> ( z =/= (/) <-> [ v ] .~ =/= (/) ) )
37 fveq2 
 |-  ( z = [ v ] .~ -> ( F ` z ) = ( F ` [ v ] .~ ) )
38 id 
 |-  ( z = [ v ] .~ -> z = [ v ] .~ )
39 37 38 eleq12d 
 |-  ( z = [ v ] .~ -> ( ( F ` z ) e. z <-> ( F ` [ v ] .~ ) e. [ v ] .~ ) )
40 36 39 imbi12d 
 |-  ( z = [ v ] .~ -> ( ( z =/= (/) -> ( F ` z ) e. z ) <-> ( [ v ] .~ =/= (/) -> ( F ` [ v ] .~ ) e. [ v ] .~ ) ) )
41 4 adantr 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> A. z e. S ( z =/= (/) -> ( F ` z ) e. z ) )
42 ovex 
 |-  ( 0 [,] 1 ) e. _V
43 erex 
 |-  ( .~ Er ( 0 [,] 1 ) -> ( ( 0 [,] 1 ) e. _V -> .~ e. _V ) )
44 9 42 43 mp2 
 |-  .~ e. _V
45 44 ecelqsi 
 |-  ( v e. ( 0 [,] 1 ) -> [ v ] .~ e. ( ( 0 [,] 1 ) /. .~ ) )
46 45 adantl 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> [ v ] .~ e. ( ( 0 [,] 1 ) /. .~ ) )
47 46 2 eleqtrrdi 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> [ v ] .~ e. S )
48 40 41 47 rspcdva 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( [ v ] .~ =/= (/) -> ( F ` [ v ] .~ ) e. [ v ] .~ ) )
49 35 48 mpd 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( F ` [ v ] .~ ) e. [ v ] .~ )
50 fvex 
 |-  ( F ` [ v ] .~ ) e. _V
51 vex 
 |-  v e. _V
52 50 51 elec 
 |-  ( ( F ` [ v ] .~ ) e. [ v ] .~ <-> v .~ ( F ` [ v ] .~ ) )
53 oveq12 
 |-  ( ( x = v /\ y = ( F ` [ v ] .~ ) ) -> ( x - y ) = ( v - ( F ` [ v ] .~ ) ) )
54 53 eleq1d 
 |-  ( ( x = v /\ y = ( F ` [ v ] .~ ) ) -> ( ( x - y ) e. QQ <-> ( v - ( F ` [ v ] .~ ) ) e. QQ ) )
55 54 1 brab2a 
 |-  ( v .~ ( F ` [ v ] .~ ) <-> ( ( v e. ( 0 [,] 1 ) /\ ( F ` [ v ] .~ ) e. ( 0 [,] 1 ) ) /\ ( v - ( F ` [ v ] .~ ) ) e. QQ ) )
56 52 55 bitri 
 |-  ( ( F ` [ v ] .~ ) e. [ v ] .~ <-> ( ( v e. ( 0 [,] 1 ) /\ ( F ` [ v ] .~ ) e. ( 0 [,] 1 ) ) /\ ( v - ( F ` [ v ] .~ ) ) e. QQ ) )
57 49 56 sylib 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( ( v e. ( 0 [,] 1 ) /\ ( F ` [ v ] .~ ) e. ( 0 [,] 1 ) ) /\ ( v - ( F ` [ v ] .~ ) ) e. QQ ) )
58 57 simprd 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( v - ( F ` [ v ] .~ ) ) e. QQ )
59 elicc01 
 |-  ( v e. ( 0 [,] 1 ) <-> ( v e. RR /\ 0 <_ v /\ v <_ 1 ) )
60 34 59 sylib 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( v e. RR /\ 0 <_ v /\ v <_ 1 ) )
61 60 simp1d 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> v e. RR )
62 57 simpld 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( v e. ( 0 [,] 1 ) /\ ( F ` [ v ] .~ ) e. ( 0 [,] 1 ) ) )
63 62 simprd 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( F ` [ v ] .~ ) e. ( 0 [,] 1 ) )
64 elicc01 
 |-  ( ( F ` [ v ] .~ ) e. ( 0 [,] 1 ) <-> ( ( F ` [ v ] .~ ) e. RR /\ 0 <_ ( F ` [ v ] .~ ) /\ ( F ` [ v ] .~ ) <_ 1 ) )
65 63 64 sylib 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( ( F ` [ v ] .~ ) e. RR /\ 0 <_ ( F ` [ v ] .~ ) /\ ( F ` [ v ] .~ ) <_ 1 ) )
66 65 simp1d 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( F ` [ v ] .~ ) e. RR )
67 61 66 resubcld 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( v - ( F ` [ v ] .~ ) ) e. RR )
68 66 61 resubcld 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( ( F ` [ v ] .~ ) - v ) e. RR )
69 1red 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> 1 e. RR )
70 60 simp2d 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> 0 <_ v )
71 66 61 subge02d 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( 0 <_ v <-> ( ( F ` [ v ] .~ ) - v ) <_ ( F ` [ v ] .~ ) ) )
72 70 71 mpbid 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( ( F ` [ v ] .~ ) - v ) <_ ( F ` [ v ] .~ ) )
73 65 simp3d 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( F ` [ v ] .~ ) <_ 1 )
74 68 66 69 72 73 letrd 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( ( F ` [ v ] .~ ) - v ) <_ 1 )
75 68 69 lenegd 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( ( ( F ` [ v ] .~ ) - v ) <_ 1 <-> -u 1 <_ -u ( ( F ` [ v ] .~ ) - v ) ) )
76 74 75 mpbid 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> -u 1 <_ -u ( ( F ` [ v ] .~ ) - v ) )
77 66 recnd 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( F ` [ v ] .~ ) e. CC )
78 61 recnd 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> v e. CC )
79 77 78 negsubdi2d 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> -u ( ( F ` [ v ] .~ ) - v ) = ( v - ( F ` [ v ] .~ ) ) )
80 76 79 breqtrd 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> -u 1 <_ ( v - ( F ` [ v ] .~ ) ) )
81 65 simp2d 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> 0 <_ ( F ` [ v ] .~ ) )
82 61 66 subge02d 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( 0 <_ ( F ` [ v ] .~ ) <-> ( v - ( F ` [ v ] .~ ) ) <_ v ) )
83 81 82 mpbid 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( v - ( F ` [ v ] .~ ) ) <_ v )
84 60 simp3d 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> v <_ 1 )
85 67 61 69 83 84 letrd 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( v - ( F ` [ v ] .~ ) ) <_ 1 )
86 neg1rr 
 |-  -u 1 e. RR
87 1re 
 |-  1 e. RR
88 86 87 elicc2i 
 |-  ( ( v - ( F ` [ v ] .~ ) ) e. ( -u 1 [,] 1 ) <-> ( ( v - ( F ` [ v ] .~ ) ) e. RR /\ -u 1 <_ ( v - ( F ` [ v ] .~ ) ) /\ ( v - ( F ` [ v ] .~ ) ) <_ 1 ) )
89 67 80 85 88 syl3anbrc 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( v - ( F ` [ v ] .~ ) ) e. ( -u 1 [,] 1 ) )
90 58 89 elind 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( v - ( F ` [ v ] .~ ) ) e. ( QQ i^i ( -u 1 [,] 1 ) ) )
91 33 90 ffvelcdmd 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) e. NN )
92 oveq1 
 |-  ( s = v -> ( s - ( G ` ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) ) ) = ( v - ( G ` ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) ) ) )
93 92 eleq1d 
 |-  ( s = v -> ( ( s - ( G ` ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) ) ) e. ran F <-> ( v - ( G ` ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) ) ) e. ran F ) )
94 f1ocnvfv2 
 |-  ( ( G : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) /\ ( v - ( F ` [ v ] .~ ) ) e. ( QQ i^i ( -u 1 [,] 1 ) ) ) -> ( G ` ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) ) = ( v - ( F ` [ v ] .~ ) ) )
95 5 90 94 syl2an2r 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( G ` ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) ) = ( v - ( F ` [ v ] .~ ) ) )
96 95 oveq2d 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( v - ( G ` ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) ) ) = ( v - ( v - ( F ` [ v ] .~ ) ) ) )
97 78 77 nncand 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( v - ( v - ( F ` [ v ] .~ ) ) ) = ( F ` [ v ] .~ ) )
98 96 97 eqtrd 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( v - ( G ` ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) ) ) = ( F ` [ v ] .~ ) )
99 fnfvelrn 
 |-  ( ( F Fn S /\ [ v ] .~ e. S ) -> ( F ` [ v ] .~ ) e. ran F )
100 3 47 99 syl2an2r 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( F ` [ v ] .~ ) e. ran F )
101 98 100 eqeltrd 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( v - ( G ` ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) ) ) e. ran F )
102 93 61 101 elrabd 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> v e. { s e. RR | ( s - ( G ` ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) ) ) e. ran F } )
103 fveq2 
 |-  ( n = ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) -> ( G ` n ) = ( G ` ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) ) )
104 103 oveq2d 
 |-  ( n = ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) -> ( s - ( G ` n ) ) = ( s - ( G ` ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) ) ) )
105 104 eleq1d 
 |-  ( n = ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) -> ( ( s - ( G ` n ) ) e. ran F <-> ( s - ( G ` ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) ) ) e. ran F ) )
106 105 rabbidv 
 |-  ( n = ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) -> { s e. RR | ( s - ( G ` n ) ) e. ran F } = { s e. RR | ( s - ( G ` ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) ) ) e. ran F } )
107 reex 
 |-  RR e. _V
108 107 rabex 
 |-  { s e. RR | ( s - ( G ` ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) ) ) e. ran F } e. _V
109 106 6 108 fvmpt 
 |-  ( ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) e. NN -> ( T ` ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) ) = { s e. RR | ( s - ( G ` ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) ) ) e. ran F } )
110 91 109 syl 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( T ` ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) ) = { s e. RR | ( s - ( G ` ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) ) ) e. ran F } )
111 102 110 eleqtrrd 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> v e. ( T ` ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) ) )
112 fveq2 
 |-  ( m = ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) -> ( T ` m ) = ( T ` ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) ) )
113 112 eliuni 
 |-  ( ( ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) e. NN /\ v e. ( T ` ( `' G ` ( v - ( F ` [ v ] .~ ) ) ) ) ) -> v e. U_ m e. NN ( T ` m ) )
114 91 111 113 syl2anc 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> v e. U_ m e. NN ( T ` m ) )
115 114 ex 
 |-  ( ph -> ( v e. ( 0 [,] 1 ) -> v e. U_ m e. NN ( T ` m ) ) )
116 115 ssrdv 
 |-  ( ph -> ( 0 [,] 1 ) C_ U_ m e. NN ( T ` m ) )
117 eliun 
 |-  ( x e. U_ m e. NN ( T ` m ) <-> E. m e. NN x e. ( T ` m ) )
118 fveq2 
 |-  ( n = m -> ( G ` n ) = ( G ` m ) )
119 118 oveq2d 
 |-  ( n = m -> ( s - ( G ` n ) ) = ( s - ( G ` m ) ) )
120 119 eleq1d 
 |-  ( n = m -> ( ( s - ( G ` n ) ) e. ran F <-> ( s - ( G ` m ) ) e. ran F ) )
121 120 rabbidv 
 |-  ( n = m -> { s e. RR | ( s - ( G ` n ) ) e. ran F } = { s e. RR | ( s - ( G ` m ) ) e. ran F } )
122 107 rabex 
 |-  { s e. RR | ( s - ( G ` m ) ) e. ran F } e. _V
123 121 6 122 fvmpt 
 |-  ( m e. NN -> ( T ` m ) = { s e. RR | ( s - ( G ` m ) ) e. ran F } )
124 123 adantl 
 |-  ( ( ph /\ m e. NN ) -> ( T ` m ) = { s e. RR | ( s - ( G ` m ) ) e. ran F } )
125 124 eleq2d 
 |-  ( ( ph /\ m e. NN ) -> ( x e. ( T ` m ) <-> x e. { s e. RR | ( s - ( G ` m ) ) e. ran F } ) )
126 125 biimpa 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> x e. { s e. RR | ( s - ( G ` m ) ) e. ran F } )
127 oveq1 
 |-  ( s = x -> ( s - ( G ` m ) ) = ( x - ( G ` m ) ) )
128 127 eleq1d 
 |-  ( s = x -> ( ( s - ( G ` m ) ) e. ran F <-> ( x - ( G ` m ) ) e. ran F ) )
129 128 elrab 
 |-  ( x e. { s e. RR | ( s - ( G ` m ) ) e. ran F } <-> ( x e. RR /\ ( x - ( G ` m ) ) e. ran F ) )
130 126 129 sylib 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> ( x e. RR /\ ( x - ( G ` m ) ) e. ran F ) )
131 130 simpld 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> x e. RR )
132 86 a1i 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> -u 1 e. RR )
133 iccssre 
 |-  ( ( -u 1 e. RR /\ 1 e. RR ) -> ( -u 1 [,] 1 ) C_ RR )
134 86 87 133 mp2an 
 |-  ( -u 1 [,] 1 ) C_ RR
135 f1of 
 |-  ( G : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) -> G : NN --> ( QQ i^i ( -u 1 [,] 1 ) ) )
136 5 135 syl 
 |-  ( ph -> G : NN --> ( QQ i^i ( -u 1 [,] 1 ) ) )
137 136 ffvelcdmda 
 |-  ( ( ph /\ m e. NN ) -> ( G ` m ) e. ( QQ i^i ( -u 1 [,] 1 ) ) )
138 137 elin2d 
 |-  ( ( ph /\ m e. NN ) -> ( G ` m ) e. ( -u 1 [,] 1 ) )
139 134 138 sselid 
 |-  ( ( ph /\ m e. NN ) -> ( G ` m ) e. RR )
140 139 adantr 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> ( G ` m ) e. RR )
141 138 adantr 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> ( G ` m ) e. ( -u 1 [,] 1 ) )
142 86 87 elicc2i 
 |-  ( ( G ` m ) e. ( -u 1 [,] 1 ) <-> ( ( G ` m ) e. RR /\ -u 1 <_ ( G ` m ) /\ ( G ` m ) <_ 1 ) )
143 141 142 sylib 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> ( ( G ` m ) e. RR /\ -u 1 <_ ( G ` m ) /\ ( G ` m ) <_ 1 ) )
144 143 simp2d 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> -u 1 <_ ( G ` m ) )
145 29 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> ran F C_ ( 0 [,] 1 ) )
146 130 simprd 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> ( x - ( G ` m ) ) e. ran F )
147 145 146 sseldd 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> ( x - ( G ` m ) ) e. ( 0 [,] 1 ) )
148 elicc01 
 |-  ( ( x - ( G ` m ) ) e. ( 0 [,] 1 ) <-> ( ( x - ( G ` m ) ) e. RR /\ 0 <_ ( x - ( G ` m ) ) /\ ( x - ( G ` m ) ) <_ 1 ) )
149 147 148 sylib 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> ( ( x - ( G ` m ) ) e. RR /\ 0 <_ ( x - ( G ` m ) ) /\ ( x - ( G ` m ) ) <_ 1 ) )
150 149 simp2d 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> 0 <_ ( x - ( G ` m ) ) )
151 131 140 subge0d 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> ( 0 <_ ( x - ( G ` m ) ) <-> ( G ` m ) <_ x ) )
152 150 151 mpbid 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> ( G ` m ) <_ x )
153 132 140 131 144 152 letrd 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> -u 1 <_ x )
154 peano2re 
 |-  ( ( G ` m ) e. RR -> ( ( G ` m ) + 1 ) e. RR )
155 140 154 syl 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> ( ( G ` m ) + 1 ) e. RR )
156 2re 
 |-  2 e. RR
157 156 a1i 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> 2 e. RR )
158 149 simp3d 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> ( x - ( G ` m ) ) <_ 1 )
159 1red 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> 1 e. RR )
160 131 140 159 lesubadd2d 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> ( ( x - ( G ` m ) ) <_ 1 <-> x <_ ( ( G ` m ) + 1 ) ) )
161 158 160 mpbid 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> x <_ ( ( G ` m ) + 1 ) )
162 143 simp3d 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> ( G ` m ) <_ 1 )
163 140 159 159 162 leadd1dd 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> ( ( G ` m ) + 1 ) <_ ( 1 + 1 ) )
164 df-2 
 |-  2 = ( 1 + 1 )
165 163 164 breqtrrdi 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> ( ( G ` m ) + 1 ) <_ 2 )
166 131 155 157 161 165 letrd 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> x <_ 2 )
167 86 156 elicc2i 
 |-  ( x e. ( -u 1 [,] 2 ) <-> ( x e. RR /\ -u 1 <_ x /\ x <_ 2 ) )
168 131 153 166 167 syl3anbrc 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. ( T ` m ) ) -> x e. ( -u 1 [,] 2 ) )
169 168 rexlimdva2 
 |-  ( ph -> ( E. m e. NN x e. ( T ` m ) -> x e. ( -u 1 [,] 2 ) ) )
170 117 169 biimtrid 
 |-  ( ph -> ( x e. U_ m e. NN ( T ` m ) -> x e. ( -u 1 [,] 2 ) ) )
171 170 ssrdv 
 |-  ( ph -> U_ m e. NN ( T ` m ) C_ ( -u 1 [,] 2 ) )
172 29 116 171 3jca 
 |-  ( ph -> ( ran F C_ ( 0 [,] 1 ) /\ ( 0 [,] 1 ) C_ U_ m e. NN ( T ` m ) /\ U_ m e. NN ( T ` m ) C_ ( -u 1 [,] 2 ) ) )