Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  supicc Structured version   Visualization version   GIF version

Theorem supicc 12484
 Description: Supremum of a bounded set of real numbers. (Contributed by Thierry Arnoux, 17-May-2019.)
Hypotheses
Ref Expression
supicc.1 (𝜑𝐵 ∈ ℝ)
supicc.2 (𝜑𝐶 ∈ ℝ)
supicc.3 (𝜑𝐴 ⊆ (𝐵[,]𝐶))
supicc.4 (𝜑𝐴 ≠ ∅)
Assertion
Ref Expression
supicc (𝜑 → sup(𝐴, ℝ, < ) ∈ (𝐵[,]𝐶))

Proof of Theorem supicc
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 supicc.3 . . . 4 (𝜑𝐴 ⊆ (𝐵[,]𝐶))
2 supicc.1 . . . . 5 (𝜑𝐵 ∈ ℝ)
3 supicc.2 . . . . 5 (𝜑𝐶 ∈ ℝ)
4 iccssre 12419 . . . . 5 ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵[,]𝐶) ⊆ ℝ)
52, 3, 4syl2anc 696 . . . 4 (𝜑 → (𝐵[,]𝐶) ⊆ ℝ)
61, 5sstrd 3742 . . 3 (𝜑𝐴 ⊆ ℝ)
7 supicc.4 . . 3 (𝜑𝐴 ≠ ∅)
82adantr 472 . . . . . . 7 ((𝜑𝑥𝐴) → 𝐵 ∈ ℝ)
98rexrd 10252 . . . . . 6 ((𝜑𝑥𝐴) → 𝐵 ∈ ℝ*)
103adantr 472 . . . . . . 7 ((𝜑𝑥𝐴) → 𝐶 ∈ ℝ)
1110rexrd 10252 . . . . . 6 ((𝜑𝑥𝐴) → 𝐶 ∈ ℝ*)
121sselda 3732 . . . . . 6 ((𝜑𝑥𝐴) → 𝑥 ∈ (𝐵[,]𝐶))
13 iccleub 12393 . . . . . 6 ((𝐵 ∈ ℝ*𝐶 ∈ ℝ*𝑥 ∈ (𝐵[,]𝐶)) → 𝑥𝐶)
149, 11, 12, 13syl3anc 1463 . . . . 5 ((𝜑𝑥𝐴) → 𝑥𝐶)
1514ralrimiva 3092 . . . 4 (𝜑 → ∀𝑥𝐴 𝑥𝐶)
16 breq2 4796 . . . . . 6 (𝑦 = 𝐶 → (𝑥𝑦𝑥𝐶))
1716ralbidv 3112 . . . . 5 (𝑦 = 𝐶 → (∀𝑥𝐴 𝑥𝑦 ↔ ∀𝑥𝐴 𝑥𝐶))
1817rspcev 3437 . . . 4 ((𝐶 ∈ ℝ ∧ ∀𝑥𝐴 𝑥𝐶) → ∃𝑦 ∈ ℝ ∀𝑥𝐴 𝑥𝑦)
193, 15, 18syl2anc 696 . . 3 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥𝐴 𝑥𝑦)
20 suprcl 11146 . . 3 ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑥𝐴 𝑥𝑦) → sup(𝐴, ℝ, < ) ∈ ℝ)
216, 7, 19, 20syl3anc 1463 . 2 (𝜑 → sup(𝐴, ℝ, < ) ∈ ℝ)
226sselda 3732 . . . . 5 ((𝜑𝑥𝐴) → 𝑥 ∈ ℝ)
231adantr 472 . . . . . . 7 ((𝜑𝑥𝐴) → 𝐴 ⊆ (𝐵[,]𝐶))
24 simpr 479 . . . . . . 7 ((𝜑𝑥𝐴) → 𝑥𝐴)
25 iccsupr 12430 . . . . . . 7 (((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ⊆ (𝐵[,]𝐶) ∧ 𝑥𝐴) → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑥𝐴 𝑥𝑦))
268, 10, 23, 24, 25syl211anc 1469 . . . . . 6 ((𝜑𝑥𝐴) → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑥𝐴 𝑥𝑦))
2726, 20syl 17 . . . . 5 ((𝜑𝑥𝐴) → sup(𝐴, ℝ, < ) ∈ ℝ)
28 iccgelb 12394 . . . . . 6 ((𝐵 ∈ ℝ*𝐶 ∈ ℝ*𝑥 ∈ (𝐵[,]𝐶)) → 𝐵𝑥)
299, 11, 12, 28syl3anc 1463 . . . . 5 ((𝜑𝑥𝐴) → 𝐵𝑥)
30 suprub 11147 . . . . . 6 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑥𝐴 𝑥𝑦) ∧ 𝑥𝐴) → 𝑥 ≤ sup(𝐴, ℝ, < ))
3126, 24, 30syl2anc 696 . . . . 5 ((𝜑𝑥𝐴) → 𝑥 ≤ sup(𝐴, ℝ, < ))
328, 22, 27, 29, 31letrd 10357 . . . 4 ((𝜑𝑥𝐴) → 𝐵 ≤ sup(𝐴, ℝ, < ))
3332ralrimiva 3092 . . 3 (𝜑 → ∀𝑥𝐴 𝐵 ≤ sup(𝐴, ℝ, < ))
34 r19.3rzv 4196 . . . 4 (𝐴 ≠ ∅ → (𝐵 ≤ sup(𝐴, ℝ, < ) ↔ ∀𝑥𝐴 𝐵 ≤ sup(𝐴, ℝ, < )))
357, 34syl 17 . . 3 (𝜑 → (𝐵 ≤ sup(𝐴, ℝ, < ) ↔ ∀𝑥𝐴 𝐵 ≤ sup(𝐴, ℝ, < )))
3633, 35mpbird 247 . 2 (𝜑𝐵 ≤ sup(𝐴, ℝ, < ))
37 suprleub 11152 . . . 4 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑥𝐴 𝑥𝑦) ∧ 𝐶 ∈ ℝ) → (sup(𝐴, ℝ, < ) ≤ 𝐶 ↔ ∀𝑥𝐴 𝑥𝐶))
386, 7, 19, 3, 37syl31anc 1466 . . 3 (𝜑 → (sup(𝐴, ℝ, < ) ≤ 𝐶 ↔ ∀𝑥𝐴 𝑥𝐶))
3915, 38mpbird 247 . 2 (𝜑 → sup(𝐴, ℝ, < ) ≤ 𝐶)
40 elicc2 12402 . . 3 ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (sup(𝐴, ℝ, < ) ∈ (𝐵[,]𝐶) ↔ (sup(𝐴, ℝ, < ) ∈ ℝ ∧ 𝐵 ≤ sup(𝐴, ℝ, < ) ∧ sup(𝐴, ℝ, < ) ≤ 𝐶)))
412, 3, 40syl2anc 696 . 2 (𝜑 → (sup(𝐴, ℝ, < ) ∈ (𝐵[,]𝐶) ↔ (sup(𝐴, ℝ, < ) ∈ ℝ ∧ 𝐵 ≤ sup(𝐴, ℝ, < ) ∧ sup(𝐴, ℝ, < ) ≤ 𝐶)))
4221, 36, 39, 41mpbir3and 1406 1 (𝜑 → sup(𝐴, ℝ, < ) ∈ (𝐵[,]𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072   = wceq 1620   ∈ wcel 2127   ≠ wne 2920  ∀wral 3038  ∃wrex 3039   ⊆ wss 3703  ∅c0 4046   class class class wbr 4792  (class class class)co 6801  supcsup 8499  ℝcr 10098  ℝ*cxr 10236   < clt 10237   ≤ cle 10238  [,]cicc 12342 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043  ax-un 7102  ax-cnex 10155  ax-resscn 10156  ax-1cn 10157  ax-icn 10158  ax-addcl 10159  ax-addrcl 10160  ax-mulcl 10161  ax-mulrcl 10162  ax-mulcom 10163  ax-addass 10164  ax-mulass 10165  ax-distr 10166  ax-i2m1 10167  ax-1ne0 10168  ax-1rid 10169  ax-rnegex 10170  ax-rrecex 10171  ax-cnre 10172  ax-pre-lttri 10173  ax-pre-lttrn 10174  ax-pre-ltadd 10175  ax-pre-mulgt0 10176  ax-pre-sup 10177 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-nel 3024  df-ral 3043  df-rex 3044  df-reu 3045  df-rmo 3046  df-rab 3047  df-v 3330  df-sbc 3565  df-csb 3663  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-pw 4292  df-sn 4310  df-pr 4312  df-op 4316  df-uni 4577  df-br 4793  df-opab 4853  df-mpt 4870  df-id 5162  df-po 5175  df-so 5176  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267  df-iota 6000  df-fun 6039  df-fn 6040  df-f 6041  df-f1 6042  df-fo 6043  df-f1o 6044  df-fv 6045  df-riota 6762  df-ov 6804  df-oprab 6805  df-mpt2 6806  df-er 7899  df-en 8110  df-dom 8111  df-sdom 8112  df-sup 8501  df-pnf 10239  df-mnf 10240  df-xr 10241  df-ltxr 10242  df-le 10243  df-sub 10431  df-neg 10432  df-icc 12346 This theorem is referenced by:  supicclub2  12487  hoidmv1lelem1  41280  hoidmvlelem1  41284
 Copyright terms: Public domain W3C validator