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

Theorem rnmptbddlem 40368
 Description: Boundness of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
Hypotheses
Ref Expression
rnmptbddlem.x 𝑥𝜑
rnmptbddlem.b (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥𝐴 𝐵𝑦)
Assertion
Ref Expression
rnmptbddlem (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥𝐴𝐵)𝑧𝑦)
Distinct variable groups:   𝑧,𝐴   𝑧,𝐵   𝜑,𝑦,𝑧   𝑥,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem rnmptbddlem
StepHypRef Expression
1 rnmptbddlem.b . 2 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥𝐴 𝐵𝑦)
2 vex 3401 . . . . . . . . 9 𝑧 ∈ V
3 eqid 2778 . . . . . . . . . 10 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
43elrnmpt 5618 . . . . . . . . 9 (𝑧 ∈ V → (𝑧 ∈ ran (𝑥𝐴𝐵) ↔ ∃𝑥𝐴 𝑧 = 𝐵))
52, 4ax-mp 5 . . . . . . . 8 (𝑧 ∈ ran (𝑥𝐴𝐵) ↔ ∃𝑥𝐴 𝑧 = 𝐵)
65biimpi 208 . . . . . . 7 (𝑧 ∈ ran (𝑥𝐴𝐵) → ∃𝑥𝐴 𝑧 = 𝐵)
76adantl 475 . . . . . 6 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥𝐴 𝐵𝑦) ∧ 𝑧 ∈ ran (𝑥𝐴𝐵)) → ∃𝑥𝐴 𝑧 = 𝐵)
8 rnmptbddlem.x . . . . . . . . . 10 𝑥𝜑
9 nfv 1957 . . . . . . . . . 10 𝑥 𝑦 ∈ ℝ
108, 9nfan 1946 . . . . . . . . 9 𝑥(𝜑𝑦 ∈ ℝ)
11 nfra1 3123 . . . . . . . . 9 𝑥𝑥𝐴 𝐵𝑦
1210, 11nfan 1946 . . . . . . . 8 𝑥((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥𝐴 𝐵𝑦)
13 nfv 1957 . . . . . . . 8 𝑥 𝑧𝑦
14 rspa 3112 . . . . . . . . . . . 12 ((∀𝑥𝐴 𝐵𝑦𝑥𝐴) → 𝐵𝑦)
15143adant3 1123 . . . . . . . . . . 11 ((∀𝑥𝐴 𝐵𝑦𝑥𝐴𝑧 = 𝐵) → 𝐵𝑦)
16 simp3 1129 . . . . . . . . . . 11 ((∀𝑥𝐴 𝐵𝑦𝑥𝐴𝑧 = 𝐵) → 𝑧 = 𝐵)
17 simpr 479 . . . . . . . . . . . 12 ((𝐵𝑦𝑧 = 𝐵) → 𝑧 = 𝐵)
18 simpl 476 . . . . . . . . . . . 12 ((𝐵𝑦𝑧 = 𝐵) → 𝐵𝑦)
1917, 18eqbrtrd 4908 . . . . . . . . . . 11 ((𝐵𝑦𝑧 = 𝐵) → 𝑧𝑦)
2015, 16, 19syl2anc 579 . . . . . . . . . 10 ((∀𝑥𝐴 𝐵𝑦𝑥𝐴𝑧 = 𝐵) → 𝑧𝑦)
21203exp 1109 . . . . . . . . 9 (∀𝑥𝐴 𝐵𝑦 → (𝑥𝐴 → (𝑧 = 𝐵𝑧𝑦)))
2221adantl 475 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥𝐴 𝐵𝑦) → (𝑥𝐴 → (𝑧 = 𝐵𝑧𝑦)))
2312, 13, 22rexlimd 3208 . . . . . . 7 (((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥𝐴 𝐵𝑦) → (∃𝑥𝐴 𝑧 = 𝐵𝑧𝑦))
2423imp 397 . . . . . 6 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥𝐴 𝐵𝑦) ∧ ∃𝑥𝐴 𝑧 = 𝐵) → 𝑧𝑦)
257, 24syldan 585 . . . . 5 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥𝐴 𝐵𝑦) ∧ 𝑧 ∈ ran (𝑥𝐴𝐵)) → 𝑧𝑦)
2625ralrimiva 3148 . . . 4 (((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥𝐴 𝐵𝑦) → ∀𝑧 ∈ ran (𝑥𝐴𝐵)𝑧𝑦)
2726ex 403 . . 3 ((𝜑𝑦 ∈ ℝ) → (∀𝑥𝐴 𝐵𝑦 → ∀𝑧 ∈ ran (𝑥𝐴𝐵)𝑧𝑦))
2827reximdva 3198 . 2 (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥𝐴 𝐵𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥𝐴𝐵)𝑧𝑦))
291, 28mpd 15 1 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥𝐴𝐵)𝑧𝑦)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   ∧ w3a 1071   = wceq 1601  Ⅎwnf 1827   ∈ wcel 2107  ∀wral 3090  ∃wrex 3091  Vcvv 3398   class class class wbr 4886   ↦ cmpt 4965  ran crn 5356  ℝcr 10271   ≤ cle 10412 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pr 5138 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4887  df-opab 4949  df-mpt 4966  df-cnv 5363  df-dm 5365  df-rn 5366 This theorem is referenced by:  rnmptbdd  40369
 Copyright terms: Public domain W3C validator