ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  suprleubex GIF version

Theorem suprleubex 8936
Description: The supremum of a nonempty bounded set of reals is less than or equal to an upper bound. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 6-Sep-2014.)
Hypotheses
Ref Expression
suprubex.ex (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
suprubex.ss (𝜑𝐴 ⊆ ℝ)
suprlubex.b (𝜑𝐵 ∈ ℝ)
Assertion
Ref Expression
suprleubex (𝜑 → (sup(𝐴, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧𝐴 𝑧𝐵))
Distinct variable groups:   𝑥,𝐴,𝑦,𝑧   𝜑,𝑥   𝑧,𝐵
Allowed substitution hints:   𝜑(𝑦,𝑧)   𝐵(𝑥,𝑦)

Proof of Theorem suprleubex
Dummy variables 𝑓 𝑔 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lttri3 8062 . . . . . . . 8 ((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) → (𝑓 = 𝑔 ↔ (¬ 𝑓 < 𝑔 ∧ ¬ 𝑔 < 𝑓)))
21adantl 277 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) → (𝑓 = 𝑔 ↔ (¬ 𝑓 < 𝑔 ∧ ¬ 𝑔 < 𝑓)))
3 suprubex.ex . . . . . . 7 (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
42, 3supclti 7022 . . . . . 6 (𝜑 → sup(𝐴, ℝ, < ) ∈ ℝ)
5 suprlubex.b . . . . . 6 (𝜑𝐵 ∈ ℝ)
64, 5lenltd 8100 . . . . 5 (𝜑 → (sup(𝐴, ℝ, < ) ≤ 𝐵 ↔ ¬ 𝐵 < sup(𝐴, ℝ, < )))
7 suprubex.ss . . . . . 6 (𝜑𝐴 ⊆ ℝ)
83, 7, 5suprnubex 8935 . . . . 5 (𝜑 → (¬ 𝐵 < sup(𝐴, ℝ, < ) ↔ ∀𝑧𝐴 ¬ 𝐵 < 𝑧))
96, 8bitrd 188 . . . 4 (𝜑 → (sup(𝐴, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧𝐴 ¬ 𝐵 < 𝑧))
10 breq2 4022 . . . . . 6 (𝑤 = 𝑧 → (𝐵 < 𝑤𝐵 < 𝑧))
1110notbid 668 . . . . 5 (𝑤 = 𝑧 → (¬ 𝐵 < 𝑤 ↔ ¬ 𝐵 < 𝑧))
1211cbvralv 2718 . . . 4 (∀𝑤𝐴 ¬ 𝐵 < 𝑤 ↔ ∀𝑧𝐴 ¬ 𝐵 < 𝑧)
139, 12bitr4di 198 . . 3 (𝜑 → (sup(𝐴, ℝ, < ) ≤ 𝐵 ↔ ∀𝑤𝐴 ¬ 𝐵 < 𝑤))
147sselda 3170 . . . . 5 ((𝜑𝑤𝐴) → 𝑤 ∈ ℝ)
155adantr 276 . . . . 5 ((𝜑𝑤𝐴) → 𝐵 ∈ ℝ)
1614, 15lenltd 8100 . . . 4 ((𝜑𝑤𝐴) → (𝑤𝐵 ↔ ¬ 𝐵 < 𝑤))
1716ralbidva 2486 . . 3 (𝜑 → (∀𝑤𝐴 𝑤𝐵 ↔ ∀𝑤𝐴 ¬ 𝐵 < 𝑤))
1813, 17bitr4d 191 . 2 (𝜑 → (sup(𝐴, ℝ, < ) ≤ 𝐵 ↔ ∀𝑤𝐴 𝑤𝐵))
19 breq1 4021 . . 3 (𝑤 = 𝑧 → (𝑤𝐵𝑧𝐵))
2019cbvralv 2718 . 2 (∀𝑤𝐴 𝑤𝐵 ↔ ∀𝑧𝐴 𝑧𝐵)
2118, 20bitrdi 196 1 (𝜑 → (sup(𝐴, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧𝐴 𝑧𝐵))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wcel 2160  wral 2468  wrex 2469  wss 3144   class class class wbr 4018  supcsup 7006  cr 7835   < clt 8017  cle 8018
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-pow 4189  ax-pr 4224  ax-un 4448  ax-setind 4551  ax-cnex 7927  ax-resscn 7928  ax-pre-ltirr 7948  ax-pre-ltwlin 7949  ax-pre-lttrn 7950  ax-pre-apti 7951
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-reu 2475  df-rmo 2476  df-rab 2477  df-v 2754  df-sbc 2978  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-opab 4080  df-po 4311  df-iso 4312  df-xp 4647  df-cnv 4649  df-iota 5193  df-riota 5848  df-sup 7008  df-pnf 8019  df-mnf 8020  df-xr 8021  df-ltxr 8022  df-le 8023
This theorem is referenced by:  suprzclex  9376  suplociccex  14540
  Copyright terms: Public domain W3C validator