Theorem taupilemrplb

Description: A set of positive reals has (in the reals) a lower bound. (Contributed by Jim Kingdon, 19-Feb-2019)

	Ref	Expression
Assertion	taupilemrplb	⊢ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( ℝ+ ∩ 𝐴 ) 𝑥 ≤ 𝑦

Proof

Step	Hyp	Ref	Expression
1		0re	⊢ 0 ∈ ℝ
2		inss1	⊢ ( ℝ+ ∩ 𝐴 ) ⊆ ℝ+
3	2	sseli	⊢ ( 𝑦 ∈ ( ℝ+ ∩ 𝐴 ) → 𝑦 ∈ ℝ+ )
4	3	rpge0d	⊢ ( 𝑦 ∈ ( ℝ+ ∩ 𝐴 ) → 0 ≤ 𝑦 )
5	4	rgen	⊢ ∀ 𝑦 ∈ ( ℝ+ ∩ 𝐴 ) 0 ≤ 𝑦
6		breq1	⊢ ( 𝑥 = 0 → ( 𝑥 ≤ 𝑦 ↔ 0 ≤ 𝑦 ) )
7	6	ralbidv	⊢ ( 𝑥 = 0 → ( ∀ 𝑦 ∈ ( ℝ+ ∩ 𝐴 ) 𝑥 ≤ 𝑦 ↔ ∀ 𝑦 ∈ ( ℝ+ ∩ 𝐴 ) 0 ≤ 𝑦 ) )
8	7	rspcev	⊢ ( ( 0 ∈ ℝ ∧ ∀ 𝑦 ∈ ( ℝ+ ∩ 𝐴 ) 0 ≤ 𝑦 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( ℝ+ ∩ 𝐴 ) 𝑥 ≤ 𝑦 )
9	1 5 8	mp2an	⊢ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( ℝ+ ∩ 𝐴 ) 𝑥 ≤ 𝑦