|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > reliun | Structured version Visualization version GIF version | ||
| Description: An indexed union is a relation iff each member of its indexed family is a relation. (Contributed by NM, 19-Dec-2008.) | 
| Ref | Expression | 
|---|---|
| reliun | ⊢ (Rel ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 Rel 𝐵) | 
| 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 𝐵) | 
| 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 |