Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stoweidlem27 Unicode version

Theorem stoweidlem27 27878
 Description: This lemma is used to prove the existence of a function p as in Lemma 1 [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p(t_0) = 0, and p > 0 on T - U. Here is used to represent p(t_i) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem27.1
stoweidlem27.2
stoweidlem27.3
stoweidlem27.4
stoweidlem27.5
stoweidlem27.6
stoweidlem27.7
stoweidlem27.8
stoweidlem27.9
stoweidlem27.10
stoweidlem27.11
Assertion
Ref Expression
stoweidlem27
Distinct variable groups:   ,,,,   ,,,,   ,,   ,,,   ,   ,,   ,,   ,,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   (,,,)   (,,)   (,,)   (,,,)   ()   (,,,)   (,,)   (,,,)

Proof of Theorem stoweidlem27
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 stoweidlem27.3 . . 3
2 stoweidlem27.4 . . . . . . . 8
3 stoweidlem27.7 . . . . . . . . 9
4 f1of 5488 . . . . . . . . 9
53, 4syl 15 . . . . . . . 8
62, 5jca 518 . . . . . . 7
7 fnfco 5423 . . . . . . 7
86, 7syl 15 . . . . . 6
9 rncoss 4961 . . . . . . 7
10 fvelrnb 5586 . . . . . . . . . . . . 13
112, 10syl 15 . . . . . . . . . . . 12
1211biimpa 470 . . . . . . . . . . 11
13 simpr 447 . . . . . . . . . . . . . . . 16
14 stoweidlem27.1 . . . . . . . . . . . . . . . . . 18
1514elrnmpt 4942 . . . . . . . . . . . . . . . . 17
1613, 15syl 15 . . . . . . . . . . . . . . . 16
1713, 16mpbid 201 . . . . . . . . . . . . . . 15
18 stoweidlem27.10 . . . . . . . . . . . . . . . . 17
19 nfcv 2432 . . . . . . . . . . . . . . . . . 18
20 nfmpt1 4125 . . . . . . . . . . . . . . . . . . . 20
2114, 20nfcxfr 2429 . . . . . . . . . . . . . . . . . . 19
2221nfrn 4937 . . . . . . . . . . . . . . . . . 18
2319, 22nfel 2440 . . . . . . . . . . . . . . . . 17
2418, 23nfan 1783 . . . . . . . . . . . . . . . 16
25 nfv 1609 . . . . . . . . . . . . . . . 16
26 stoweidlem27.6 . . . . . . . . . . . . . . . . . . . . . 22
2726ad2antrr 706 . . . . . . . . . . . . . . . . . . . . 21
28 simpr 447 . . . . . . . . . . . . . . . . . . . . . 22
29 eleq2 2357 . . . . . . . . . . . . . . . . . . . . . 22
3028, 29syl 15 . . . . . . . . . . . . . . . . . . . . 21
3127, 30mpbid 201 . . . . . . . . . . . . . . . . . . . 20
32 nfcv 2432 . . . . . . . . . . . . . . . . . . . . 21
33 stoweidlem27.11 . . . . . . . . . . . . . . . . . . . . 21
34 nfv 1609 . . . . . . . . . . . . . . . . . . . . 21
35 fveq1 5540 . . . . . . . . . . . . . . . . . . . . . . . 24
3635breq2d 4051 . . . . . . . . . . . . . . . . . . . . . . 23
3736rabbidv 2793 . . . . . . . . . . . . . . . . . . . . . 22
3837eqeq2d 2307 . . . . . . . . . . . . . . . . . . . . 21
3932, 33, 34, 38elrabf 2935 . . . . . . . . . . . . . . . . . . . 20
4031, 39sylib 188 . . . . . . . . . . . . . . . . . . 19
4140simpld 445 . . . . . . . . . . . . . . . . . 18
4241ex 423 . . . . . . . . . . . . . . . . 17
4342ex 423 . . . . . . . . . . . . . . . 16
4424, 25, 43rexlimd 2677 . . . . . . . . . . . . . . 15
4517, 44mpd 14 . . . . . . . . . . . . . 14
4645adantlr 695 . . . . . . . . . . . . 13
47 eleq1 2356 . . . . . . . . . . . . 13
4846, 47syl5ibcom 211 . . . . . . . . . . . 12
4948reximdva 2668 . . . . . . . . . . 11
5012, 49mpd 14 . . . . . . . . . 10
51 idd 21 . . . . . . . . . . . 12
5251a1i 10 . . . . . . . . . . 11
5352rexlimdv 2679 . . . . . . . . . 10
5450, 53mpd 14 . . . . . . . . 9
5554ex 423 . . . . . . . 8
5655ssrdv 3198 . . . . . . 7
579, 56syl5ss 3203 . . . . . 6
588, 57jca 518 . . . . 5
59 df-f 5275 . . . . 5
6058, 59sylibr 203 . . . 4
61 stoweidlem27.9 . . . . 5
62 stoweidlem27.8 . . . . . . . . . 10
6362sselda 3193 . . . . . . . . 9
64 eluni 3846 . . . . . . . . 9
6563, 64sylib 188 . . . . . . . 8
66 nfv 1609 . . . . . . . . . 10
6718, 66nfan 1783 . . . . . . . . 9
68 simpl 443 . . . . . . . . . . . . . 14
69 simprr 733 . . . . . . . . . . . . . . . 16
7068, 69jca 518 . . . . . . . . . . . . . . 15
7114funmpt2 5307 . . . . . . . . . . . . . . . . . 18
7271a1i 10 . . . . . . . . . . . . . . . . 17
73 dmeq 4895 . . . . . . . . . . . . . . . . . . . . . 22
7414, 73ax-mp 8 . . . . . . . . . . . . . . . . . . . . 21
75 stoweidlem27.2 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7633rabexgf 27797 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7775, 76syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25
7877adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24
7978ex 423 . . . . . . . . . . . . . . . . . . . . . . 23
8018, 79ralrimi 2637 . . . . . . . . . . . . . . . . . . . . . 22
81 dmmptg 5186 . . . . . . . . . . . . . . . . . . . . . 22
8280, 81syl 15 . . . . . . . . . . . . . . . . . . . . 21
8374, 82syl5eq 2340 . . . . . . . . . . . . . . . . . . . 20
8483eleq2d 2363 . . . . . . . . . . . . . . . . . . 19
8584biimprd 214 . . . . . . . . . . . . . . . . . 18
8685imp 418 . . . . . . . . . . . . . . . . 17
8772, 86jca 518 . . . . . . . . . . . . . . . 16
88 fvelrn 5677 . . . . . . . . . . . . . . . 16
8987, 88syl 15 . . . . . . . . . . . . . . 15
9070, 89syl 15 . . . . . . . . . . . . . 14
9168, 90jca 518 . . . . . . . . . . . . 13
92 f1ofo 5495 . . . . . . . . . . . . . . . . . . . 20
93 forn 5470 . . . . . . . . . . . . . . . . . . . 20
943, 92, 933syl 18 . . . . . . . . . . . . . . . . . . 19
9594eleq2d 2363 . . . . . . . . . . . . . . . . . 18
9695biimpar 471 . . . . . . . . . . . . . . . . 17
97 f1ofn 5489 . . . . . . . . . . . . . . . . . . . 20
983, 97syl 15 . . . . . . . . . . . . . . . . . . 19
9998adantr 451 . . . . . . . . . . . . . . . . . 18
100 fvelrnb 5586 . . . . . . . . . . . . . . . . . 18
10199, 100syl 15 . . . . . . . . . . . . . . . . 17
10296, 101mpbid 201 . . . . . . . . . . . . . . . 16
103 df-rex 2562 . . . . . . . . . . . . . . . 16
104102, 103sylib 188 . . . . . . . . . . . . . . 15
105 simprl 732 . . . . . . . . . . . . . . . . . 18
1065adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23
107106adantr 451 . . . . . . . . . . . . . . . . . . . . . 22
108107, 105jca 518 . . . . . . . . . . . . . . . . . . . . 21
109 fvco3 5612 . . . . . . . . . . . . . . . . . . . . 21
110108, 109syl 15 . . . . . . . . . . . . . . . . . . . 20
111 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . 22
112111adantl 452 . . . . . . . . . . . . . . . . . . . . 21
113112adantl 452 . . . . . . . . . . . . . . . . . . . 20
114110, 113eqtrd 2328 . . . . . . . . . . . . . . . . . . 19
115 simpr 447 . . . . . . . . . . . . . . . . . . . . . 22
116 eleq1 2356 . . . . . . . . . . . . . . . . . . . . . . . . 25
117116anbi2d 684 . . . . . . . . . . . . . . . . . . . . . . . 24
118 eleq2 2357 . . . . . . . . . . . . . . . . . . . . . . . . 25
119 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . 26
120119eleq1d 2362 . . . . . . . . . . . . . . . . . . . . . . . . 25
121118, 120bitrd 244 . . . . . . . . . . . . . . . . . . . . . . . 24
122117, 121imbi12d 311 . . . . . . . . . . . . . . . . . . . . . . 23
12326a1i 10 . . . . . . . . . . . . . . . . . . . . . . 23
124122, 123vtoclga 2862 . . . . . . . . . . . . . . . . . . . . . 22
125115, 124syl 15 . . . . . . . . . . . . . . . . . . . . 21
126125pm2.43i 43 . . . . . . . . . . . . . . . . . . . 20
127126adantr 451 . . . . . . . . . . . . . . . . . . 19
128114, 127eqeltrd 2370 . . . . . . . . . . . . . . . . . 18
129105, 128jca 518 . . . . . . . . . . . . . . . . 17
130129ex 423 . . . . . . . . . . . . . . . 16
131130eximdv 1612 . . . . . . . . . . . . . . 15
132104, 131mpd 14 . . . . . . . . . . . . . 14
133 df-rex 2562 . . . . . . . . . . . . . 14
134132, 133sylibr 203 . . . . . . . . . . . . 13
13591, 134syl 15 . . . . . . . . . . . 12
136 simplrl 736 . . . . . . . . . . . . . . . . 17
137 simpll 730 . . . . . . . . . . . . . . . . . . . . . 22
138 simplrr 737 . . . . . . . . . . . . . . . . . . . . . 22
139137, 138jca 518 . . . . . . . . . . . . . . . . . . . . 21
140 simpr 447 . . . . . . . . . . . . . . . . . . . . 21
141139, 140jca 518 . . . . . . . . . . . . . . . . . . . 20
142 simpr 447 . . . . . . . . . . . . . . . . . . . . 21
143 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . 25
144143, 78jca 518 . . . . . . . . . . . . . . . . . . . . . . . 24
14514fvmpt2 5624 . . . . . . . . . . . . . . . . . . . . . . . 24
146144, 145syl 15 . . . . . . . . . . . . . . . . . . . . . . 23
147146eleq2d 2363 . . . . . . . . . . . . . . . . . . . . . 22
148147biimpa 470 . . . . . . . . . . . . . . . . . . . . 21
149142, 148syldan 456 . . . . . . . . . . . . . . . . . . . 20
150141, 149syl 15 . . . . . . . . . . . . . . . . . . 19
151 nfcv 2432 . . . . . . . . . . . . . . . . . . . 20
152 nfv 1609 . . . . . . . . . . . . . . . . . . . 20
153 fveq1 5540 . . . . . . . . . . . . . . . . . . . . . . 23
154153breq2d 4051 . . . . . . . . . . . . . . . . . . . . . 22
155154rabbidv 2793 . . . . . . . . . . . . . . . . . . . . 21
156155eqeq2d 2307 . . . . . . . . . . . . . . . . . . . 20
157151, 33, 152, 156elrabf 2935 . . . . . . . . . . . . . . . . . . 19
158150, 157sylib 188 . . . . . . . . . . . . . . . . . 18
159158simprd 449 . . . . . . . . . . . . . . . . 17
160136, 159eleqtrd 2372 . . . . . . . . . . . . . . . 16
161 rabid 2729 . . . . . . . . . . . . . . . 16
162160, 161sylib 188 . . . . . . . . . . . . . . 15
163162simprd 449 . . . . . . . . . . . . . 14
164163ex 423 . . . . . . . . . . . . 13
165164reximdv 2667 . . . . . . . . . . . 12
166135, 165mpd 14 . . . . . . . . . . 11
167166ex 423 . . . . . . . . . 10
168167adantr 451 . . . . . . . . 9
16967, 168eximd 1762 . . . . . . . 8
17065, 169mpd 14 . . . . . . 7
171 nfv 1609 . . . . . . . 8
172 idd 21 . . . . . . . 8
17367, 171, 172exlimd 1815 . . . . . . 7
174170, 173mpd 14 . . . . . 6
175174ex 423 . . . . 5
17661, 175ralrimi 2637 . . . 4
17760, 176jca 518 . . 3
1781, 177jca 518 . 2
179 stoweidlem27.5 . . . . . . 7
1802, 179jca 518 . . . . . 6
181 fnex 5757 . . . . . 6
182180, 181syl 15 . . . . 5
183 ovex 5899 . . . . . . . 8
184183a1i 10 . . . . . . 7
18598, 184jca 518 . . . . . 6
186 fnex 5757 . . . . . 6
187185, 186syl 15 . . . . 5
188182, 187jca 518 . . . 4
189 coexg 5231 . . . 4
190188, 189syl 15 . . 3
191 feq1 5391 . . . . . 6
192 fveq1 5540 . . . . . . . . . 10
193192fveq1d 5543 . . . . . . . . 9
194193breq2d 4051 . . . . . . . 8
195194rexbidv 2577 . . . . . . 7
196195ralbidv 2576 . . . . . 6
197191, 196anbi12d 691 . . . . 5
198197anbi2d 684 . . . 4
199198spcegv 2882 . . 3
200190, 199syl 15 . 2
201178, 200mpd 14 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358  wex 1531  wnf 1534   wceq 1632   wcel 1696  wnfc 2419  wral 2556  wrex 2557  crab 2560  cvv 2801   cdif 3162   wss 3165  cuni 3843   class class class wbr 4039   cmpt 4093   cdm 4705   crn 4706   ccom 4709   wfun 5265   wfn 5266  wf 5267  wfo 5269  wf1o 5270  cfv 5271  (class class class)co 5874  cc0 8753  c1 8754   clt 8883  cn 9762  cfz 10798 This theorem is referenced by:  stoweidlem35  27886 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-rep 4147  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-reu 2563  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-id 4325  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-ov 5877
 Copyright terms: Public domain W3C validator