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

Theorem xrsupsslem 11527
Description: Lemma for xrsupss 11529. (Contributed by NM, 25-Oct-2005.)
Assertion
Ref Expression
xrsupsslem
Distinct variable group:   , , ,

Proof of Theorem xrsupsslem
StepHypRef Expression
1 raleq 3054 . . . . . 6
2 rexeq 3055 . . . . . . . 8
32imbi2d 316 . . . . . . 7
43ralbidv 2896 . . . . . 6
51, 4anbi12d 710 . . . . 5
65rexbidv 2968 . . . 4
7 sup3 10525 . . . . . . . 8
8 rexr 9660 . . . . . . . . . 10
98anim1i 568 . . . . . . . . 9
109reximi2 2924 . . . . . . . 8
117, 10syl 16 . . . . . . 7
12 elxr 11354 . . . . . . . . . . . . 13
13 simpr 461 . . . . . . . . . . . . . 14
14 pnfnlt 11366 . . . . . . . . . . . . . . . . . . 19
1514adantr 465 . . . . . . . . . . . . . . . . . 18
16 breq1 4455 . . . . . . . . . . . . . . . . . . . 20
1716notbid 294 . . . . . . . . . . . . . . . . . . 19
1817adantl 466 . . . . . . . . . . . . . . . . . 18
1915, 18mpbird 232 . . . . . . . . . . . . . . . . 17
2019pm2.21d 106 . . . . . . . . . . . . . . . 16
2120ex 434 . . . . . . . . . . . . . . 15
2221ad2antlr 726 . . . . . . . . . . . . . 14
23 ssel 3497 . . . . . . . . . . . . . . . . . . . . . . . 24
24 mnflt 11362 . . . . . . . . . . . . . . . . . . . . . . . 24
2523, 24syl6 33 . . . . . . . . . . . . . . . . . . . . . . 23
2625ancld 553 . . . . . . . . . . . . . . . . . . . . . 22
2726eximdv 1710 . . . . . . . . . . . . . . . . . . . . 21
28 n0 3794 . . . . . . . . . . . . . . . . . . . . 21
29 df-rex 2813 . . . . . . . . . . . . . . . . . . . . 21
3027, 28, 293imtr4g 270 . . . . . . . . . . . . . . . . . . . 20
3130imp 429 . . . . . . . . . . . . . . . . . . 19
3231a1d 25 . . . . . . . . . . . . . . . . . 18
3332ad2antrr 725 . . . . . . . . . . . . . . . . 17
34 breq1 4455 . . . . . . . . . . . . . . . . . . 19
35 breq1 4455 . . . . . . . . . . . . . . . . . . . 20
3635rexbidv 2968 . . . . . . . . . . . . . . . . . . 19
3734, 36imbi12d 320 . . . . . . . . . . . . . . . . . 18
3837adantl 466 . . . . . . . . . . . . . . . . 17
3933, 38mpbird 232 . . . . . . . . . . . . . . . 16
4039ex 434 . . . . . . . . . . . . . . 15
4140adantr 465 . . . . . . . . . . . . . 14
4213, 22, 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 . . . . . . . . . . . . . . . 16
5554ord 377 . . . . . . . . . . . . . . 15
5653, 55sylan 471 . . . . . . . . . . . . . 14
5756an32s 804 . . . . . . . . . . . . 13
5857reximdva 2932 . . . . . . . . . . . 12
5952, 58syl5bir 218 . . . . . . . . . . 11
6059ralimdva 2865 . . . . . . . . . 10
6160imp 429 . . . . . . . . 9
6251, 61sylan2br 476 . . . . . . . 8
63 breq2 4456 . . . . . . . . . 10
6463cbvrexv 3085 . . . . . . . . 9
6564ralbii 2888 . . . . . . . 8
6662, 65sylib 196 . . . . . . 7
67 pnfxr 11350 . . . . . . . 8
68 ssel 3497 . . . . . . . . . . . 12
69 rexr 9660 . . . . . . . . . . . . 13
70 pnfnlt 11366 . . . . . . . . . . . . 13
7169, 70syl 16 . . . . . . . . . . . 12
7268, 71syl6 33 . . . . . . . . . . 11
7372ralrimiv 2869 . . . . . . . . . 10
7473adantr 465 . . . . . . . . 9
75 peano2re 9774 . . . . . . . . . . . . . . . . . . 19
76 breq1 4455 . . . . . . . . . . . . . . . . . . . . . . 23
7776rexbidv 2968 . . . . . . . . . . . . . . . . . . . . . 22
7877rspcva 3208 . . . . . . . . . . . . . . . . . . . . 21
7978adantrr 716 . . . . . . . . . . . . . . . . . . . 20
8079ancoms 453 . . . . . . . . . . . . . . . . . . 19
8175, 80sylan2 474 . . . . . . . . . . . . . . . . . 18
82 ssel2 3498 . . . . . . . . . . . . . . . . . . . . . 22
83 ltp1 10405 . . . . . . . . . . . . . . . . . . . . . . . . 25
8483adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24
8575ancli 551 . . . . . . . . . . . . . . . . . . . . . . . . 25
86 ltletr 9697 . . . . . . . . . . . . . . . . . . . . . . . . . 26
87863expa 1196 . . . . . . . . . . . . . . . . . . . . . . . . 25
8885, 87sylan 471 . . . . . . . . . . . . . . . . . . . . . . . 24
8984, 88mpand 675 . . . . . . . . . . . . . . . . . . . . . . 23
9089ancoms 453 . . . . . . . . . . . . . . . . . . . . . 22
9182, 90sylan 471 . . . . . . . . . . . . . . . . . . . . 21
9291an32s 804 . . . . . . . . . . . . . . . . . . . 20
9392reximdva 2932 . . . . . . . . . . . . . . . . . . 19
9493adantll 713 . . . . . . . . . . . . . . . . . 18
9581, 94mpd 15 . . . . . . . . . . . . . . . . 17
9695exp31 604 . . . . . . . . . . . . . . . 16
9796a1dd 46 . . . . . . . . . . . . . . 15
9897com4r 86 . . . . . . . . . . . . . 14
99 xrltnr 11359 . . . . . . . . . . . . . . . . . . 19
10067, 99ax-mp 5 . . . . . . . . . . . . . . . . . 18
101 breq1 4455 . . . . . . . . . . . . . . . . . 18
102100, 101mtbiri 303 . . . . . . . . . . . . . . . . 17
103102pm2.21d 106 . . . . . . . . . . . . . . . 16
104103a1d 25 . . . . . . . . . . . . . . 15
105104a1d 25 . . . . . . . . . . . . . 14
106 0re 9617 . . . . . . . . . . . . . . . . . . 19
107 breq1 4455 . . . . . . . . . . . . . . . . . . . . 21
108107rexbidv 2968 . . . . . . . . . . . . . . . . . . . 20
109108rspcva 3208 . . . . . . . . . . . . . . . . . . 19
110106, 109mpan 670 . . . . . . . . . . . . . . . . . 18
11182, 24syl 16 . . . . . . . . . . . . . . . . . . . 20
112111a1d 25 . . . . . . . . . . . . . . . . . . 19
113112reximdva 2932 . . . . . . . . . . . . . . . . . 18
114110, 113mpan9 469 . . . . . . . . . . . . . . . . 17
115114, 36syl5ibr 221 . . . . . . . . . . . . . . . 16
116115a1dd 46 . . . . . . . . . . . . . . 15
117116expd 436 . . . . . . . . . . . . . 14
11898, 105, 1173jaoi 1291 . . . . . . . . . . . . 13
11912, 118sylbi 195 . . . . . . . . . . . 12
120119com13 80 . . . . . . . . . . 11
121120imp 429 . . . . . . . . . 10
122121ralrimiv 2869 . . . . . . . . 9
12374, 122jca 532 . . . . . . . 8
124 breq1 4455 . . . . . . . . . . . 12
125124notbid 294 . . . . . . . . . . 11
126125ralbidv 2896 . . . . . . . . . 10
127 breq2 4456 . . . . . . . . . . . 12
128127imbi1d 317 . . . . . . . . . . 11
129128ralbidv 2896 . . . . . . . . . 10
130126, 129anbi12d 710 . . . . . . . . 9
131130rspcev 3210 . . . . . . . 8
13267, 123, 131sylancr 663 . . . . . . 7
13366, 132syldan 470 . . . . . 6
134133adantlr 714 . . . . 5
13550, 134pm2.61dan 791 . . . 4
136 mnfxr 11352 . . . . . 6
137 ral0 3934 . . . . . . 7
138 nltmnf 11367 . . . . . . . . 9
139138pm2.21d 106 . . . . . . . 8
140139rgen 2817 . . . . . . 7
141137, 140pm3.2i 455 . . . . . 6
142 breq1 4455 . . . . . . . . . 10
143142notbid 294 . . . . . . . . 9
144143ralbidv 2896 . . . . . . . 8
145 breq2 4456 . . . . . . . . . 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, 70syl6 33 . . . . 5
156155ralrimiv 2869 . . . 4
157 breq2 4456 . . . . . . 7
158157rspcev 3210 . . . . . 6
159158ex 434 . . . . 5
160159ralrimivw 2872 . . . 4
161156, 160anim12i 566 . . 3
16267, 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   caddc 9516   cpnf 9646   cmnf 9647   cxr 9648   clt 9649   cle 9650
This theorem is referenced by:  xrsupss  11529
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