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

Theorem dfiun2g 5034
Description: Alternate definition of indexed union when 𝐵 is a set. Definition 15(a) of [Suppes] p. 44. (Contributed by NM, 23-Mar-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (Proof shortened by Rohan Ridenour, 11-Aug-2023.) Avoid ax-10 2138, ax-12 2174. (Revised by SN, 11-Dec-2024.)
Assertion
Ref Expression
dfiun2g (∀𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵})
Distinct variable groups:   𝑦,𝐴   𝑦,𝐵   𝑥,𝑦
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥,𝑦)

Proof of Theorem dfiun2g
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-iun 4997 . 2 𝑥𝐴 𝐵 = {𝑧 ∣ ∃𝑥𝐴 𝑧𝐵}
2 elisset 2820 . . . . . . . . 9 (𝐵𝐶 → ∃𝑧 𝑧 = 𝐵)
3 eleq2 2827 . . . . . . . . . . . 12 (𝑧 = 𝐵 → (𝑤𝑧𝑤𝐵))
43pm5.32ri 575 . . . . . . . . . . 11 ((𝑤𝑧𝑧 = 𝐵) ↔ (𝑤𝐵𝑧 = 𝐵))
54simplbi2 500 . . . . . . . . . 10 (𝑤𝐵 → (𝑧 = 𝐵 → (𝑤𝑧𝑧 = 𝐵)))
65eximdv 1914 . . . . . . . . 9 (𝑤𝐵 → (∃𝑧 𝑧 = 𝐵 → ∃𝑧(𝑤𝑧𝑧 = 𝐵)))
72, 6syl5com 31 . . . . . . . 8 (𝐵𝐶 → (𝑤𝐵 → ∃𝑧(𝑤𝑧𝑧 = 𝐵)))
87ralimi 3080 . . . . . . 7 (∀𝑥𝐴 𝐵𝐶 → ∀𝑥𝐴 (𝑤𝐵 → ∃𝑧(𝑤𝑧𝑧 = 𝐵)))
9 rexim 3084 . . . . . . 7 (∀𝑥𝐴 (𝑤𝐵 → ∃𝑧(𝑤𝑧𝑧 = 𝐵)) → (∃𝑥𝐴 𝑤𝐵 → ∃𝑥𝐴𝑧(𝑤𝑧𝑧 = 𝐵)))
108, 9syl 17 . . . . . 6 (∀𝑥𝐴 𝐵𝐶 → (∃𝑥𝐴 𝑤𝐵 → ∃𝑥𝐴𝑧(𝑤𝑧𝑧 = 𝐵)))
11 rexcom4 3285 . . . . . . 7 (∃𝑥𝐴𝑧(𝑤𝑧𝑧 = 𝐵) ↔ ∃𝑧𝑥𝐴 (𝑤𝑧𝑧 = 𝐵))
12 r19.42v 3188 . . . . . . . 8 (∃𝑥𝐴 (𝑤𝑧𝑧 = 𝐵) ↔ (𝑤𝑧 ∧ ∃𝑥𝐴 𝑧 = 𝐵))
1312exbii 1844 . . . . . . 7 (∃𝑧𝑥𝐴 (𝑤𝑧𝑧 = 𝐵) ↔ ∃𝑧(𝑤𝑧 ∧ ∃𝑥𝐴 𝑧 = 𝐵))
1411, 13bitri 275 . . . . . 6 (∃𝑥𝐴𝑧(𝑤𝑧𝑧 = 𝐵) ↔ ∃𝑧(𝑤𝑧 ∧ ∃𝑥𝐴 𝑧 = 𝐵))
1510, 14imbitrdi 251 . . . . 5 (∀𝑥𝐴 𝐵𝐶 → (∃𝑥𝐴 𝑤𝐵 → ∃𝑧(𝑤𝑧 ∧ ∃𝑥𝐴 𝑧 = 𝐵)))
163biimpac 478 . . . . . . . 8 ((𝑤𝑧𝑧 = 𝐵) → 𝑤𝐵)
1716reximi 3081 . . . . . . 7 (∃𝑥𝐴 (𝑤𝑧𝑧 = 𝐵) → ∃𝑥𝐴 𝑤𝐵)
1812, 17sylbir 235 . . . . . 6 ((𝑤𝑧 ∧ ∃𝑥𝐴 𝑧 = 𝐵) → ∃𝑥𝐴 𝑤𝐵)
1918exlimiv 1927 . . . . 5 (∃𝑧(𝑤𝑧 ∧ ∃𝑥𝐴 𝑧 = 𝐵) → ∃𝑥𝐴 𝑤𝐵)
2015, 19impbid1 225 . . . 4 (∀𝑥𝐴 𝐵𝐶 → (∃𝑥𝐴 𝑤𝐵 ↔ ∃𝑧(𝑤𝑧 ∧ ∃𝑥𝐴 𝑧 = 𝐵)))
21 vex 3481 . . . . 5 𝑤 ∈ V
22 eleq1w 2821 . . . . . 6 (𝑧 = 𝑤 → (𝑧𝐵𝑤𝐵))
2322rexbidv 3176 . . . . 5 (𝑧 = 𝑤 → (∃𝑥𝐴 𝑧𝐵 ↔ ∃𝑥𝐴 𝑤𝐵))
2421, 23elab 3680 . . . 4 (𝑤 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧𝐵} ↔ ∃𝑥𝐴 𝑤𝐵)
25 eluni 4914 . . . . 5 (𝑤 {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ↔ ∃𝑧(𝑤𝑧𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵}))
26 vex 3481 . . . . . . . 8 𝑧 ∈ V
27 eqeq1 2738 . . . . . . . . 9 (𝑦 = 𝑧 → (𝑦 = 𝐵𝑧 = 𝐵))
2827rexbidv 3176 . . . . . . . 8 (𝑦 = 𝑧 → (∃𝑥𝐴 𝑦 = 𝐵 ↔ ∃𝑥𝐴 𝑧 = 𝐵))
2926, 28elab 3680 . . . . . . 7 (𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ↔ ∃𝑥𝐴 𝑧 = 𝐵)
3029anbi2i 623 . . . . . 6 ((𝑤𝑧𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵}) ↔ (𝑤𝑧 ∧ ∃𝑥𝐴 𝑧 = 𝐵))
3130exbii 1844 . . . . 5 (∃𝑧(𝑤𝑧𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵}) ↔ ∃𝑧(𝑤𝑧 ∧ ∃𝑥𝐴 𝑧 = 𝐵))
3225, 31bitri 275 . . . 4 (𝑤 {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ↔ ∃𝑧(𝑤𝑧 ∧ ∃𝑥𝐴 𝑧 = 𝐵))
3320, 24, 323bitr4g 314 . . 3 (∀𝑥𝐴 𝐵𝐶 → (𝑤 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧𝐵} ↔ 𝑤 {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵}))
3433eqrdv 2732 . 2 (∀𝑥𝐴 𝐵𝐶 → {𝑧 ∣ ∃𝑥𝐴 𝑧𝐵} = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵})
351, 34eqtrid 2786 1 (∀𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1536  wex 1775  wcel 2105  {cab 2711  wral 3058  wrex 3067   cuni 4911   ciun 4995
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-11 2154  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-v 3479  df-uni 4912  df-iun 4997
This theorem is referenced by:  dfiun2  5037  dfiun3g  5980  abnexg  7774  iunexg  7986  uniqs  8815  ac6num  10516  iunopn  22919  pnrmopn  23366  cncmp  23415  ptcmplem3  24077  iunmbl  25601  voliun  25602  sigaclcuni  34098  sigaclcu2  34100  sigaclci  34112  measvunilem  34192  meascnbl  34199  carsgclctunlem3  34301  uniqsALTV  38310
  Copyright terms: Public domain W3C validator