Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  upbdrech2 Structured version   Visualization version   GIF version

Theorem upbdrech2 42354
 Description: Choice of an upper bound for a possibly empty bunded set (image set version). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
upbdrech2.b ((𝜑𝑥𝐴) → 𝐵 ∈ ℝ)
upbdrech2.bd (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥𝐴 𝐵𝑦)
upbdrech2.c 𝐶 = if(𝐴 = ∅, 0, sup({𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}, ℝ, < ))
Assertion
Ref Expression
upbdrech2 (𝜑 → (𝐶 ∈ ℝ ∧ ∀𝑥𝐴 𝐵𝐶))
Distinct variable groups:   𝑥,𝐴,𝑦,𝑧   𝑦,𝐵,𝑧   𝜑,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑧)   𝐵(𝑥)   𝐶(𝑥,𝑦,𝑧)

Proof of Theorem upbdrech2
StepHypRef Expression
1 upbdrech2.c . . 3 𝐶 = if(𝐴 = ∅, 0, sup({𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}, ℝ, < ))
2 iftrue 4430 . . . . . 6 (𝐴 = ∅ → if(𝐴 = ∅, 0, sup({𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}, ℝ, < )) = 0)
3 0red 10696 . . . . . 6 (𝐴 = ∅ → 0 ∈ ℝ)
42, 3eqeltrd 2853 . . . . 5 (𝐴 = ∅ → if(𝐴 = ∅, 0, sup({𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}, ℝ, < )) ∈ ℝ)
54adantl 485 . . . 4 ((𝜑𝐴 = ∅) → if(𝐴 = ∅, 0, sup({𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}, ℝ, < )) ∈ ℝ)
6 simpr 488 . . . . . 6 ((𝜑 ∧ ¬ 𝐴 = ∅) → ¬ 𝐴 = ∅)
76iffalsed 4435 . . . . 5 ((𝜑 ∧ ¬ 𝐴 = ∅) → if(𝐴 = ∅, 0, sup({𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}, ℝ, < )) = sup({𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}, ℝ, < ))
86neqned 2959 . . . . . . 7 ((𝜑 ∧ ¬ 𝐴 = ∅) → 𝐴 ≠ ∅)
9 upbdrech2.b . . . . . . . 8 ((𝜑𝑥𝐴) → 𝐵 ∈ ℝ)
109adantlr 714 . . . . . . 7 (((𝜑 ∧ ¬ 𝐴 = ∅) ∧ 𝑥𝐴) → 𝐵 ∈ ℝ)
11 upbdrech2.bd . . . . . . . 8 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥𝐴 𝐵𝑦)
1211adantr 484 . . . . . . 7 ((𝜑 ∧ ¬ 𝐴 = ∅) → ∃𝑦 ∈ ℝ ∀𝑥𝐴 𝐵𝑦)
13 eqid 2759 . . . . . . 7 sup({𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}, ℝ, < ) = sup({𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}, ℝ, < )
148, 10, 12, 13upbdrech 42351 . . . . . 6 ((𝜑 ∧ ¬ 𝐴 = ∅) → (sup({𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}, ℝ, < ) ∈ ℝ ∧ ∀𝑥𝐴 𝐵 ≤ sup({𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}, ℝ, < )))
1514simpld 498 . . . . 5 ((𝜑 ∧ ¬ 𝐴 = ∅) → sup({𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}, ℝ, < ) ∈ ℝ)
167, 15eqeltrd 2853 . . . 4 ((𝜑 ∧ ¬ 𝐴 = ∅) → if(𝐴 = ∅, 0, sup({𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}, ℝ, < )) ∈ ℝ)
175, 16pm2.61dan 812 . . 3 (𝜑 → if(𝐴 = ∅, 0, sup({𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}, ℝ, < )) ∈ ℝ)
181, 17eqeltrid 2857 . 2 (𝜑𝐶 ∈ ℝ)
19 rzal 4405 . . . 4 (𝐴 = ∅ → ∀𝑥𝐴 𝐵𝐶)
2019adantl 485 . . 3 ((𝜑𝐴 = ∅) → ∀𝑥𝐴 𝐵𝐶)
2114simprd 499 . . . 4 ((𝜑 ∧ ¬ 𝐴 = ∅) → ∀𝑥𝐴 𝐵 ≤ sup({𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}, ℝ, < ))
22 iffalse 4433 . . . . . . . 8 𝐴 = ∅ → if(𝐴 = ∅, 0, sup({𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}, ℝ, < )) = sup({𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}, ℝ, < ))
231, 22syl5eq 2806 . . . . . . 7 𝐴 = ∅ → 𝐶 = sup({𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}, ℝ, < ))
2423breq2d 5049 . . . . . 6 𝐴 = ∅ → (𝐵𝐶𝐵 ≤ sup({𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}, ℝ, < )))
2524ralbidv 3127 . . . . 5 𝐴 = ∅ → (∀𝑥𝐴 𝐵𝐶 ↔ ∀𝑥𝐴 𝐵 ≤ sup({𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}, ℝ, < )))
2625adantl 485 . . . 4 ((𝜑 ∧ ¬ 𝐴 = ∅) → (∀𝑥𝐴 𝐵𝐶 ↔ ∀𝑥𝐴 𝐵 ≤ sup({𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}, ℝ, < )))
2721, 26mpbird 260 . . 3 ((𝜑 ∧ ¬ 𝐴 = ∅) → ∀𝑥𝐴 𝐵𝐶)
2820, 27pm2.61dan 812 . 2 (𝜑 → ∀𝑥𝐴 𝐵𝐶)
2918, 28jca 515 1 (𝜑 → (𝐶 ∈ ℝ ∧ ∀𝑥𝐴 𝐵𝐶))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1539   ∈ wcel 2112  {cab 2736  ∀wral 3071  ∃wrex 3072  ∅c0 4228  ifcif 4424   class class class wbr 5037  supcsup 8951  ℝcr 10588  0cc0 10589   < clt 10727   ≤ cle 10728 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5174  ax-nul 5181  ax-pow 5239  ax-pr 5303  ax-un 7466  ax-resscn 10646  ax-1cn 10647  ax-icn 10648  ax-addcl 10649  ax-addrcl 10650  ax-mulcl 10651  ax-mulrcl 10652  ax-mulcom 10653  ax-addass 10654  ax-mulass 10655  ax-distr 10656  ax-i2m1 10657  ax-1ne0 10658  ax-1rid 10659  ax-rnegex 10660  ax-rrecex 10661  ax-cnre 10662  ax-pre-lttri 10663  ax-pre-lttrn 10664  ax-pre-ltadd 10665  ax-pre-mulgt0 10666  ax-pre-sup 10667 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3700  df-csb 3809  df-dif 3864  df-un 3866  df-in 3868  df-ss 3878  df-nul 4229  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-op 4533  df-uni 4803  df-br 5038  df-opab 5100  df-mpt 5118  df-id 5435  df-po 5448  df-so 5449  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-res 5541  df-ima 5542  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-riota 7115  df-ov 7160  df-oprab 7161  df-mpo 7162  df-er 8306  df-en 8542  df-dom 8543  df-sdom 8544  df-sup 8953  df-pnf 10729  df-mnf 10730  df-xr 10731  df-ltxr 10732  df-le 10733  df-sub 10924  df-neg 10925 This theorem is referenced by:  ssfiunibd  42355
 Copyright terms: Public domain W3C validator