Theorem gtinf

Description: Any number greater than an infimum is greater than some element of the set. (Contributed by Jeff Hankins, 29-Sep-2013) (Revised by AV, 10-Oct-2021)

	Ref	Expression
Assertion	gtinf	⊢ ( ( ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ∧ ( 𝐴 ∈ ℝ ∧ inf ( 𝑆 , ℝ , < ) < 𝐴 ) ) → ∃ 𝑧 ∈ 𝑆 𝑧 < 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		simprl	⊢ ( ( ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ∧ ( 𝐴 ∈ ℝ ∧ inf ( 𝑆 , ℝ , < ) < 𝐴 ) ) → 𝐴 ∈ ℝ )
2		simprr	⊢ ( ( ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ∧ ( 𝐴 ∈ ℝ ∧ inf ( 𝑆 , ℝ , < ) < 𝐴 ) ) → inf ( 𝑆 , ℝ , < ) < 𝐴 )
3		ltso	⊢ < Or ℝ
4	3	a1i	⊢ ( ( ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ∧ ( 𝐴 ∈ ℝ ∧ inf ( 𝑆 , ℝ , < ) < 𝐴 ) ) → < Or ℝ )
5		infm3	⊢ ( ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝑆 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝑆 𝑧 < 𝑦 ) ) )
6	5	adantr	⊢ ( ( ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ∧ ( 𝐴 ∈ ℝ ∧ inf ( 𝑆 , ℝ , < ) < 𝐴 ) ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝑆 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝑆 𝑧 < 𝑦 ) ) )
7	4 6	infglb	⊢ ( ( ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ∧ ( 𝐴 ∈ ℝ ∧ inf ( 𝑆 , ℝ , < ) < 𝐴 ) ) → ( ( 𝐴 ∈ ℝ ∧ inf ( 𝑆 , ℝ , < ) < 𝐴 ) → ∃ 𝑧 ∈ 𝑆 𝑧 < 𝐴 ) )
8	1 2 7	mp2and	⊢ ( ( ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ∧ ( 𝐴 ∈ ℝ ∧ inf ( 𝑆 , ℝ , < ) < 𝐴 ) ) → ∃ 𝑧 ∈ 𝑆 𝑧 < 𝐴 )