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

Theorem reliun 5817
Description: An indexed union is a relation iff each member of its indexed family is a relation. (Contributed by NM, 19-Dec-2008.)
Assertion
Ref Expression
reliun (Rel 𝑥𝐴 𝐵 ↔ ∀𝑥𝐴 Rel 𝐵)

Proof of Theorem reliun
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 df-iun 5000 . . 3 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
21releqi 5778 . 2 (Rel 𝑥𝐴 𝐵 ↔ Rel {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵})
3 df-rel 5684 . 2 (Rel {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵} ↔ {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵} ⊆ (V × V))
4 abss 4058 . . 3 ({𝑦 ∣ ∃𝑥𝐴 𝑦𝐵} ⊆ (V × V) ↔ ∀𝑦(∃𝑥𝐴 𝑦𝐵𝑦 ∈ (V × V)))
5 df-rel 5684 . . . . . 6 (Rel 𝐵𝐵 ⊆ (V × V))
6 dfss2 3969 . . . . . 6 (𝐵 ⊆ (V × V) ↔ ∀𝑦(𝑦𝐵𝑦 ∈ (V × V)))
75, 6bitri 275 . . . . 5 (Rel 𝐵 ↔ ∀𝑦(𝑦𝐵𝑦 ∈ (V × V)))
87ralbii 3094 . . . 4 (∀𝑥𝐴 Rel 𝐵 ↔ ∀𝑥𝐴𝑦(𝑦𝐵𝑦 ∈ (V × V)))
9 ralcom4 3284 . . . 4 (∀𝑥𝐴𝑦(𝑦𝐵𝑦 ∈ (V × V)) ↔ ∀𝑦𝑥𝐴 (𝑦𝐵𝑦 ∈ (V × V)))
10 r19.23v 3183 . . . . 5 (∀𝑥𝐴 (𝑦𝐵𝑦 ∈ (V × V)) ↔ (∃𝑥𝐴 𝑦𝐵𝑦 ∈ (V × V)))
1110albii 1822 . . . 4 (∀𝑦𝑥𝐴 (𝑦𝐵𝑦 ∈ (V × V)) ↔ ∀𝑦(∃𝑥𝐴 𝑦𝐵𝑦 ∈ (V × V)))
128, 9, 113bitri 297 . . 3 (∀𝑥𝐴 Rel 𝐵 ↔ ∀𝑦(∃𝑥𝐴 𝑦𝐵𝑦 ∈ (V × V)))
134, 12bitr4i 278 . 2 ({𝑦 ∣ ∃𝑥𝐴 𝑦𝐵} ⊆ (V × V) ↔ ∀𝑥𝐴 Rel 𝐵)
142, 3, 133bitri 297 1 (Rel 𝑥𝐴 𝐵 ↔ ∀𝑥𝐴 Rel 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1540  wcel 2107  {cab 2710  wral 3062  wrex 3071  Vcvv 3475  wss 3949   ciun 4998   × cxp 5675  Rel wrel 5682
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-v 3477  df-in 3956  df-ss 3966  df-iun 5000  df-rel 5684
This theorem is referenced by:  reluni  5819  eliunxp  5838  opeliunxp2  5839  dfco2  6245  coiun  6256  fvn0ssdmfun  7077  opeliunxp2f  8195  fsumcom2  15720  fprodcom2  15928  imasaddfnlem  17474  imasvscafn  17483  gsum2d2lem  19841  gsum2d2  19842  gsumcom2  19843  dprd2d2  19914  cnextrel  23567  reldv  25387  dfcnv2  31932  gsumpart  32238  cvmliftlem1  34307  cnviun  42449  coiun1  42451  eliunxp2  47057
  Copyright terms: Public domain W3C validator