Metamath Proof Explorer


Theorem prn0

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

Ref Expression
Assertion prn0 ( 𝐴P𝐴 ≠ ∅ )

Proof

Step Hyp Ref Expression
1 elnpi ( 𝐴P ↔ ( ( 𝐴 ∈ V ∧ ∅ ⊊ 𝐴𝐴Q ) ∧ ∀ 𝑥𝐴 ( ∀ 𝑦 ( 𝑦 <Q 𝑥𝑦𝐴 ) ∧ ∃ 𝑦𝐴 𝑥 <Q 𝑦 ) ) )
2 simpl2 ( ( ( 𝐴 ∈ V ∧ ∅ ⊊ 𝐴𝐴Q ) ∧ ∀ 𝑥𝐴 ( ∀ 𝑦 ( 𝑦 <Q 𝑥𝑦𝐴 ) ∧ ∃ 𝑦𝐴 𝑥 <Q 𝑦 ) ) → ∅ ⊊ 𝐴 )
3 1 2 sylbi ( 𝐴P → ∅ ⊊ 𝐴 )
4 0pss ( ∅ ⊊ 𝐴𝐴 ≠ ∅ )
5 3 4 sylib ( 𝐴P𝐴 ≠ ∅ )