Theorem prn0 8078

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

Step	Hyp	Ref	Expression
1		elnpi 8077	. . 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 924	. . 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 185	. 2 |- ( A e. P. -> (/) C. A )
4		0pss 3147	. 2 |- ( (/) C. A <-> A =/= (/) )
5	3, 4	sylib 186	1 |- ( A e. P. -> A =/= (/) )

Syntax hints:   -> wi 4   /\ wa 356   /\ w3a 900   A.wal 1451   e. wcel 1533   =/= wne 2218   A.wral 2311   E.wrex 2312   _Vcvv 2512   C. wpss 2831   (/)c0 3110   class class class wbr 3630   Q.cnq 7939   <Q cltq 7945   P.cnp 7946

This theorem is referenced by:  0npr  8081  npomex  8085  genpn0  8092  prlem934  8122  ltaddpr  8123  prlem936  8136  reclem2pr  8137  suplem1pr  8141

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1452  ax-6 1453  ax-7 1454  ax-gen 1455  ax-8 1535  ax-11 1536  ax-17 1540  ax-12o 1574  ax-10 1588  ax-9 1594  ax-4 1601  ax-16 1787  ax-ext 2082

This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3an 902  df-ex 1457  df-sb 1748  df-clab 2088  df-cleq 2093  df-clel 2096  df-ne 2220  df-ral 2315  df-rex 2316  df-v 2514  df-dif 2833  df-in 2837  df-ss 2841  df-pss 2843  df-nul 3111  df-np 8070