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 ) → ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 ) )