![]() |
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 4996 | . . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} | |
2 | 1 | releqi 5774 | . 2 ⊢ (Rel ∪ 𝑥 ∈ 𝐴 𝐵 ↔ Rel {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}) |
3 | df-rel 5680 | . 2 ⊢ (Rel {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ (V × V)) | |
4 | abss 4057 | . . 3 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ (V × V) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V))) | |
5 | df-rel 5680 | . . . . . 6 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V)) | |
6 | df-ss 3964 | . . . . . 6 ⊢ (𝐵 ⊆ (V × V) ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V))) | |
7 | 5, 6 | bitri 274 | . . . . 5 ⊢ (Rel 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V))) |
8 | 7 | ralbii 3083 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 Rel 𝐵 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V))) |
9 | ralcom4 3274 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V)) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V))) | |
10 | r19.23v 3173 | . . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V)) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V))) | |
11 | 10 | albii 1814 | . . . 4 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V)) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V))) |
12 | 8, 9, 11 | 3bitri 296 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 Rel 𝐵 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V))) |
13 | 4, 12 | bitr4i 277 | . 2 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ (V × V) ↔ ∀𝑥 ∈ 𝐴 Rel 𝐵) |
14 | 2, 3, 13 | 3bitri 296 | 1 ⊢ (Rel ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 Rel 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1532 ∈ wcel 2099 {cab 2703 ∀wral 3051 ∃wrex 3060 Vcvv 3463 ⊆ wss 3947 ∪ ciun 4994 × cxp 5671 Rel wrel 5678 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1537 df-ex 1775 df-nf 1779 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ral 3052 df-rex 3061 df-ss 3964 df-iun 4996 df-rel 5680 |
This theorem is referenced by: reluni 5815 eliunxp 5835 opeliunxp2 5836 dfco2 6247 coiun 6258 fvn0ssdmfun 7078 opeliunxp2f 8215 fsumcom2 15771 fprodcom2 15979 imasaddfnlem 17536 imasvscafn 17545 gsum2d2lem 19965 gsum2d2 19966 gsumcom2 19967 dprd2d2 20038 cnextrel 24053 reldv 25885 dfcnv2 32591 gsumpart 32925 cvmliftlem1 35124 cnviun 43352 coiun1 43354 eliunxp2 47746 |
Copyright terms: Public domain | W3C validator |