Metamath Proof Explorer


Theorem lo1le

Description: Transfer eventual upper boundedness from a larger function to a smaller function. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses lo1le.1 ( 𝜑𝑀 ∈ ℝ )
lo1le.2 ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ ≤𝑂(1) )
lo1le.3 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
lo1le.4 ( ( 𝜑𝑥𝐴 ) → 𝐶 ∈ ℝ )
lo1le.5 ( ( 𝜑 ∧ ( 𝑥𝐴𝑀𝑥 ) ) → 𝐶𝐵 )
Assertion lo1le ( 𝜑 → ( 𝑥𝐴𝐶 ) ∈ ≤𝑂(1) )

Proof

Step Hyp Ref Expression
1 lo1le.1 ( 𝜑𝑀 ∈ ℝ )
2 lo1le.2 ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ ≤𝑂(1) )
3 lo1le.3 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
4 lo1le.4 ( ( 𝜑𝑥𝐴 ) → 𝐶 ∈ ℝ )
5 lo1le.5 ( ( 𝜑 ∧ ( 𝑥𝐴𝑀𝑥 ) ) → 𝐶𝐵 )
6 simpr ( ( 𝜑𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
7 1 adantr ( ( 𝜑𝑦 ∈ ℝ ) → 𝑀 ∈ ℝ )
8 6 7 ifcld ( ( 𝜑𝑦 ∈ ℝ ) → if ( 𝑀𝑦 , 𝑦 , 𝑀 ) ∈ ℝ )
9 1 ad2antrr ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥𝐴 ) ) → 𝑀 ∈ ℝ )
10 simplr ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥𝐴 ) ) → 𝑦 ∈ ℝ )
11 3 ralrimiva ( 𝜑 → ∀ 𝑥𝐴 𝐵𝑉 )
12 dmmptg ( ∀ 𝑥𝐴 𝐵𝑉 → dom ( 𝑥𝐴𝐵 ) = 𝐴 )
13 11 12 syl ( 𝜑 → dom ( 𝑥𝐴𝐵 ) = 𝐴 )
14 lo1dm ( ( 𝑥𝐴𝐵 ) ∈ ≤𝑂(1) → dom ( 𝑥𝐴𝐵 ) ⊆ ℝ )
15 2 14 syl ( 𝜑 → dom ( 𝑥𝐴𝐵 ) ⊆ ℝ )
16 13 15 eqsstrrd ( 𝜑𝐴 ⊆ ℝ )
17 16 ad2antrr ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥𝐴 ) ) → 𝐴 ⊆ ℝ )
18 simprr ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥𝐴 ) ) → 𝑥𝐴 )
19 17 18 sseldd ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥𝐴 ) ) → 𝑥 ∈ ℝ )
20 maxle ( ( 𝑀 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( if ( 𝑀𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 ↔ ( 𝑀𝑥𝑦𝑥 ) ) )
21 9 10 19 20 syl3anc ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥𝐴 ) ) → ( if ( 𝑀𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 ↔ ( 𝑀𝑥𝑦𝑥 ) ) )
22 simpr ( ( 𝑀𝑥𝑦𝑥 ) → 𝑦𝑥 )
23 21 22 syl6bi ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥𝐴 ) ) → ( if ( 𝑀𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥𝑦𝑥 ) )
24 23 imim1d ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥𝐴 ) ) → ( ( 𝑦𝑥𝐵𝑚 ) → ( if ( 𝑀𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥𝐵𝑚 ) ) )
25 5 adantlr ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ( 𝑥𝐴𝑀𝑥 ) ) → 𝐶𝐵 )
26 25 adantrll ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ( ( 𝑚 ∈ ℝ ∧ 𝑥𝐴 ) ∧ 𝑀𝑥 ) ) → 𝐶𝐵 )
27 simpl ( ( 𝜑𝑦 ∈ ℝ ) → 𝜑 )
28 simplr ( ( ( 𝑚 ∈ ℝ ∧ 𝑥𝐴 ) ∧ 𝑀𝑥 ) → 𝑥𝐴 )
29 27 28 4 syl2an ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ( ( 𝑚 ∈ ℝ ∧ 𝑥𝐴 ) ∧ 𝑀𝑥 ) ) → 𝐶 ∈ ℝ )
30 3 2 lo1mptrcl ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ )
31 27 28 30 syl2an ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ( ( 𝑚 ∈ ℝ ∧ 𝑥𝐴 ) ∧ 𝑀𝑥 ) ) → 𝐵 ∈ ℝ )
32 simprll ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ( ( 𝑚 ∈ ℝ ∧ 𝑥𝐴 ) ∧ 𝑀𝑥 ) ) → 𝑚 ∈ ℝ )
33 letr ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑚 ∈ ℝ ) → ( ( 𝐶𝐵𝐵𝑚 ) → 𝐶𝑚 ) )
34 29 31 32 33 syl3anc ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ( ( 𝑚 ∈ ℝ ∧ 𝑥𝐴 ) ∧ 𝑀𝑥 ) ) → ( ( 𝐶𝐵𝐵𝑚 ) → 𝐶𝑚 ) )
35 26 34 mpand ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ( ( 𝑚 ∈ ℝ ∧ 𝑥𝐴 ) ∧ 𝑀𝑥 ) ) → ( 𝐵𝑚𝐶𝑚 ) )
36 35 expr ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥𝐴 ) ) → ( 𝑀𝑥 → ( 𝐵𝑚𝐶𝑚 ) ) )
37 36 adantrd ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥𝐴 ) ) → ( ( 𝑀𝑥𝑦𝑥 ) → ( 𝐵𝑚𝐶𝑚 ) ) )
38 21 37 sylbid ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥𝐴 ) ) → ( if ( 𝑀𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 → ( 𝐵𝑚𝐶𝑚 ) ) )
39 38 a2d ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥𝐴 ) ) → ( ( if ( 𝑀𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥𝐵𝑚 ) → ( if ( 𝑀𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥𝐶𝑚 ) ) )
40 24 39 syld ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥𝐴 ) ) → ( ( 𝑦𝑥𝐵𝑚 ) → ( if ( 𝑀𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥𝐶𝑚 ) ) )
41 40 anassrs ( ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑥𝐴 ) → ( ( 𝑦𝑥𝐵𝑚 ) → ( if ( 𝑀𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥𝐶𝑚 ) ) )
42 41 ralimdva ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ∀ 𝑥𝐴 ( 𝑦𝑥𝐵𝑚 ) → ∀ 𝑥𝐴 ( if ( 𝑀𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥𝐶𝑚 ) ) )
43 42 reximdva ( ( 𝜑𝑦 ∈ ℝ ) → ( ∃ 𝑚 ∈ ℝ ∀ 𝑥𝐴 ( 𝑦𝑥𝐵𝑚 ) → ∃ 𝑚 ∈ ℝ ∀ 𝑥𝐴 ( if ( 𝑀𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥𝐶𝑚 ) ) )
44 breq1 ( 𝑧 = if ( 𝑀𝑦 , 𝑦 , 𝑀 ) → ( 𝑧𝑥 ↔ if ( 𝑀𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 ) )
45 44 imbi1d ( 𝑧 = if ( 𝑀𝑦 , 𝑦 , 𝑀 ) → ( ( 𝑧𝑥𝐶𝑚 ) ↔ ( if ( 𝑀𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥𝐶𝑚 ) ) )
46 45 rexralbidv ( 𝑧 = if ( 𝑀𝑦 , 𝑦 , 𝑀 ) → ( ∃ 𝑚 ∈ ℝ ∀ 𝑥𝐴 ( 𝑧𝑥𝐶𝑚 ) ↔ ∃ 𝑚 ∈ ℝ ∀ 𝑥𝐴 ( if ( 𝑀𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥𝐶𝑚 ) ) )
47 46 rspcev ( ( if ( 𝑀𝑦 , 𝑦 , 𝑀 ) ∈ ℝ ∧ ∃ 𝑚 ∈ ℝ ∀ 𝑥𝐴 ( if ( 𝑀𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥𝐶𝑚 ) ) → ∃ 𝑧 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥𝐴 ( 𝑧𝑥𝐶𝑚 ) )
48 8 43 47 syl6an ( ( 𝜑𝑦 ∈ ℝ ) → ( ∃ 𝑚 ∈ ℝ ∀ 𝑥𝐴 ( 𝑦𝑥𝐵𝑚 ) → ∃ 𝑧 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥𝐴 ( 𝑧𝑥𝐶𝑚 ) ) )
49 48 rexlimdva ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥𝐴 ( 𝑦𝑥𝐵𝑚 ) → ∃ 𝑧 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥𝐴 ( 𝑧𝑥𝐶𝑚 ) ) )
50 16 30 ello1mpt ( 𝜑 → ( ( 𝑥𝐴𝐵 ) ∈ ≤𝑂(1) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥𝐴 ( 𝑦𝑥𝐵𝑚 ) ) )
51 16 4 ello1mpt ( 𝜑 → ( ( 𝑥𝐴𝐶 ) ∈ ≤𝑂(1) ↔ ∃ 𝑧 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥𝐴 ( 𝑧𝑥𝐶𝑚 ) ) )
52 49 50 51 3imtr4d ( 𝜑 → ( ( 𝑥𝐴𝐵 ) ∈ ≤𝑂(1) → ( 𝑥𝐴𝐶 ) ∈ ≤𝑂(1) ) )
53 2 52 mpd ( 𝜑 → ( 𝑥𝐴𝐶 ) ∈ ≤𝑂(1) )