![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > suprcl | Structured version Visualization version GIF version |
Description: Closure of supremum of a nonempty bounded set of reals. (Contributed by NM, 12-Oct-2004.) |
Ref | Expression |
---|---|
suprcl | ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) ∈ ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltso 10308 | . . 3 ⊢ < Or ℝ | |
2 | 1 | a1i 11 | . 2 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → < Or ℝ) |
3 | sup3 11170 | . 2 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | |
4 | 2, 3 | supcl 8527 | 1 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) ∈ ℝ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1072 ∈ wcel 2137 ≠ wne 2930 ∀wral 3048 ∃wrex 3049 ⊆ wss 3713 ∅c0 4056 class class class wbr 4802 Or wor 5184 supcsup 8509 ℝcr 10125 < clt 10264 ≤ cle 10265 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1986 ax-6 2052 ax-7 2088 ax-8 2139 ax-9 2146 ax-10 2166 ax-11 2181 ax-12 2194 ax-13 2389 ax-ext 2738 ax-sep 4931 ax-nul 4939 ax-pow 4990 ax-pr 5053 ax-un 7112 ax-resscn 10183 ax-1cn 10184 ax-icn 10185 ax-addcl 10186 ax-addrcl 10187 ax-mulcl 10188 ax-mulrcl 10189 ax-mulcom 10190 ax-addass 10191 ax-mulass 10192 ax-distr 10193 ax-i2m1 10194 ax-1ne0 10195 ax-1rid 10196 ax-rnegex 10197 ax-rrecex 10198 ax-cnre 10199 ax-pre-lttri 10200 ax-pre-lttrn 10201 ax-pre-ltadd 10202 ax-pre-mulgt0 10203 ax-pre-sup 10204 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2045 df-eu 2609 df-mo 2610 df-clab 2745 df-cleq 2751 df-clel 2754 df-nfc 2889 df-ne 2931 df-nel 3034 df-ral 3053 df-rex 3054 df-reu 3055 df-rmo 3056 df-rab 3057 df-v 3340 df-sbc 3575 df-csb 3673 df-dif 3716 df-un 3718 df-in 3720 df-ss 3727 df-nul 4057 df-if 4229 df-pw 4302 df-sn 4320 df-pr 4322 df-op 4326 df-uni 4587 df-br 4803 df-opab 4863 df-mpt 4880 df-id 5172 df-po 5185 df-so 5186 df-xp 5270 df-rel 5271 df-cnv 5272 df-co 5273 df-dm 5274 df-rn 5275 df-res 5276 df-ima 5277 df-iota 6010 df-fun 6049 df-fn 6050 df-f 6051 df-f1 6052 df-fo 6053 df-f1o 6054 df-fv 6055 df-riota 6772 df-ov 6814 df-oprab 6815 df-mpt2 6816 df-er 7909 df-en 8120 df-dom 8121 df-sdom 8122 df-sup 8511 df-pnf 10266 df-mnf 10267 df-xr 10268 df-ltxr 10269 df-le 10270 df-sub 10458 df-neg 10459 |
This theorem is referenced by: suprub 11174 suprcld 11176 suprleub 11179 supaddc 11180 supadd 11181 supmul1 11182 supmullem1 11183 supmullem2 11184 supmul 11185 suprclii 11187 suprzcl 11647 supminf 11966 rpnnen1lem4 12008 rpnnen1lem4OLD 12014 supxrre 12348 supxrbnd 12349 supicc 12511 flval3 12808 sqrlem4 14183 climsup 14597 supcvg 14785 mertenslem1 14813 ruclem12 15167 prmreclem6 15825 icccmplem2 22825 icccmplem3 22826 reconnlem2 22829 evth 22957 ivthlem2 23419 ivthlem3 23420 ioombl1lem4 23527 mbfsup 23628 mbflimsup 23630 itg2monolem1 23714 itg2mono 23717 itg2cnlem1 23725 c1liplem1 23956 nmcexi 29192 rge0scvg 30302 ismblfin 33761 itg2addnclem2 33773 ftc1anclem7 33802 ftc1anc 33804 ubelsupr 39676 suprnmpt 39852 upbdrech 40016 suprltrp 40040 supsubc 40065 supminfxr 40190 |
Copyright terms: Public domain | W3C validator |