Metamath Proof Explorer

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	$⊢ ((S \subseteq ℝ \land S \neq \emptyset \land \exists x \in ℝ \forall y \in S x \leq y) \land (A \in ℝ \land sup (S ℝ <) < A)) \to \exists z \in S z < A$

Proof

Step	Hyp	Ref	Expression
1		simprl	$⊢ ((S \subseteq ℝ \land S \neq \emptyset \land \exists x \in ℝ \forall y \in S x \leq y) \land (A \in ℝ \land sup (S ℝ <) < A)) \to A \in ℝ$
2		simprr	$⊢ ((S \subseteq ℝ \land S \neq \emptyset \land \exists x \in ℝ \forall y \in S x \leq y) \land (A \in ℝ \land sup (S ℝ <) < A)) \to sup (S ℝ <) < A$
3		ltso	$⊢ < Or ℝ$
4	3	a1i	$⊢ ((S \subseteq ℝ \land S \neq \emptyset \land \exists x \in ℝ \forall y \in S x \leq y) \land (A \in ℝ \land sup (S ℝ <) < A)) \to < Or ℝ$
5		infm3	$⊢ (S \subseteq ℝ \land S \neq \emptyset \land \exists x \in ℝ \forall y \in S x \leq y) \to \exists x \in ℝ (\forall y \in S \neg y < x \land \forall y \in ℝ (x < y \to \exists z \in S z < y))$
6	5	adantr	$⊢ ((S \subseteq ℝ \land S \neq \emptyset \land \exists x \in ℝ \forall y \in S x \leq y) \land (A \in ℝ \land sup (S ℝ <) < A)) \to \exists x \in ℝ (\forall y \in S \neg y < x \land \forall y \in ℝ (x < y \to \exists z \in S z < y))$
7	4 6	infglb	$⊢ ((S \subseteq ℝ \land S \neq \emptyset \land \exists x \in ℝ \forall y \in S x \leq y) \land (A \in ℝ \land sup (S ℝ <) < A)) \to ((A \in ℝ \land sup (S ℝ <) < A) \to \exists z \in S z < A)$
8	1 2 7	mp2and	$⊢ ((S \subseteq ℝ \land S \neq \emptyset \land \exists x \in ℝ \forall y \in S x \leq y) \land (A \in ℝ \land sup (S ℝ <) < A)) \to \exists z \in S z < A$