Theorem lble

Description: If a set of reals contains a lower bound, the lower bound is less than or equal to all members of the set. (Contributed by NM, 9-Oct-2005) (Proof shortened by Mario Carneiro, 24-Dec-2016)

	Ref	Expression
Assertion	lble	⊢ ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		lbreu	⊢ ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) → ∃! 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 )
2		nfcv	⊢ Ⅎ 𝑥 𝑆
3		nfriota1	⊢ Ⅎ 𝑥 ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 )
4		nfcv	⊢ Ⅎ 𝑥 ≤
5		nfcv	⊢ Ⅎ 𝑥 𝑦
6	3 4 5	nfbr	⊢ Ⅎ 𝑥 ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝑦
7	2 6	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ 𝑆 ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝑦
8		eqid	⊢ ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) = ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 )
9		nfra1	⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦
10		nfcv	⊢ Ⅎ 𝑦 𝑆
11	9 10	nfriota	⊢ Ⅎ 𝑦 ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 )
12	11	nfeq2	⊢ Ⅎ 𝑦 𝑥 = ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 )
13		breq1	⊢ ( 𝑥 = ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) → ( 𝑥 ≤ 𝑦 ↔ ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝑦 ) )
14	12 13	ralbid	⊢ ( 𝑥 = ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) → ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ↔ ∀ 𝑦 ∈ 𝑆 ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝑦 ) )
15	7 8 14	riotaprop	⊢ ( ∃! 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 → ( ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝑦 ) )
16	1 15	syl	⊢ ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) → ( ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝑦 ) )
17	16	simprd	⊢ ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) → ∀ 𝑦 ∈ 𝑆 ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝑦 )
18		nfcv	⊢ Ⅎ 𝑦 ≤
19		nfcv	⊢ Ⅎ 𝑦 𝐴
20	11 18 19	nfbr	⊢ Ⅎ 𝑦 ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝐴
21		breq2	⊢ ( 𝑦 = 𝐴 → ( ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝑦 ↔ ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝐴 ) )
22	20 21	rspc	⊢ ( 𝐴 ∈ 𝑆 → ( ∀ 𝑦 ∈ 𝑆 ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝑦 → ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝐴 ) )
23	17 22	mpan9	⊢ ( ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ∧ 𝐴 ∈ 𝑆 ) → ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝐴 )
24	23	3impa	⊢ ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝐴 )