infrelb

Description: If a nonempty set of real numbers has a lower bound, its infimum is less than or equal to any of its elements. (Contributed by Jeff Hankins, 15-Sep-2013) (Revised by AV, 4-Sep-2020)

		Ref	Expression
	Assertion	infrelb	⊢ ( ( 𝐵 ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 ∧ 𝐴 ∈ 𝐵 ) → inf ( 𝐵 , ℝ , < ) ≤ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐵 ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 ∧ 𝐴 ∈ 𝐵 ) → 𝐵 ⊆ ℝ )
2		ne0i	⊢ ( 𝐴 ∈ 𝐵 → 𝐵 ≠ ∅ )
3	2	3ad2ant3	⊢ ( ( 𝐵 ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 ∧ 𝐴 ∈ 𝐵 ) → 𝐵 ≠ ∅ )
4		simp2	⊢ ( ( 𝐵 ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 ∧ 𝐴 ∈ 𝐵 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 )
5		infrecl	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 ) → inf ( 𝐵 , ℝ , < ) ∈ ℝ )
6	1 3 4 5	syl3anc	⊢ ( ( 𝐵 ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 ∧ 𝐴 ∈ 𝐵 ) → inf ( 𝐵 , ℝ , < ) ∈ ℝ )
7		ssel2	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ ℝ )
8	7	3adant2	⊢ ( ( 𝐵 ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ ℝ )
9		ltso	⊢ < Or ℝ
10	9	a1i	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 ) ∧ 𝐴 ∈ 𝐵 ) → < Or ℝ )
11		simpll	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 ) ∧ 𝐴 ∈ 𝐵 ) → 𝐵 ⊆ ℝ )
12	2	adantl	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 ) ∧ 𝐴 ∈ 𝐵 ) → 𝐵 ≠ ∅ )
13		simplr	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 ) ∧ 𝐴 ∈ 𝐵 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 )
14		infm3	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 < 𝑦 ) ) )
15	11 12 13 14	syl3anc	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 ) ∧ 𝐴 ∈ 𝐵 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 < 𝑦 ) ) )
16	10 15	inflb	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 ∈ 𝐵 → ¬ 𝐴 < inf ( 𝐵 , ℝ , < ) ) )
17	16	expcom	⊢ ( 𝐴 ∈ 𝐵 → ( ( 𝐵 ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 ) → ( 𝐴 ∈ 𝐵 → ¬ 𝐴 < inf ( 𝐵 , ℝ , < ) ) ) )
18	17	pm2.43b	⊢ ( ( 𝐵 ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 ) → ( 𝐴 ∈ 𝐵 → ¬ 𝐴 < inf ( 𝐵 , ℝ , < ) ) )
19	18	3impia	⊢ ( ( 𝐵 ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 ∧ 𝐴 ∈ 𝐵 ) → ¬ 𝐴 < inf ( 𝐵 , ℝ , < ) )
20	6 8 19	nltled	⊢ ( ( 𝐵 ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 ∧ 𝐴 ∈ 𝐵 ) → inf ( 𝐵 , ℝ , < ) ≤ 𝐴 )

Metamath Proof Explorer

Theorem infrelb

Proof