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.

Step	Hyp	Ref	Expression
1		df-iun 4992	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2	1	releqi 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)))
7	5, 6	bitri 275	. . . . 5 ⊢ (Rel 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V)))
8	7	ralbii 3092	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 Rel 𝐵 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V)))
9		ralcom4 3285	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V)) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V)))
10		r19.23v 3182	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V)) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V)))
11	10	albii 1818	. . . 4 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V)) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V)))
12	8, 9, 11	3bitri 297	. . 3 ⊢ (∀𝑥 ∈ 𝐴 Rel 𝐵 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V)))
13	4, 12	bitr4i 278	. 2 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ (V × V) ↔ ∀𝑥 ∈ 𝐴 Rel 𝐵)
14	2, 3, 13	3bitri 297	1 ⊢ (Rel ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 Rel 𝐵)

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