Theorem prn0 6982

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 6981	. . 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 920	. . 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 184	. 2 |- (A e. P. -> (/) C. A)
4		0pss 2935	. 2 |- ((/) C. A <-> A =/= (/))
5	3, 4	sylib 185	1 |- (A e. P. -> A =/= (/))

Syntax hints:   -> wi 4   /\ wa 356   /\ w3a 898  A.wal 1329   e. wcel 1415   =/= wne 2034  A.wral 2125  E.wrex 2126  _Vcvv 2322   C. wpss 2633  (/)c0 2898   class class class wbr 3358  Q.cnq 6842   <Q cltq 6848  P.cnp 6849

This theorem is referenced by:  0npr 6985  npomex 6989  genpn0 6996  prlem934 7026  ltaddpr 7027  prlem936 7040  reclem2pr 7041  suplem1pr 7045

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1330  ax-6 1331  ax-7 1332  ax-gen 1333  ax-8 1417  ax-10 1418  ax-11 1419  ax-12 1420  ax-17 1429  ax-9 1444  ax-4 1450  ax-16 1628  ax-ext 1899

This theorem depends on definitions:  df-bi 174  df-or 357  df-an 358  df-3an 900  df-ex 1335  df-sb 1590  df-clab 1905  df-cleq 1910  df-clel 1913  df-ne 2036  df-ral 2129  df-rex 2130  df-v 2324  df-dif 2635  df-in 2639  df-ss 2641  df-pss 2643  df-nul 2899  df-np 6974

Copyright terms: Public domain