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

Theorem dfiun2g 5030
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 2141, ax-12 2177. (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 4993 . 2 𝑥𝐴 𝐵 = {𝑧 ∣ ∃𝑥𝐴 𝑧𝐵}
2 elisset 2823 . . . . . . . . 9 (𝐵𝐶 → ∃𝑧 𝑧 = 𝐵)
3 eleq2 2830 . . . . . . . . . . . 12 (𝑧 = 𝐵 → (𝑤𝑧𝑤𝐵))
43pm5.32ri 575 . . . . . . . . . . 11 ((𝑤𝑧𝑧 = 𝐵) ↔ (𝑤𝐵𝑧 = 𝐵))
54simplbi2 500 . . . . . . . . . 10 (𝑤𝐵 → (𝑧 = 𝐵 → (𝑤𝑧𝑧 = 𝐵)))
65eximdv 1917 . . . . . . . . 9 (𝑤𝐵 → (∃𝑧 𝑧 = 𝐵 → ∃𝑧(𝑤𝑧𝑧 = 𝐵)))
72, 6syl5com 31 . . . . . . . 8 (𝐵𝐶 → (𝑤𝐵 → ∃𝑧(𝑤𝑧𝑧 = 𝐵)))
87ralimi 3083 . . . . . . 7 (∀𝑥𝐴 𝐵𝐶 → ∀𝑥𝐴 (𝑤𝐵 → ∃𝑧(𝑤𝑧𝑧 = 𝐵)))
9 rexim 3087 . . . . . . 7 (∀𝑥𝐴 (𝑤𝐵 → ∃𝑧(𝑤𝑧𝑧 = 𝐵)) → (∃𝑥𝐴 𝑤𝐵 → ∃𝑥𝐴𝑧(𝑤𝑧𝑧 = 𝐵)))
108, 9syl 17 . . . . . 6 (∀𝑥𝐴 𝐵𝐶 → (∃𝑥𝐴 𝑤𝐵 → ∃𝑥𝐴𝑧(𝑤𝑧𝑧 = 𝐵)))
11 rexcom4 3288 . . . . . . 7 (∃𝑥𝐴𝑧(𝑤𝑧𝑧 = 𝐵) ↔ ∃𝑧𝑥𝐴 (𝑤𝑧𝑧 = 𝐵))
12 r19.42v 3191 . . . . . . . 8 (∃𝑥𝐴 (𝑤𝑧𝑧 = 𝐵) ↔ (𝑤𝑧 ∧ ∃𝑥𝐴 𝑧 = 𝐵))
1312exbii 1848 . . . . . . 7 (∃𝑧𝑥𝐴 (𝑤𝑧𝑧 = 𝐵) ↔ ∃𝑧(𝑤𝑧 ∧ ∃𝑥𝐴 𝑧 = 𝐵))
1411, 13bitri 275 . . . . . 6 (∃𝑥𝐴𝑧(𝑤𝑧𝑧 = 𝐵) ↔ ∃𝑧(𝑤𝑧 ∧ ∃𝑥𝐴 𝑧 = 𝐵))
1510, 14imbitrdi 251 . . . . 5 (∀𝑥𝐴 𝐵𝐶 → (∃𝑥𝐴 𝑤𝐵 → ∃𝑧(𝑤𝑧 ∧ ∃𝑥𝐴 𝑧 = 𝐵)))
163biimpac 478 . . . . . . . 8 ((𝑤𝑧𝑧 = 𝐵) → 𝑤𝐵)
1716reximi 3084 . . . . . . 7 (∃𝑥𝐴 (𝑤𝑧𝑧 = 𝐵) → ∃𝑥𝐴 𝑤𝐵)
1812, 17sylbir 235 . . . . . 6 ((𝑤𝑧 ∧ ∃𝑥𝐴 𝑧 = 𝐵) → ∃𝑥𝐴 𝑤𝐵)
1918exlimiv 1930 . . . . 5 (∃𝑧(𝑤𝑧 ∧ ∃𝑥𝐴 𝑧 = 𝐵) → ∃𝑥𝐴 𝑤𝐵)
2015, 19impbid1 225 . . . 4 (∀𝑥𝐴 𝐵𝐶 → (∃𝑥𝐴 𝑤𝐵 ↔ ∃𝑧(𝑤𝑧 ∧ ∃𝑥𝐴 𝑧 = 𝐵)))
21 vex 3484 . . . . 5 𝑤 ∈ V
22 eleq1w 2824 . . . . . 6 (𝑧 = 𝑤 → (𝑧𝐵𝑤𝐵))
2322rexbidv 3179 . . . . 5 (𝑧 = 𝑤 → (∃𝑥𝐴 𝑧𝐵 ↔ ∃𝑥𝐴 𝑤𝐵))
2421, 23elab 3679 . . . 4 (𝑤 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧𝐵} ↔ ∃𝑥𝐴 𝑤𝐵)
25 eluni 4910 . . . . 5 (𝑤 {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ↔ ∃𝑧(𝑤𝑧𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵}))
26 vex 3484 . . . . . . . 8 𝑧 ∈ V
27 eqeq1 2741 . . . . . . . . 9 (𝑦 = 𝑧 → (𝑦 = 𝐵𝑧 = 𝐵))
2827rexbidv 3179 . . . . . . . 8 (𝑦 = 𝑧 → (∃𝑥𝐴 𝑦 = 𝐵 ↔ ∃𝑥𝐴 𝑧 = 𝐵))
2926, 28elab 3679 . . . . . . 7 (𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ↔ ∃𝑥𝐴 𝑧 = 𝐵)
3029anbi2i 623 . . . . . 6 ((𝑤𝑧𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵}) ↔ (𝑤𝑧 ∧ ∃𝑥𝐴 𝑧 = 𝐵))
3130exbii 1848 . . . . 5 (∃𝑧(𝑤𝑧𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵}) ↔ ∃𝑧(𝑤𝑧 ∧ ∃𝑥𝐴 𝑧 = 𝐵))
3225, 31bitri 275 . . . 4 (𝑤 {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ↔ ∃𝑧(𝑤𝑧 ∧ ∃𝑥𝐴 𝑧 = 𝐵))
3320, 24, 323bitr4g 314 . . 3 (∀𝑥𝐴 𝐵𝐶 → (𝑤 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧𝐵} ↔ 𝑤 {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵}))
3433eqrdv 2735 . 2 (∀𝑥𝐴 𝐵𝐶 → {𝑧 ∣ ∃𝑥𝐴 𝑧𝐵} = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵})
351, 34eqtrid 2789 1 (∀𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  wex 1779  wcel 2108  {cab 2714  wral 3061  wrex 3070   cuni 4907   ciun 4991
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-11 2157  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-v 3482  df-uni 4908  df-iun 4993
This theorem is referenced by:  dfiun2  5033  dfiun3g  5978  abnexg  7776  iunexg  7988  uniqs  8817  ac6num  10519  iunopn  22904  pnrmopn  23351  cncmp  23400  ptcmplem3  24062  iunmbl  25588  voliun  25589  sigaclcuni  34119  sigaclcu2  34121  sigaclci  34133  measvunilem  34213  meascnbl  34220  carsgclctunlem3  34322  uniqsALTV  38330
  Copyright terms: Public domain W3C validator