lo1const

Description: A constant function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016)

		Ref	Expression
	Assertion	lo1const	$⊢ (A \subseteq ℝ \land B \in ℝ) \to (x \in A ⟼ B) \in \leq 𝑂 (1)$

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \subseteq ℝ \land B \in ℝ) \to A \subseteq ℝ$
2		simplr	$⊢ ((A \subseteq ℝ \land B \in ℝ) \land x \in A) \to B \in ℝ$
3		simpr	$⊢ (A \subseteq ℝ \land B \in ℝ) \to B \in ℝ$
4		leid	$⊢ B \in ℝ \to B \leq B$
5	4	ad2antlr	$⊢ ((A \subseteq ℝ \land B \in ℝ) \land (x \in A \land B \leq x)) \to B \leq B$
6	1 2 3 3 5	ello1d	$⊢ (A \subseteq ℝ \land B \in ℝ) \to (x \in A ⟼ B) \in \leq 𝑂 (1)$

Metamath Proof Explorer