This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 → 𝐴 ≠ ∅ )