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

Theorem suplem1pr 9477
 Description: The union of a nonempty, bounded set of positive reals is a positive real. Part of Proposition 9-3.3 of [Gleason] p. 122. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
Assertion
Ref Expression
suplem1pr
Distinct variable group:   ,,

Proof of Theorem suplem1pr
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ltrelpr 9423 . . . . . . . . 9
21brel 4883 . . . . . . . 8
32simpld 461 . . . . . . 7
43ralimi 2781 . . . . . 6
5 dfss3 3422 . . . . . 6
64, 5sylibr 216 . . . . 5
76rexlimivw 2876 . . . 4
9 n0 3741 . . . . 5
10 ssel 3426 . . . . . . 7
11 prn0 9414 . . . . . . . . . 10
12 0pss 3802 . . . . . . . . . 10
1311, 12sylibr 216 . . . . . . . . 9
14 elssuni 4227 . . . . . . . . 9
15 psssstr 3539 . . . . . . . . 9
1613, 14, 15syl2an 480 . . . . . . . 8
1716expcom 437 . . . . . . 7
1810, 17sylcom 30 . . . . . 6
1918exlimdv 1779 . . . . 5
209, 19syl5bi 221 . . . 4
21 prpssnq 9415 . . . . . . 7
2221adantl 468 . . . . . 6
23 ltprord 9455 . . . . . . . . . 10
24 pssss 3528 . . . . . . . . . 10
2523, 24syl6bi 232 . . . . . . . . 9
262, 25mpcom 37 . . . . . . . 8
2726ralimi 2781 . . . . . . 7
28 unissb 4229 . . . . . . 7
2927, 28sylibr 216 . . . . . 6
30 sspsstr 3538 . . . . . . 7
3130expcom 437 . . . . . 6
3222, 29, 31syl2im 39 . . . . 5
3332rexlimdva 2879 . . . 4
3420, 33anim12d 566 . . 3
358, 34mpcom 37 . 2
36 prcdnq 9418 . . . . . . . . . . . . 13
3736ex 436 . . . . . . . . . . . 12
3837com3r 82 . . . . . . . . . . 11
3910, 38sylan9 663 . . . . . . . . . 10
4039reximdvai 2859 . . . . . . . . 9
41 eluni2 4202 . . . . . . . . 9
42 eluni2 4202 . . . . . . . . 9
4340, 41, 423imtr4g 274 . . . . . . . 8
4443ex 436 . . . . . . 7
4544com23 81 . . . . . 6
4645alrimdv 1775 . . . . 5
47 eluni 4201 . . . . . 6
48 prnmax 9420 . . . . . . . . . . . . 13
4948ex 436 . . . . . . . . . . . 12
5010, 49syl6 34 . . . . . . . . . . 11
5150com23 81 . . . . . . . . . 10
5251imp 431 . . . . . . . . 9
53 ssrexv 3494 . . . . . . . . . 10
5414, 53syl 17 . . . . . . . . 9
5552, 54sylcom 30 . . . . . . . 8
5655expimpd 608 . . . . . . 7
5756exlimdv 1779 . . . . . 6
5847, 57syl5bi 221 . . . . 5
5946, 58jcad 536 . . . 4
6059ralrimiv 2800 . . 3
618, 60syl 17 . 2
62 elnp 9412 . 2
6335, 61, 62sylanbrc 670 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 371  wal 1442  wex 1663   wcel 1887   wne 2622  wral 2737  wrex 2738   wss 3404   wpss 3405  c0 3731  cuni 4198   class class class wbr 4402  cnq 9277   cltq 9283  cnp 9284   cltp 9288 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-inf2 8146 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-tr 4498  df-eprel 4745  df-po 4755  df-so 4756  df-fr 4793  df-we 4795  df-xp 4840  df-rel 4841  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-om 6693  df-ni 9297  df-nq 9337  df-ltnq 9343  df-np 9406  df-ltp 9410 This theorem is referenced by:  supexpr  9479
 Copyright terms: Public domain W3C validator