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