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