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 4906 | . . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} | |
2 | 1 | releqi 5649 | . 2 ⊢ (Rel ∪ 𝑥 ∈ 𝐴 𝐵 ↔ Rel {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}) |
3 | df-rel 5558 | . 2 ⊢ (Rel {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ (V × V)) | |
4 | abss 3974 | . . 3 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ (V × V) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V))) | |
5 | df-rel 5558 | . . . . . 6 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V)) | |
6 | dfss2 3886 | . . . . . 6 ⊢ (𝐵 ⊆ (V × V) ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V))) | |
7 | 5, 6 | bitri 278 | . . . . 5 ⊢ (Rel 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V))) |
8 | 7 | ralbii 3088 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 Rel 𝐵 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V))) |
9 | ralcom4 3157 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V)) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V))) | |
10 | r19.23v 3198 | . . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V)) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V))) | |
11 | 10 | albii 1827 | . . . 4 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V)) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V))) |
12 | 8, 9, 11 | 3bitri 300 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 Rel 𝐵 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V))) |
13 | 4, 12 | bitr4i 281 | . 2 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ (V × V) ↔ ∀𝑥 ∈ 𝐴 Rel 𝐵) |
14 | 2, 3, 13 | 3bitri 300 | 1 ⊢ (Rel ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 Rel 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∀wal 1541 ∈ wcel 2110 {cab 2714 ∀wral 3061 ∃wrex 3062 Vcvv 3408 ⊆ wss 3866 ∪ ciun 4904 × cxp 5549 Rel wrel 5556 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-tru 1546 df-ex 1788 df-nf 1792 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-ral 3066 df-rex 3067 df-v 3410 df-in 3873 df-ss 3883 df-iun 4906 df-rel 5558 |
This theorem is referenced by: reluni 5688 eliunxp 5706 opeliunxp2 5707 dfco2 6109 coiun 6120 fvn0ssdmfun 6895 opeliunxp2f 7952 fsumcom2 15338 fprodcom2 15546 imasaddfnlem 17033 imasvscafn 17042 gsum2d2lem 19358 gsum2d2 19359 gsumcom2 19360 dprd2d2 19431 cnextrel 22960 reldv 24767 dfcnv2 30733 gsumpart 31034 cvmliftlem1 32960 cnviun 40935 coiun1 40937 eliunxp2 45342 |
Copyright terms: Public domain | W3C validator |