HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem prn0 6981
Description: A positive real is not empty. (Revised by Mario Carneiro, 11-May-2013.)
Assertion
Ref Expression
prn0 |- (A e. P. -> A =/= (/))

Proof of Theorem prn0
StepHypRef Expression
1 elnpi 6980 . . 3 |- (A e. P. <-> ((A e. _V /\ (/) C. A /\ A C. Q.) /\ A.x e. A (A.y(y <Q x -> y e. A) /\ E.y e. A x <Q y)))
2 simpl2 1059 . . 3 |- (((A e. _V /\ (/) C. A /\ A C. Q.) /\ A.x e. A (A.y(y <Q x -> y e. A) /\ E.y e. A x <Q y)) -> (/) C. A)
31, 2sylbi 220 . 2 |- (A e. P. -> (/) C. A)
4 0pss 3099 . 2 |- ((/) C. A <-> A =/= (/))
53, 4sylib 221 1 |- (A e. P. -> A =/= (/))
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 418   /\ w3a 1037  A.wal 1515   e. wcel 1594   =/= wne 2218  A.wral 2310  E.wrex 2311  _Vcvv 2499   C. wpss 2802  (/)c0 3065   class class class wbr 3509  Q.cnq 6841   <Q cltq 6847  P.cnp 6848
This theorem is referenced by:  0npr 6984  npomex 6988  genpn0 6995  prlem934 7025  ltaddpr 7026  prlem936 7039  reclem2pr 7040  suplem1pr 7044
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1516  ax-6 1517  ax-7 1518  ax-gen 1519  ax-8 1596  ax-10 1597  ax-11 1598  ax-12 1599  ax-17 1608  ax-9 1620  ax-4 1626  ax-16 1803  ax-ext 2074
This theorem depends on definitions:  df-bi 210  df-or 419  df-an 420  df-3an 1039  df-ex 1521  df-sb 1765  df-clab 2080  df-cleq 2085  df-clel 2088  df-ne 2220  df-ral 2314  df-rex 2315  df-v 2501  df-dif 2804  df-in 2808  df-ss 2810  df-pss 2812  df-nul 3066  df-np 6973
Copyright terms: Public domain