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:AB⟶cnℂ
cncfioobd.l ⊢φ→L∈FlimℂB
cncfioobd.r ⊢φ→R∈FlimℂA
Assertion cncfioobd ⊢φ→∃x∈ℝ∀y∈ABF⁡y≤x

Proof

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