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 ) ) )