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

Theorem fimaxre3 11638
 Description: A nonempty finite set of real numbers has a maximum (image set version). (Contributed by Mario Carneiro, 13-Feb-2014.)
Assertion
Ref Expression
fimaxre3 ((𝐴 ∈ Fin ∧ ∀𝑦𝐴 𝐵 ∈ ℝ) → ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝐵𝑥)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵
Allowed substitution hint:   𝐵(𝑦)

Proof of Theorem fimaxre3
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 r19.29 3182 . . . . . 6 ((∀𝑦𝐴 𝐵 ∈ ℝ ∧ ∃𝑦𝐴 𝑧 = 𝐵) → ∃𝑦𝐴 (𝐵 ∈ ℝ ∧ 𝑧 = 𝐵))
2 eleq1 2840 . . . . . . . 8 (𝑧 = 𝐵 → (𝑧 ∈ ℝ ↔ 𝐵 ∈ ℝ))
32biimparc 483 . . . . . . 7 ((𝐵 ∈ ℝ ∧ 𝑧 = 𝐵) → 𝑧 ∈ ℝ)
43rexlimivw 3207 . . . . . 6 (∃𝑦𝐴 (𝐵 ∈ ℝ ∧ 𝑧 = 𝐵) → 𝑧 ∈ ℝ)
51, 4syl 17 . . . . 5 ((∀𝑦𝐴 𝐵 ∈ ℝ ∧ ∃𝑦𝐴 𝑧 = 𝐵) → 𝑧 ∈ ℝ)
65ex 416 . . . 4 (∀𝑦𝐴 𝐵 ∈ ℝ → (∃𝑦𝐴 𝑧 = 𝐵𝑧 ∈ ℝ))
76abssdv 3976 . . 3 (∀𝑦𝐴 𝐵 ∈ ℝ → {𝑧 ∣ ∃𝑦𝐴 𝑧 = 𝐵} ⊆ ℝ)
8 abrexfi 8871 . . 3 (𝐴 ∈ Fin → {𝑧 ∣ ∃𝑦𝐴 𝑧 = 𝐵} ∈ Fin)
9 fimaxre2 11637 . . 3 (({𝑧 ∣ ∃𝑦𝐴 𝑧 = 𝐵} ⊆ ℝ ∧ {𝑧 ∣ ∃𝑦𝐴 𝑧 = 𝐵} ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑦𝐴 𝑧 = 𝐵}𝑤𝑥)
107, 8, 9syl2anr 599 . 2 ((𝐴 ∈ Fin ∧ ∀𝑦𝐴 𝐵 ∈ ℝ) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑦𝐴 𝑧 = 𝐵}𝑤𝑥)
11 r19.23v 3204 . . . . . . 7 (∀𝑦𝐴 (𝑤 = 𝐵𝑤𝑥) ↔ (∃𝑦𝐴 𝑤 = 𝐵𝑤𝑥))
1211albii 1822 . . . . . 6 (∀𝑤𝑦𝐴 (𝑤 = 𝐵𝑤𝑥) ↔ ∀𝑤(∃𝑦𝐴 𝑤 = 𝐵𝑤𝑥))
13 ralcom4 3163 . . . . . 6 (∀𝑦𝐴𝑤(𝑤 = 𝐵𝑤𝑥) ↔ ∀𝑤𝑦𝐴 (𝑤 = 𝐵𝑤𝑥))
14 eqeq1 2763 . . . . . . . 8 (𝑧 = 𝑤 → (𝑧 = 𝐵𝑤 = 𝐵))
1514rexbidv 3222 . . . . . . 7 (𝑧 = 𝑤 → (∃𝑦𝐴 𝑧 = 𝐵 ↔ ∃𝑦𝐴 𝑤 = 𝐵))
1615ralab 3610 . . . . . 6 (∀𝑤 ∈ {𝑧 ∣ ∃𝑦𝐴 𝑧 = 𝐵}𝑤𝑥 ↔ ∀𝑤(∃𝑦𝐴 𝑤 = 𝐵𝑤𝑥))
1712, 13, 163bitr4i 306 . . . . 5 (∀𝑦𝐴𝑤(𝑤 = 𝐵𝑤𝑥) ↔ ∀𝑤 ∈ {𝑧 ∣ ∃𝑦𝐴 𝑧 = 𝐵}𝑤𝑥)
18 nfv 1916 . . . . . . . 8 𝑤 𝐵𝑥
19 breq1 5040 . . . . . . . 8 (𝑤 = 𝐵 → (𝑤𝑥𝐵𝑥))
2018, 19ceqsalg 3446 . . . . . . 7 (𝐵 ∈ ℝ → (∀𝑤(𝑤 = 𝐵𝑤𝑥) ↔ 𝐵𝑥))
2120ralimi 3093 . . . . . 6 (∀𝑦𝐴 𝐵 ∈ ℝ → ∀𝑦𝐴 (∀𝑤(𝑤 = 𝐵𝑤𝑥) ↔ 𝐵𝑥))
22 ralbi 3100 . . . . . 6 (∀𝑦𝐴 (∀𝑤(𝑤 = 𝐵𝑤𝑥) ↔ 𝐵𝑥) → (∀𝑦𝐴𝑤(𝑤 = 𝐵𝑤𝑥) ↔ ∀𝑦𝐴 𝐵𝑥))
2321, 22syl 17 . . . . 5 (∀𝑦𝐴 𝐵 ∈ ℝ → (∀𝑦𝐴𝑤(𝑤 = 𝐵𝑤𝑥) ↔ ∀𝑦𝐴 𝐵𝑥))
2417, 23bitr3id 288 . . . 4 (∀𝑦𝐴 𝐵 ∈ ℝ → (∀𝑤 ∈ {𝑧 ∣ ∃𝑦𝐴 𝑧 = 𝐵}𝑤𝑥 ↔ ∀𝑦𝐴 𝐵𝑥))
2524rexbidv 3222 . . 3 (∀𝑦𝐴 𝐵 ∈ ℝ → (∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑦𝐴 𝑧 = 𝐵}𝑤𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝐵𝑥))
2625adantl 485 . 2 ((𝐴 ∈ Fin ∧ ∀𝑦𝐴 𝐵 ∈ ℝ) → (∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑦𝐴 𝑧 = 𝐵}𝑤𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝐵𝑥))
2710, 26mpbid 235 1 ((𝐴 ∈ Fin ∧ ∀𝑦𝐴 𝐵 ∈ ℝ) → ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝐵𝑥)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1537   = wceq 1539   ∈ wcel 2112  {cab 2736  ∀wral 3071  ∃wrex 3072   ⊆ wss 3861   class class class wbr 5037  Fincfn 8541  ℝcr 10588   ≤ 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-addrcl 10650  ax-rnegex 10660  ax-cnre 10662  ax-pre-lttri 10663  ax-pre-lttrn 10664 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-rab 3080  df-v 3412  df-sbc 3700  df-csb 3809  df-dif 3864  df-un 3866  df-in 3868  df-ss 3878  df-pss 3880  df-nul 4229  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-tp 4531  df-op 4533  df-uni 4803  df-br 5038  df-opab 5100  df-mpt 5118  df-tr 5144  df-id 5435  df-eprel 5440  df-po 5448  df-so 5449  df-fr 5488  df-we 5490  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-ord 6178  df-on 6179  df-lim 6180  df-suc 6181  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-om 7587  df-1st 7700  df-2nd 7701  df-1o 8119  df-er 8306  df-en 8542  df-dom 8543  df-sdom 8544  df-fin 8545  df-pnf 10729  df-mnf 10730  df-xr 10731  df-ltxr 10732  df-le 10733 This theorem is referenced by:  fsequb  13406  fsequb2  13407  caubnd  14780  limsupgre  14900  vdwnnlem3  16403  cnheibor  23671  bndth  23674  ovoliunlem2  24218  dchrisum  26190  ssfiunibd  42355  fimaxre4  42450  uzublem  42479  fourierdlem70  43230  fourierdlem71  43231  fourierdlem80  43240
 Copyright terms: Public domain W3C validator