MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xrinfmsslem Unicode version

Theorem xrinfmsslem 11528
Description: Lemma for xrinfmss 11530. (Contributed by NM, 19-Jan-2006.)
Assertion
Ref Expression
xrinfmsslem
Distinct variable group:   , , ,

Proof of Theorem xrinfmsslem
StepHypRef Expression
1 raleq 3054 . . . . . 6
2 rexeq 3055 . . . . . . . 8
32imbi2d 316 . . . . . . 7
43ralbidv 2896 . . . . . 6
51, 4anbi12d 710 . . . . 5
65rexbidv 2968 . . . 4
7 infm3 10527 . . . . . . . 8
8 rexr 9660 . . . . . . . . . 10
98anim1i 568 . . . . . . . . 9
109reximi2 2924 . . . . . . . 8
117, 10syl 16 . . . . . . 7
12 elxr 11354 . . . . . . . . . . . . 13
13 simpr 461 . . . . . . . . . . . . . 14
14 ssel 3497 . . . . . . . . . . . . . . . . . . . . . . . 24
15 ltpnf 11360 . . . . . . . . . . . . . . . . . . . . . . . 24
1614, 15syl6 33 . . . . . . . . . . . . . . . . . . . . . . 23
1716ancld 553 . . . . . . . . . . . . . . . . . . . . . 22
1817eximdv 1710 . . . . . . . . . . . . . . . . . . . . 21
19 n0 3794 . . . . . . . . . . . . . . . . . . . . 21
20 df-rex 2813 . . . . . . . . . . . . . . . . . . . . 21
2118, 19, 203imtr4g 270 . . . . . . . . . . . . . . . . . . . 20
2221imp 429 . . . . . . . . . . . . . . . . . . 19
2322a1d 25 . . . . . . . . . . . . . . . . . 18
2423ad2antrr 725 . . . . . . . . . . . . . . . . 17
25 breq2 4456 . . . . . . . . . . . . . . . . . . 19
26 breq2 4456 . . . . . . . . . . . . . . . . . . . 20
2726rexbidv 2968 . . . . . . . . . . . . . . . . . . 19
2825, 27imbi12d 320 . . . . . . . . . . . . . . . . . 18
2928adantl 466 . . . . . . . . . . . . . . . . 17
3024, 29mpbird 232 . . . . . . . . . . . . . . . 16
3130ex 434 . . . . . . . . . . . . . . 15
3231adantr 465 . . . . . . . . . . . . . 14
33 nltmnf 11367 . . . . . . . . . . . . . . . . . . 19
3433adantr 465 . . . . . . . . . . . . . . . . . 18
35 breq2 4456 . . . . . . . . . . . . . . . . . . . 20
3635notbid 294 . . . . . . . . . . . . . . . . . . 19
3736adantl 466 . . . . . . . . . . . . . . . . . 18
3834, 37mpbird 232 . . . . . . . . . . . . . . . . 17
3938pm2.21d 106 . . . . . . . . . . . . . . . 16
4039ex 434 . . . . . . . . . . . . . . 15
4140ad2antlr 726 . . . . . . . . . . . . . 14
4213, 32, 413jaod 1292 . . . . . . . . . . . . 13
4312, 42syl5bi 217 . . . . . . . . . . . 12
4443ex 434 . . . . . . . . . . 11
4544ralimdv2 2864 . . . . . . . . . 10
4645anim2d 565 . . . . . . . . 9
4746reximdva 2932 . . . . . . . 8
48473adant3 1016 . . . . . . 7
4911, 48mpd 15 . . . . . 6
50493expa 1196 . . . . 5
51 ralnex 2903 . . . . . . . . 9
52 rexnal 2905 . . . . . . . . . . . 12
53 ssel2 3498 . . . . . . . . . . . . . . 15
54 letric 9706 . . . . . . . . . . . . . . . . 17
5554ancoms 453 . . . . . . . . . . . . . . . 16
5655ord 377 . . . . . . . . . . . . . . 15
5753, 56sylan 471 . . . . . . . . . . . . . 14
5857an32s 804 . . . . . . . . . . . . 13
5958reximdva 2932 . . . . . . . . . . . 12
6052, 59syl5bir 218 . . . . . . . . . . 11
6160ralimdva 2865 . . . . . . . . . 10
6261imp 429 . . . . . . . . 9
6351, 62sylan2br 476 . . . . . . . 8
64 breq1 4455 . . . . . . . . . 10
6564cbvrexv 3085 . . . . . . . . 9
6665ralbii 2888 . . . . . . . 8
6763, 66sylib 196 . . . . . . 7
68 mnfxr 11352 . . . . . . . 8
69 ssel 3497 . . . . . . . . . . . 12
70 rexr 9660 . . . . . . . . . . . . 13
71 nltmnf 11367 . . . . . . . . . . . . 13
7270, 71syl 16 . . . . . . . . . . . 12
7369, 72syl6 33 . . . . . . . . . . 11
7473ralrimiv 2869 . . . . . . . . . 10
7574adantr 465 . . . . . . . . 9
76 peano2rem 9909 . . . . . . . . . . . . . . . . . . 19
77 breq2 4456 . . . . . . . . . . . . . . . . . . . . . . 23
7877rexbidv 2968 . . . . . . . . . . . . . . . . . . . . . 22
7978rspcva 3208 . . . . . . . . . . . . . . . . . . . . 21
8079adantrr 716 . . . . . . . . . . . . . . . . . . . 20
8180ancoms 453 . . . . . . . . . . . . . . . . . . 19
8276, 81sylan2 474 . . . . . . . . . . . . . . . . . 18
83 ssel2 3498 . . . . . . . . . . . . . . . . . . . . . 22
84 ltm1 10407 . . . . . . . . . . . . . . . . . . . . . . . 24
8584adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23
8676ancri 552 . . . . . . . . . . . . . . . . . . . . . . . 24
87 lelttr 9696 . . . . . . . . . . . . . . . . . . . . . . . . 25
88873expb 1197 . . . . . . . . . . . . . . . . . . . . . . . 24
8986, 88sylan2 474 . . . . . . . . . . . . . . . . . . . . . . 23
9085, 89mpan2d 674 . . . . . . . . . . . . . . . . . . . . . 22
9183, 90sylan 471 . . . . . . . . . . . . . . . . . . . . 21
9291an32s 804 . . . . . . . . . . . . . . . . . . . 20
9392reximdva 2932 . . . . . . . . . . . . . . . . . . 19
9493adantll 713 . . . . . . . . . . . . . . . . . 18
9582, 94mpd 15 . . . . . . . . . . . . . . . . 17
9695exp31 604 . . . . . . . . . . . . . . . 16
9796a1dd 46 . . . . . . . . . . . . . . 15
9897com4r 86 . . . . . . . . . . . . . 14
99 0re 9617 . . . . . . . . . . . . . . . . . . 19
100 breq2 4456 . . . . . . . . . . . . . . . . . . . . 21
101100rexbidv 2968 . . . . . . . . . . . . . . . . . . . 20
102101rspcva 3208 . . . . . . . . . . . . . . . . . . 19
10399, 102mpan 670 . . . . . . . . . . . . . . . . . 18
10483, 15syl 16 . . . . . . . . . . . . . . . . . . . 20
105104a1d 25 . . . . . . . . . . . . . . . . . . 19
106105reximdva 2932 . . . . . . . . . . . . . . . . . 18
107103, 106mpan9 469 . . . . . . . . . . . . . . . . 17
108107, 27syl5ibr 221 . . . . . . . . . . . . . . . 16
109108a1dd 46 . . . . . . . . . . . . . . 15
110109expd 436 . . . . . . . . . . . . . 14
111 xrltnr 11359 . . . . . . . . . . . . . . . . . . 19
11268, 111ax-mp 5 . . . . . . . . . . . . . . . . . 18
113 breq2 4456 . . . . . . . . . . . . . . . . . 18
114112, 113mtbiri 303 . . . . . . . . . . . . . . . . 17
115114pm2.21d 106 . . . . . . . . . . . . . . . 16
116115a1d 25 . . . . . . . . . . . . . . 15
117116a1d 25 . . . . . . . . . . . . . 14
11898, 110, 1173jaoi 1291 . . . . . . . . . . . . 13
11912, 118sylbi 195 . . . . . . . . . . . 12
120119com13 80 . . . . . . . . . . 11
121120imp 429 . . . . . . . . . 10
122121ralrimiv 2869 . . . . . . . . 9
12375, 122jca 532 . . . . . . . 8
124 breq2 4456 . . . . . . . . . . . 12
125124notbid 294 . . . . . . . . . . 11
126125ralbidv 2896 . . . . . . . . . 10
127 breq1 4455 . . . . . . . . . . . 12
128127imbi1d 317 . . . . . . . . . . 11
129128ralbidv 2896 . . . . . . . . . 10
130126, 129anbi12d 710 . . . . . . . . 9
131130rspcev 3210 . . . . . . . 8
13268, 123, 131sylancr 663 . . . . . . 7
13367, 132syldan 470 . . . . . 6
134133adantlr 714 . . . . 5
13550, 134pm2.61dan 791 . . . 4
136 pnfxr 11350 . . . . . 6
137 ral0 3934 . . . . . . 7
138 pnfnlt 11366 . . . . . . . . 9
139138pm2.21d 106 . . . . . . . 8
140139rgen 2817 . . . . . . 7
141137, 140pm3.2i 455 . . . . . 6
142 breq2 4456 . . . . . . . . . 10
143142notbid 294 . . . . . . . . 9
144143ralbidv 2896 . . . . . . . 8
145 breq1 4455 . . . . . . . . . 10
146145imbi1d 317 . . . . . . . . 9
147146ralbidv 2896 . . . . . . . 8
148144, 147anbi12d 710 . . . . . . 7
149148rspcev 3210 . . . . . 6
150136, 141, 149mp2an 672 . . . . 5
151150a1i 11 . . . 4
1526, 135, 151pm2.61ne 2772 . . 3
153152adantl 466 . 2
154 ssel 3497 . . . . . 6
155154, 71syl6 33 . . . . 5
156155ralrimiv 2869 . . . 4
157 breq1 4455 . . . . . . 7
158157rspcev 3210 . . . . . 6
159158ex 434 . . . . 5
160159ralrimivw 2872 . . . 4
161156, 160anim12i 566 . . 3
16268, 161, 131sylancr 663 . 2
163153, 162jaodan 785 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368  /\wa 369  \/w3o 972  /\w3a 973  =wceq 1395  E.wex 1612  e.wcel 1818  =/=wne 2652  A.wral 2807  E.wrex 2808  C_wss 3475   c0 3784   class class class wbr 4452  (class class class)co 6296   cr 9512  0cc0 9513  1c1 9514   cpnf 9646   cmnf 9647   cxr 9648   clt 9649   cle 9650   cmin 9828
This theorem is referenced by:  xrinfmss  11530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-cnex 9569  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-mulcom 9577  ax-addass 9578  ax-mulass 9579  ax-distr 9580  ax-i2m1 9581  ax-1ne0 9582  ax-1rid 9583  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586  ax-pre-lttri 9587  ax-pre-lttrn 9588  ax-pre-ltadd 9589  ax-pre-mulgt0 9590  ax-pre-sup 9591
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-po 4805  df-so 4806  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-riota 6257  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-er 7330  df-en 7537  df-dom 7538  df-sdom 7539  df-pnf 9651  df-mnf 9652  df-xr 9653  df-ltxr 9654  df-le 9655  df-sub 9830  df-neg 9831
  Copyright terms: Public domain W3C validator