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

Theorem reliun 5825
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 4992 . . 3 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
21releqi 5786 . 2 (Rel 𝑥𝐴 𝐵 ↔ Rel {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵})
3 df-rel 5691 . 2 (Rel {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵} ↔ {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵} ⊆ (V × V))
4 abss 4062 . . 3 ({𝑦 ∣ ∃𝑥𝐴 𝑦𝐵} ⊆ (V × V) ↔ ∀𝑦(∃𝑥𝐴 𝑦𝐵𝑦 ∈ (V × V)))
5 df-rel 5691 . . . . . 6 (Rel 𝐵𝐵 ⊆ (V × V))
6 df-ss 3967 . . . . . 6 (𝐵 ⊆ (V × V) ↔ ∀𝑦(𝑦𝐵𝑦 ∈ (V × V)))
75, 6bitri 275 . . . . 5 (Rel 𝐵 ↔ ∀𝑦(𝑦𝐵𝑦 ∈ (V × V)))
87ralbii 3092 . . . 4 (∀𝑥𝐴 Rel 𝐵 ↔ ∀𝑥𝐴𝑦(𝑦𝐵𝑦 ∈ (V × V)))
9 ralcom4 3285 . . . 4 (∀𝑥𝐴𝑦(𝑦𝐵𝑦 ∈ (V × V)) ↔ ∀𝑦𝑥𝐴 (𝑦𝐵𝑦 ∈ (V × V)))
10 r19.23v 3182 . . . . 5 (∀𝑥𝐴 (𝑦𝐵𝑦 ∈ (V × V)) ↔ (∃𝑥𝐴 𝑦𝐵𝑦 ∈ (V × V)))
1110albii 1818 . . . 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 206  wal 1537  wcel 2107  {cab 2713  wral 3060  wrex 3069  Vcvv 3479  wss 3950   ciun 4990   × cxp 5682  Rel wrel 5689
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ral 3061  df-rex 3070  df-ss 3967  df-iun 4992  df-rel 5691
This theorem is referenced by:  reluni  5827  eliunxp  5847  opeliunxp2  5848  dfco2  6264  coiun  6275  fvn0ssdmfun  7093  opeliunxp2f  8236  fsumcom2  15811  fprodcom2  16021  imasaddfnlem  17574  imasvscafn  17583  gsum2d2lem  19992  gsum2d2  19993  gsumcom2  19994  dprd2d2  20065  cnextrel  24072  reldv  25906  dfcnv2  32687  gsumpart  33061  gsumwrd2dccat  33071  cvmliftlem1  35291  cnviun  43668  coiun1  43670  eliunxp2  48255
  Copyright terms: Public domain W3C validator