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

Metamath Proof Explorer

Theorem elo1d

Description: Sufficient condition for elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 21-Sep-2014) (Proof shortened by Mario Carneiro, 26-May-2016)

		Ref	Expression
	Hypotheses	elo1mpt.1	$⊢ φ \to A \subseteq ℝ$
		elo1mpt.2	$⊢ (φ \land x \in A) \to B \in ℂ$
		elo1d.3	$⊢ φ \to C \in ℝ$
		elo1d.4	$⊢ φ \to M \in ℝ$
		elo1d.5	$⊢ (φ \land (x \in A \land C \leq x)) \to \|B\| \leq M$
	Assertion	elo1d	$⊢ φ \to (x \in A ⟼ B) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		elo1mpt.1	$⊢ φ \to A \subseteq ℝ$
2		elo1mpt.2	$⊢ (φ \land x \in A) \to B \in ℂ$
3		elo1d.3	$⊢ φ \to C \in ℝ$
4		elo1d.4	$⊢ φ \to M \in ℝ$
5		elo1d.5	$⊢ (φ \land (x \in A \land C \leq x)) \to \|B\| \leq M$
6	2	abscld	$⊢ (φ \land x \in A) \to \|B\| \in ℝ$
7	1 6 3 4 5	ello1d	$⊢ φ \to (x \in A ⟼ \|B\|) \in \leq 𝑂 (1)$
8	2	lo1o12	$⊢ φ \to ((x \in A ⟼ B) \in 𝑂 (1) \leftrightarrow (x \in A ⟼ \|B\|) \in \leq 𝑂 (1))$
9	7 8	mpbird	$⊢ φ \to (x \in A ⟼ B) \in 𝑂 (1)$