Theorem reliun 5755

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 4941	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2	1	releqi 5717	. 2 ⊢ (Rel ∪ 𝑥 ∈ 𝐴 𝐵 ↔ Rel {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵})
3		df-rel 5621	. 2 ⊢ (Rel {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ (V × V))
4		abss 4009	. . 3 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ (V × V) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V)))
5		df-rel 5621	. . . . . 6 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V))
6		df-ss 3914	. . . . . 6 ⊢ (𝐵 ⊆ (V × V) ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V)))
7	5, 6	bitri 275	. . . . 5 ⊢ (Rel 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V)))
8	7	ralbii 3078	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 Rel 𝐵 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V)))
9		ralcom4 3258	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V)) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V)))
10		r19.23v 3159	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V)) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V)))
11	10	albii 1820	. . . 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 1539   ∈ wcel 2111  {cab 2709  ∀wral 3047  ∃wrex 3056  Vcvv 3436   ⊆ wss 3897  ∪ ciun 4939   × cxp 5612  Rel wrel 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-ss 3914  df-iun 4941  df-rel 5621

This theorem is referenced by:  reluni  5757  eliunxp  5776  opeliunxp2  5777  dfco2  6192  coiun  6204  fvn0ssdmfun  7007  opeliunxp2f  8140  fsumcom2  15681  fprodcom2  15891  imasaddfnlem  17432  imasvscafn  17441  gsum2d2lem  19885  gsum2d2  19886  gsumcom2  19887  dprd2d2  19958  cnextrel  23978  reldv  25798  dfcnv2  32658  gsumpart  33037  gsumwrd2dccat  33047  cvmliftlem1  35329  cnviun  43742  coiun1  43744  eliunxp2  48433