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 ⊢ φ → M ∈ ℝ
lo1le.2 ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1
lo1le.3 ⊢ φ ∧ x ∈ A → B ∈ V
lo1le.4 ⊢ φ ∧ x ∈ A → C ∈ ℝ
lo1le.5 ⊢ φ ∧ x ∈ A ∧ M ≤ x → C ≤ B
Assertion lo1le ⊢ φ → x ∈ A ⟼ C ∈ ≤𝑂⁡1

Proof

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