Metamath Proof Explorer

Theorem cncfioobd

Description: A continuous function F on an open interval ( A (,) B ) with a finite right limit R in A and a finite left limit L in B is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses cncfioobd.a ⊢ φ → A ∈ ℝ
cncfioobd.b ⊢ φ → B ∈ ℝ
cncfioobd.f ⊢ φ → F : A B ⟶cn ℂ
cncfioobd.l ⊢ φ → L ∈ F lim ℂ B
cncfioobd.r ⊢ φ → R ∈ F lim ℂ A
Assertion cncfioobd ⊢ φ → ∃ x ∈ ℝ ∀ y ∈ A B F ⁡ y ≤ x

Proof

Step Hyp Ref Expression
1 cncfioobd.a ⊢ φ → A ∈ ℝ
2 cncfioobd.b ⊢ φ → B ∈ ℝ
3 cncfioobd.f ⊢ φ → F : A B ⟶cn ℂ
4 cncfioobd.l ⊢ φ → L ∈ F lim ℂ B
5 cncfioobd.r ⊢ φ → R ∈ F lim ℂ A
6 nfv ⊢ Ⅎ z φ
7 eqid ⊢ z ∈ A B ⟼ if z = A R if z = B L F ⁡ z = z ∈ A B ⟼ if z = A R if z = B L F ⁡ z
8 6 7 1 2 3 4 5 cncfiooicc ⊢ φ → z ∈ A B ⟼ if z = A R if z = B L F ⁡ z : A B ⟶cn ℂ
9 cniccbdd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ z ∈ A B ⟼ if z = A R if z = B L F ⁡ z : A B ⟶cn ℂ → ∃ x ∈ ℝ ∀ y ∈ A B z ∈ A B ⟼ if z = A R if z = B L F ⁡ z ⁡ y ≤ x
10 1 2 8 9 syl3anc ⊢ φ → ∃ x ∈ ℝ ∀ y ∈ A B z ∈ A B ⟼ if z = A R if z = B L F ⁡ z ⁡ y ≤ x
11 nfv ⊢ Ⅎ y φ ∧ x ∈ ℝ
12 nfra1 ⊢ Ⅎ y ∀ y ∈ A B z ∈ A B ⟼ if z = A R if z = B L F ⁡ z ⁡ y ≤ x
13 11 12 nfan ⊢ Ⅎ y φ ∧ x ∈ ℝ ∧ ∀ y ∈ A B z ∈ A B ⟼ if z = A R if z = B L F ⁡ z ⁡ y ≤ x
14 simpr ⊢ φ ∧ y ∈ A B → y ∈ A B
15 cncff ⊢ F : A B ⟶cn ℂ → F : A B ⟶ ℂ
16 3 15 syl ⊢ φ → F : A B ⟶ ℂ
17 16 fdmd ⊢ φ → dom ⁡ F = A B
18 17 eqcomd ⊢ φ → A B = dom ⁡ F
19 18 adantr ⊢ φ ∧ y ∈ A B → A B = dom ⁡ F
20 14 19 eleqtrd ⊢ φ ∧ y ∈ A B → y ∈ dom ⁡ F
21 1 adantr ⊢ φ ∧ y ∈ dom ⁡ F → A ∈ ℝ
22 2 adantr ⊢ φ ∧ y ∈ dom ⁡ F → B ∈ ℝ
23 16 adantr ⊢ φ ∧ y ∈ dom ⁡ F → F : A B ⟶ ℂ
24 simpr ⊢ φ ∧ y ∈ dom ⁡ F → y ∈ dom ⁡ F
25 17 adantr ⊢ φ ∧ y ∈ dom ⁡ F → dom ⁡ F = A B
26 24 25 eleqtrd ⊢ φ ∧ y ∈ dom ⁡ F → y ∈ A B
27 21 22 23 7 26 cncfioobdlem ⊢ φ ∧ y ∈ dom ⁡ F → z ∈ A B ⟼ if z = A R if z = B L F ⁡ z ⁡ y = F ⁡ y
28 20 27 syldan ⊢ φ ∧ y ∈ A B → z ∈ A B ⟼ if z = A R if z = B L F ⁡ z ⁡ y = F ⁡ y
29 28 eqcomd ⊢ φ ∧ y ∈ A B → F ⁡ y = z ∈ A B ⟼ if z = A R if z = B L F ⁡ z ⁡ y
30 29 fveq2d ⊢ φ ∧ y ∈ A B → F ⁡ y = z ∈ A B ⟼ if z = A R if z = B L F ⁡ z ⁡ y
31 30 ad4ant14 ⊢ φ ∧ x ∈ ℝ ∧ ∀ y ∈ A B z ∈ A B ⟼ if z = A R if z = B L F ⁡ z ⁡ y ≤ x ∧ y ∈ A B → F ⁡ y = z ∈ A B ⟼ if z = A R if z = B L F ⁡ z ⁡ y
32 simplr ⊢ φ ∧ x ∈ ℝ ∧ ∀ y ∈ A B z ∈ A B ⟼ if z = A R if z = B L F ⁡ z ⁡ y ≤ x ∧ y ∈ A B → ∀ y ∈ A B z ∈ A B ⟼ if z = A R if z = B L F ⁡ z ⁡ y ≤ x
33 ioossicc ⊢ A B ⊆ A B
34 simpr ⊢ φ ∧ x ∈ ℝ ∧ ∀ y ∈ A B z ∈ A B ⟼ if z = A R if z = B L F ⁡ z ⁡ y ≤ x ∧ y ∈ A B → y ∈ A B
35 33 34 sseldi ⊢ φ ∧ x ∈ ℝ ∧ ∀ y ∈ A B z ∈ A B ⟼ if z = A R if z = B L F ⁡ z ⁡ y ≤ x ∧ y ∈ A B → y ∈ A B
36 rspa ⊢ ∀ y ∈ A B z ∈ A B ⟼ if z = A R if z = B L F ⁡ z ⁡ y ≤ x ∧ y ∈ A B → z ∈ A B ⟼ if z = A R if z = B L F ⁡ z ⁡ y ≤ x
37 32 35 36 syl2anc ⊢ φ ∧ x ∈ ℝ ∧ ∀ y ∈ A B z ∈ A B ⟼ if z = A R if z = B L F ⁡ z ⁡ y ≤ x ∧ y ∈ A B → z ∈ A B ⟼ if z = A R if z = B L F ⁡ z ⁡ y ≤ x
38 31 37 eqbrtrd ⊢ φ ∧ x ∈ ℝ ∧ ∀ y ∈ A B z ∈ A B ⟼ if z = A R if z = B L F ⁡ z ⁡ y ≤ x ∧ y ∈ A B → F ⁡ y ≤ x
39 38 ex ⊢ φ ∧ x ∈ ℝ ∧ ∀ y ∈ A B z ∈ A B ⟼ if z = A R if z = B L F ⁡ z ⁡ y ≤ x → y ∈ A B → F ⁡ y ≤ x
40 13 39 ralrimi ⊢ φ ∧ x ∈ ℝ ∧ ∀ y ∈ A B z ∈ A B ⟼ if z = A R if z = B L F ⁡ z ⁡ y ≤ x → ∀ y ∈ A B F ⁡ y ≤ x
41 40 ex ⊢ φ ∧ x ∈ ℝ → ∀ y ∈ A B z ∈ A B ⟼ if z = A R if z = B L F ⁡ z ⁡ y ≤ x → ∀ y ∈ A B F ⁡ y ≤ x
42 41 reximdva ⊢ φ → ∃ x ∈ ℝ ∀ y ∈ A B z ∈ A B ⟼ if z = A R if z = B L F ⁡ z ⁡ y ≤ x → ∃ x ∈ ℝ ∀ y ∈ A B F ⁡ y ≤ x
43 10 42 mpd ⊢ φ → ∃ x ∈ ℝ ∀ y ∈ A B F ⁡ y ≤ x