Theorem ello1mpt2

Description: 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	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
Assertion	ello1mpt2	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ↔ ∃ 𝑦 ∈ ( 𝐶 [,) +∞ ) ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ello1mpt.1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		ello1mpt.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
3		ello1d.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4	1 2	ello1mpt	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ) )
5		rexico	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐶 ∈ ℝ ) → ( ∃ 𝑦 ∈ ( 𝐶 [,) +∞ ) ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ) )
6	1 3 5	syl2anc	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 𝐶 [,) +∞ ) ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ) )
7	6	rexbidv	⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ℝ ∃ 𝑦 ∈ ( 𝐶 [,) +∞ ) ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ↔ ∃ 𝑚 ∈ ℝ ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ) )
8		rexcom	⊢ ( ∃ 𝑦 ∈ ( 𝐶 [,) +∞ ) ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ↔ ∃ 𝑚 ∈ ℝ ∃ 𝑦 ∈ ( 𝐶 [,) +∞ ) ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) )
9		rexcom	⊢ ( ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ↔ ∃ 𝑚 ∈ ℝ ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) )
10	7 8 9	3bitr4g	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 𝐶 [,) +∞ ) ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ) )
11	4 10	bitr4d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ↔ ∃ 𝑦 ∈ ( 𝐶 [,) +∞ ) ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ) )