Metamath Proof Explorer

Theorem o1lo12

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

Ref Expression
Hypotheses o1lo1.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
o1lo12.2 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
o1lo12.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑀 ≤ 𝐵 )
Assertion o1lo12 ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ) )

Proof

Step Hyp Ref Expression
1 o1lo1.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
2 o1lo12.2 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
3 o1lo12.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑀 ≤ 𝐵 )
4 o1dm ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
5 4 a1i ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ ) )
6 lo1dm ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
7 6 a1i ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ ) )
8 1 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ℝ )
9 dmmptg ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ℝ → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
10 8 9 syl ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
11 10 sseq1d ⊢ ( 𝜑 → ( dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ ↔ 𝐴 ⊆ ℝ ) )
12 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → 𝐴 ⊆ ℝ )
13 1 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 ∈ ℝ )
14 13 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 ∈ ℝ )
15 2 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → 𝑀 ∈ ℝ )
16 15 renegcld ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → - 𝑀 ∈ ℝ )
17 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑀 ∈ ℝ )
18 17 1 lenegd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑀 ≤ 𝐵 ↔ - 𝐵 ≤ - 𝑀 ) )
19 3 18 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 ≤ - 𝑀 )
20 19 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥 ) ) → - 𝐵 ≤ - 𝑀 )
21 12 14 15 16 20 ello1d ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) )
22 1 o1lo1 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ∧ ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) ) ) )
23 22 rbaibd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ) )
24 21 23 syldan ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ) )
25 24 ex ⊢ ( 𝜑 → ( 𝐴 ⊆ ℝ → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ) ) )
26 11 25 sylbid ⊢ ( 𝜑 → ( dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ) ) )
27 5 7 26 pm5.21ndd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ) )