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

Theorem prnmax 9110
Description: A positive real has no largest member. Definition 9-3.1(iii) of [Gleason] p. 121. (Contributed by NM, 9-Mar-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.)
Assertion
Ref Expression
prnmax
Distinct variable groups:   ,   ,

Proof of Theorem prnmax
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eleq1 2482 . . . . 5
21anbi2d 688 . . . 4
3 breq1 4270 . . . . 5
43rexbidv 2715 . . . 4
52, 4imbi12d 314 . . 3
6 elnpi 9103 . . . . . 6
76simprbi 454 . . . . 5
87r19.21bi 2793 . . . 4
98simprd 453 . . 3
105, 9vtoclg 3008 . 2
1110anabsi7 800 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 362  /\w3a 950  A.wal 1580  =wceq 1687  e.wcel 1749  A.wral 2694  E.wrex 2695   cvv 2951  C.wpss 3306   c0 3614   class class class wbr 4267   cnq 8965   cltq 8971   cnp 8972
This theorem is referenced by:  npomex  9111  prnmadd  9112  genpnmax  9122  1idpr  9144  ltexprlem4  9154  reclem3pr  9164  suplem1pr  9167
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ne 2587  df-ral 2699  df-rex 2700  df-rab 2703  df-v 2953  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-pss 3321  df-nul 3615  df-if 3769  df-sn 3859  df-pr 3860  df-op 3862  df-br 4268  df-np 9096
  Copyright terms: Public domain W3C validator