Theorem ello1d

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

	Ref	Expression
Hypotheses	ello1mpt.1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	ello1mpt.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
	ello1d.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	ello1d.4	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
	ello1d.5	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝑥 ) ) → 𝐵 ≤ 𝑀 )
Assertion	ello1d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) )

Proof

Step	Hyp	Ref	Expression
1		ello1mpt.1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		ello1mpt.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
3		ello1d.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4		ello1d.4	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
5		ello1d.5	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝑥 ) ) → 𝐵 ≤ 𝑀 )
6	5	expr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 ≤ 𝑥 → 𝐵 ≤ 𝑀 ) )
7	6	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → 𝐵 ≤ 𝑀 ) )
8		breq1	⊢ ( 𝑦 = 𝐶 → ( 𝑦 ≤ 𝑥 ↔ 𝐶 ≤ 𝑥 ) )
9	8	imbi1d	⊢ ( 𝑦 = 𝐶 → ( ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ↔ ( 𝐶 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ) )
10	9	ralbidv	⊢ ( 𝑦 = 𝐶 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ) )
11		breq2	⊢ ( 𝑚 = 𝑀 → ( 𝐵 ≤ 𝑚 ↔ 𝐵 ≤ 𝑀 ) )
12	11	imbi2d	⊢ ( 𝑚 = 𝑀 → ( ( 𝐶 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ↔ ( 𝐶 ≤ 𝑥 → 𝐵 ≤ 𝑀 ) ) )
13	12	ralbidv	⊢ ( 𝑚 = 𝑀 → ( ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → 𝐵 ≤ 𝑀 ) ) )
14	10 13	rspc2ev	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → 𝐵 ≤ 𝑀 ) ) → ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) )
15	3 4 7 14	syl3anc	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) )
16	1 2	ello1mpt	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ) )
17	15 16	mpbird	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) )