Metamath Proof Explorer

Theorem o1lo1

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

Ref Expression
Hypothesis o1lo1.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
Assertion o1lo1 ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ∧ ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) ) ) )

Proof

Step Hyp Ref Expression
1 o1lo1.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
2 o1dm ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
3 2 a1i ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ ) )
4 lo1dm ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
5 4 adantr ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ∧ ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) ) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
6 5 a1i ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ∧ ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) ) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ ) )
7 1 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ℝ )
8 dmmptg ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ℝ → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
9 7 8 syl ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
10 9 sseq1d ⊢ ( 𝜑 → ( dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ ↔ 𝐴 ⊆ ℝ ) )
11 simpr ⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ 𝑚 ∈ ℝ ) → 𝑚 ∈ ℝ )
12 1 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
13 12 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
14 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑚 ∈ ℝ )
15 13 14 absled ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ 𝐵 ) ≤ 𝑚 ↔ ( - 𝑚 ≤ 𝐵 ∧ 𝐵 ≤ 𝑚 ) ) )
16 ancom ⊢ ( ( - 𝑚 ≤ 𝐵 ∧ 𝐵 ≤ 𝑚 ) ↔ ( 𝐵 ≤ 𝑚 ∧ - 𝑚 ≤ 𝐵 ) )
17 lenegcon1 ⊢ ( ( 𝑚 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( - 𝑚 ≤ 𝐵 ↔ - 𝐵 ≤ 𝑚 ) )
18 14 13 17 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( - 𝑚 ≤ 𝐵 ↔ - 𝐵 ≤ 𝑚 ) )
19 18 anbi2d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐵 ≤ 𝑚 ∧ - 𝑚 ≤ 𝐵 ) ↔ ( 𝐵 ≤ 𝑚 ∧ - 𝐵 ≤ 𝑚 ) ) )
20 16 19 bitrid ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( - 𝑚 ≤ 𝐵 ∧ 𝐵 ≤ 𝑚 ) ↔ ( 𝐵 ≤ 𝑚 ∧ - 𝐵 ≤ 𝑚 ) ) )
21 15 20 bitrd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ 𝐵 ) ≤ 𝑚 ↔ ( 𝐵 ≤ 𝑚 ∧ - 𝐵 ≤ 𝑚 ) ) )
22 21 imbi2d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ↔ ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑚 ∧ - 𝐵 ≤ 𝑚 ) ) ) )
23 22 ralbidva ⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑚 ∧ - 𝐵 ≤ 𝑚 ) ) ) )
24 23 rexbidv ⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ↔ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑚 ∧ - 𝐵 ≤ 𝑚 ) ) ) )
25 24 biimpd ⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) → ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑚 ∧ - 𝐵 ≤ 𝑚 ) ) ) )
26 breq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐵 ≤ 𝑛 ↔ 𝐵 ≤ 𝑚 ) )
27 26 anbi1d ⊢ ( 𝑛 = 𝑚 → ( ( 𝐵 ≤ 𝑛 ∧ - 𝐵 ≤ 𝑝 ) ↔ ( 𝐵 ≤ 𝑚 ∧ - 𝐵 ≤ 𝑝 ) ) )
28 27 imbi2d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑛 ∧ - 𝐵 ≤ 𝑝 ) ) ↔ ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑚 ∧ - 𝐵 ≤ 𝑝 ) ) ) )
29 28 rexralbidv ⊢ ( 𝑛 = 𝑚 → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑛 ∧ - 𝐵 ≤ 𝑝 ) ) ↔ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑚 ∧ - 𝐵 ≤ 𝑝 ) ) ) )
30 breq2 ⊢ ( 𝑝 = 𝑚 → ( - 𝐵 ≤ 𝑝 ↔ - 𝐵 ≤ 𝑚 ) )
31 30 anbi2d ⊢ ( 𝑝 = 𝑚 → ( ( 𝐵 ≤ 𝑚 ∧ - 𝐵 ≤ 𝑝 ) ↔ ( 𝐵 ≤ 𝑚 ∧ - 𝐵 ≤ 𝑚 ) ) )
32 31 imbi2d ⊢ ( 𝑝 = 𝑚 → ( ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑚 ∧ - 𝐵 ≤ 𝑝 ) ) ↔ ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑚 ∧ - 𝐵 ≤ 𝑚 ) ) ) )
33 32 rexralbidv ⊢ ( 𝑝 = 𝑚 → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑚 ∧ - 𝐵 ≤ 𝑝 ) ) ↔ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑚 ∧ - 𝐵 ≤ 𝑚 ) ) ) )
34 29 33 rspc2ev ⊢ ( ( 𝑚 ∈ ℝ ∧ 𝑚 ∈ ℝ ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑚 ∧ - 𝐵 ≤ 𝑚 ) ) ) → ∃ 𝑛 ∈ ℝ ∃ 𝑝 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑛 ∧ - 𝐵 ≤ 𝑝 ) ) )
35 34 3anidm12 ⊢ ( ( 𝑚 ∈ ℝ ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑚 ∧ - 𝐵 ≤ 𝑚 ) ) ) → ∃ 𝑛 ∈ ℝ ∃ 𝑝 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑛 ∧ - 𝐵 ≤ 𝑝 ) ) )
36 11 25 35 syl6an ⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) → ∃ 𝑛 ∈ ℝ ∃ 𝑝 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑛 ∧ - 𝐵 ≤ 𝑝 ) ) ) )
37 36 rexlimdva ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( ∃ 𝑚 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) → ∃ 𝑛 ∈ ℝ ∃ 𝑝 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑛 ∧ - 𝐵 ≤ 𝑝 ) ) ) )
38 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑛 ≤ 𝑝 ) → 𝑝 ∈ ℝ )
39 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ ¬ 𝑛 ≤ 𝑝 ) → 𝑛 ∈ ℝ )
40 38 39 ifclda ⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) → if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ∈ ℝ )
41 max2 ⊢ ( ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) → 𝑝 ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) )
42 41 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑝 ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) )
43 12 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
44 43 renegcld ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 ∈ ℝ )
45 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑝 ∈ ℝ )
46 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑛 ∈ ℝ )
47 45 46 ifcld ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ∈ ℝ )
48 letr ⊢ ( ( - 𝐵 ∈ ℝ ∧ 𝑝 ∈ ℝ ∧ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ∈ ℝ ) → ( ( - 𝐵 ≤ 𝑝 ∧ 𝑝 ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ) → - 𝐵 ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ) )
49 44 45 47 48 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( - 𝐵 ≤ 𝑝 ∧ 𝑝 ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ) → - 𝐵 ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ) )
50 42 49 mpan2d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐵 ≤ 𝑝 → - 𝐵 ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ) )
51 lenegcon1 ⊢ ( ( 𝐵 ∈ ℝ ∧ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ∈ ℝ ) → ( - 𝐵 ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ↔ - if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ≤ 𝐵 ) )
52 43 47 51 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐵 ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ↔ - if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ≤ 𝐵 ) )
53 50 52 sylibd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐵 ≤ 𝑝 → - if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ≤ 𝐵 ) )
54 max1 ⊢ ( ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) → 𝑛 ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) )
55 54 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑛 ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) )
56 letr ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ∈ ℝ ) → ( ( 𝐵 ≤ 𝑛 ∧ 𝑛 ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ) → 𝐵 ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ) )
57 43 46 47 56 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐵 ≤ 𝑛 ∧ 𝑛 ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ) → 𝐵 ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ) )
58 55 57 mpan2d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ≤ 𝑛 → 𝐵 ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ) )
59 53 58 anim12d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( - 𝐵 ≤ 𝑝 ∧ 𝐵 ≤ 𝑛 ) → ( - if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ≤ 𝐵 ∧ 𝐵 ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ) ) )
60 59 ancomsd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐵 ≤ 𝑛 ∧ - 𝐵 ≤ 𝑝 ) → ( - if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ≤ 𝐵 ∧ 𝐵 ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ) ) )
61 43 47 absled ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ 𝐵 ) ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ↔ ( - if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ≤ 𝐵 ∧ 𝐵 ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ) ) )
62 60 61 sylibrd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐵 ≤ 𝑛 ∧ - 𝐵 ≤ 𝑝 ) → ( abs ‘ 𝐵 ) ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ) )
63 62 imim2d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑛 ∧ - 𝐵 ≤ 𝑝 ) ) → ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ) ) )
64 63 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑛 ∧ - 𝐵 ≤ 𝑝 ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ) ) )
65 64 reximdv ⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑛 ∧ - 𝐵 ≤ 𝑝 ) ) → ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ) ) )
66 breq2 ⊢ ( 𝑚 = if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) → ( ( abs ‘ 𝐵 ) ≤ 𝑚 ↔ ( abs ‘ 𝐵 ) ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ) )
67 66 imbi2d ⊢ ( 𝑚 = if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) → ( ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ↔ ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ) ) )
68 67 rexralbidv ⊢ ( 𝑚 = if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ↔ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ) ) )
69 68 rspcev ⊢ ( ( if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ∈ ℝ ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ if ( 𝑛 ≤ 𝑝 , 𝑝 , 𝑛 ) ) ) → ∃ 𝑚 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) )
70 40 65 69 syl6an ⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑝 ∈ ℝ ) ) → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑛 ∧ - 𝐵 ≤ 𝑝 ) ) → ∃ 𝑚 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ) )
71 70 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( ∃ 𝑛 ∈ ℝ ∃ 𝑝 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑛 ∧ - 𝐵 ≤ 𝑝 ) ) → ∃ 𝑚 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ) )
72 37 71 impbid ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( ∃ 𝑚 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ↔ ∃ 𝑛 ∈ ℝ ∃ 𝑝 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑛 ∧ - 𝐵 ≤ 𝑝 ) ) ) )
73 rexanre ⊢ ( 𝐴 ⊆ ℝ → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑛 ∧ - 𝐵 ≤ 𝑝 ) ) ↔ ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑛 ) ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → - 𝐵 ≤ 𝑝 ) ) ) )
74 73 adantl ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑛 ∧ - 𝐵 ≤ 𝑝 ) ) ↔ ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑛 ) ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → - 𝐵 ≤ 𝑝 ) ) ) )
75 74 2rexbidv ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( ∃ 𝑛 ∈ ℝ ∃ 𝑝 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑛 ∧ - 𝐵 ≤ 𝑝 ) ) ↔ ∃ 𝑛 ∈ ℝ ∃ 𝑝 ∈ ℝ ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑛 ) ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → - 𝐵 ≤ 𝑝 ) ) ) )
76 72 75 bitrd ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( ∃ 𝑚 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ↔ ∃ 𝑛 ∈ ℝ ∃ 𝑝 ∈ ℝ ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑛 ) ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → - 𝐵 ≤ 𝑝 ) ) ) )
77 reeanv ⊢ ( ∃ 𝑛 ∈ ℝ ∃ 𝑝 ∈ ℝ ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑛 ) ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → - 𝐵 ≤ 𝑝 ) ) ↔ ( ∃ 𝑛 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑛 ) ∧ ∃ 𝑝 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → - 𝐵 ≤ 𝑝 ) ) )
78 76 77 bitrdi ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( ∃ 𝑚 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ↔ ( ∃ 𝑛 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑛 ) ∧ ∃ 𝑝 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → - 𝐵 ≤ 𝑝 ) ) ) )
79 rexcom ⊢ ( ∃ 𝑐 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ↔ ∃ 𝑚 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) )
80 rexcom ⊢ ( ∃ 𝑐 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑛 ) ↔ ∃ 𝑛 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑛 ) )
81 rexcom ⊢ ( ∃ 𝑐 ∈ ℝ ∃ 𝑝 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → - 𝐵 ≤ 𝑝 ) ↔ ∃ 𝑝 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → - 𝐵 ≤ 𝑝 ) )
82 80 81 anbi12i ⊢ ( ( ∃ 𝑐 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑛 ) ∧ ∃ 𝑐 ∈ ℝ ∃ 𝑝 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → - 𝐵 ≤ 𝑝 ) ) ↔ ( ∃ 𝑛 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑛 ) ∧ ∃ 𝑝 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → - 𝐵 ≤ 𝑝 ) ) )
83 78 79 82 3bitr4g ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( ∃ 𝑐 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ↔ ( ∃ 𝑐 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑛 ) ∧ ∃ 𝑐 ∈ ℝ ∃ 𝑝 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → - 𝐵 ≤ 𝑝 ) ) ) )
84 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → 𝐴 ⊆ ℝ )
85 12 recnd ⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
86 84 85 elo1mpt ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ∃ 𝑐 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ) )
87 84 12 ello1mpt ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ↔ ∃ 𝑐 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑛 ) ) )
88 12 renegcld ⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 ∈ ℝ )
89 84 88 ello1mpt ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) ↔ ∃ 𝑐 ∈ ℝ ∃ 𝑝 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → - 𝐵 ≤ 𝑝 ) ) )
90 87 89 anbi12d ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ∧ ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) ) ↔ ( ∃ 𝑐 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑛 ) ∧ ∃ 𝑐 ∈ ℝ ∃ 𝑝 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → - 𝐵 ≤ 𝑝 ) ) ) )
91 83 86 90 3bitr4d ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ∧ ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) ) ) )
92 91 ex ⊢ ( 𝜑 → ( 𝐴 ⊆ ℝ → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ∧ ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) ) ) ) )
93 10 92 sylbid ⊢ ( 𝜑 → ( dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ∧ ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) ) ) ) )
94 3 6 93 pm5.21ndd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ∧ ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) ) ) )