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

Metamath Proof Explorer

Theorem 01sqrexlem3

Description: Lemma for 01sqrex . (Contributed by Mario Carneiro, 10-Jul-2013)

Ref Expression
Hypotheses 01sqrexlem1.1 ⊢ 𝑆 = { 𝑥 ∈ ℝ+ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 }
01sqrexlem1.2 ⊢ 𝐵 = sup ( 𝑆 , ℝ , < )
Assertion 01sqrexlem3 ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 ) )

Proof

Step Hyp Ref Expression
1 01sqrexlem1.1 ⊢ 𝑆 = { 𝑥 ∈ ℝ+ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 }
2 01sqrexlem1.2 ⊢ 𝐵 = sup ( 𝑆 , ℝ , < )
3 ssrab2 ⊢ { 𝑥 ∈ ℝ+ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 } ⊆ ℝ+
4 rpssre ⊢ ℝ+ ⊆ ℝ
5 3 4 sstri ⊢ { 𝑥 ∈ ℝ+ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 } ⊆ ℝ
6 1 5 eqsstri ⊢ 𝑆 ⊆ ℝ
7 6 a1i ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → 𝑆 ⊆ ℝ )
8 1 2 01sqrexlem2 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → 𝐴 ∈ 𝑆 )
9 8 ne0d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → 𝑆 ≠ ∅ )
10 1re ⊢ 1 ∈ ℝ
11 1 2 01sqrexlem1 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 1 )
12 brralrspcev ⊢ ( ( 1 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 1 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 )
13 10 11 12 sylancr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 )
14 7 9 13 3jca ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 ) )