Theorem prn0 6959

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

Step	Hyp	Ref	Expression
1		elnpi 6958	. . 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 1057	. . 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)
3	1, 2	sylbi 220	. 2 |- (A e. P. -> (/) C. A)
4		0pss 3092	. 2 |- ((/) C. A <-> A =/= (/))
5	3, 4	sylib 221	1 |- (A e. P. -> A =/= (/))

Syntax hints:   -> wi 3   /\ wa 418   /\ w3a 1035  A.wal 1512   e. wcel 1590   =/= wne 2213  A.wral 2305  E.wrex 2306  _Vcvv 2494   C. wpss 2796  (/)c0 3058   class class class wbr 3502  Q.cnq 6819   <Q cltq 6825  P.cnp 6826

This theorem is referenced by:  0npr 6962  npomex 6966  genpn0 6973  prlem934 7003  ltaddpr 7004  prlem936 7017  reclem2pr 7018  suplem1pr 7022

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1513  ax-6 1514  ax-7 1515  ax-gen 1516  ax-8 1592  ax-10 1593  ax-11 1594  ax-12 1595  ax-17 1604  ax-9 1615  ax-4 1621  ax-16 1798  ax-ext 2069

This theorem depends on definitions:  df-bi 210  df-or 419  df-an 420  df-3an 1037  df-ex 1518  df-sb 1760  df-clab 2075  df-cleq 2080  df-clel 2083  df-ne 2215  df-ral 2309  df-rex 2310  df-v 2496  df-dif 2798  df-in 2802  df-ss 2804  df-pss 2806  df-nul 3059  df-np 6951

Copyright terms: Public domain