This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem infssuzle

Description: The infimum of a subset of an upper set of integers is less than or equal to all members of the subset. (Contributed by NM, 11-Oct-2005) (Revised by AV, 5-Sep-2020)

		Ref	Expression
	Assertion	infssuzle	$⊢ (S \subseteq ℤ_{\geq M} \land A \in S) \to inf (S ℝ <) \leq A$

Proof

Step	Hyp	Ref	Expression
1		ne0i	$⊢ A \in S \to S \neq \emptyset$
2		uzwo	$⊢ (S \subseteq ℤ_{\geq M} \land S \neq \emptyset) \to \exists j \in S \forall k \in S j \leq k$
3	1 2	sylan2	$⊢ (S \subseteq ℤ_{\geq M} \land A \in S) \to \exists j \in S \forall k \in S j \leq k$
4		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
5		zssre	$⊢ ℤ \subseteq ℝ$
6	4 5	sstri	$⊢ ℤ_{\geq M} \subseteq ℝ$
7		sstr	$⊢ (S \subseteq ℤ_{\geq M} \land ℤ_{\geq M} \subseteq ℝ) \to S \subseteq ℝ$
8	6 7	mpan2	$⊢ S \subseteq ℤ_{\geq M} \to S \subseteq ℝ$
9		lbinfle	$⊢ (S \subseteq ℝ \land \exists j \in S \forall k \in S j \leq k \land A \in S) \to inf (S ℝ <) \leq A$
10	9	3com23	$⊢ (S \subseteq ℝ \land A \in S \land \exists j \in S \forall k \in S j \leq k) \to inf (S ℝ <) \leq A$
11	8 10	syl3an1	$⊢ (S \subseteq ℤ_{\geq M} \land A \in S \land \exists j \in S \forall k \in S j \leq k) \to inf (S ℝ <) \leq A$
12	3 11	mpd3an3	$⊢ (S \subseteq ℤ_{\geq M} \land A \in S) \to inf (S ℝ <) \leq A$