Theorem prn0 6964

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 6963	. . 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 1040	. . 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 214	. 2 |- (A e. P. -> (/) C. A)
4		0pss 3082	. 2 |- ((/) C. A <-> A =/= (/))
5	3, 4	sylib 215	1 |- (A e. P. -> A =/= (/))

Syntax hints:   -> wi 3   /\ wa 412   /\ w3a 1018  A.wal 1496   e. wcel 1575   =/= wne 2201  A.wral 2293  E.wrex 2294  _Vcvv 2482   C. wpss 2785  (/)c0 3048   class class class wbr 3492  Q.cnq 6824   <Q cltq 6830  P.cnp 6831

This theorem is referenced by:  0npr 6967  npomex 6971  genpn0 6978  prlem934 7008  ltaddpr 7009  prlem936 7022  reclem2pr 7023  suplem1pr 7027

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1497  ax-6 1498  ax-7 1499  ax-gen 1500  ax-8 1577  ax-10 1578  ax-11 1579  ax-12 1580  ax-17 1589  ax-9 1603  ax-4 1609  ax-16 1786  ax-ext 2057

This theorem depends on definitions:  df-bi 204  df-or 413  df-an 414  df-3an 1020  df-ex 1502  df-sb 1748  df-clab 2063  df-cleq 2068  df-clel 2071  df-ne 2203  df-ral 2297  df-rex 2298  df-v 2484  df-dif 2787  df-in 2791  df-ss 2793  df-pss 2795  df-nul 3049  df-np 6956

Copyright terms: Public domain