Theorem prn0 8609

Description: A positive real is not empty. (Contributed by NM, 15-May-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.)

Assertion

Ref	Expression
prn0	|- ( A e. P. -> A =/= (/) )

Proof of Theorem prn0

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elnpi 8608	. . 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 959	. . 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 187	. 2 |- ( A e. P. -> (/) C. A )
4		0pss 3493	. 2 |- ( (/) C. A <-> A =/= (/) )
5	3, 4	sylib 188	1 |- ( A e. P. -> A =/= (/) )

Syntax hints:   -> wi 4   /\ wa 358   /\ w3a 934   A.wal 1527   e. wcel 1685   =/= wne 2447   A.wral 2544   E.wrex 2545   _Vcvv 2789   C. wpss 3154   (/)c0 3456   class class class wbr 4024   Q.cnq 8470   <Q cltq 8476   P.cnp 8477

This theorem is referenced by:  0npr  8612  npomex  8616  genpn0  8623  prlem934  8653  ltaddpr  8654  prlem936  8667  reclem2pr  8668  suplem1pr  8672

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-v 2791  df-dif 3156  df-in 3160  df-ss 3167  df-pss 3169  df-nul 3457  df-np 8601