![]() |
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 4999 | . . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} | |
2 | 1 | releqi 5777 | . 2 ⊢ (Rel ∪ 𝑥 ∈ 𝐴 𝐵 ↔ Rel {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}) |
3 | df-rel 5683 | . 2 ⊢ (Rel {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ (V × V)) | |
4 | abss 4057 | . . 3 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ (V × V) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V))) | |
5 | df-rel 5683 | . . . . . 6 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V)) | |
6 | dfss2 3968 | . . . . . 6 ⊢ (𝐵 ⊆ (V × V) ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V))) | |
7 | 5, 6 | bitri 274 | . . . . 5 ⊢ (Rel 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V))) |
8 | 7 | ralbii 3093 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 Rel 𝐵 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V))) |
9 | ralcom4 3283 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V)) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V))) | |
10 | r19.23v 3182 | . . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V)) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ (V × V))) | |
11 | 10 | albii 1821 | . . . 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 1539 ∈ wcel 2106 {cab 2709 ∀wral 3061 ∃wrex 3070 Vcvv 3474 ⊆ wss 3948 ∪ ciun 4997 × cxp 5674 Rel wrel 5681 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ral 3062 df-rex 3071 df-v 3476 df-in 3955 df-ss 3965 df-iun 4999 df-rel 5683 |
This theorem is referenced by: reluni 5818 eliunxp 5837 opeliunxp2 5838 dfco2 6244 coiun 6255 fvn0ssdmfun 7076 opeliunxp2f 8194 fsumcom2 15719 fprodcom2 15927 imasaddfnlem 17473 imasvscafn 17482 gsum2d2lem 19840 gsum2d2 19841 gsumcom2 19842 dprd2d2 19913 cnextrel 23566 reldv 25386 dfcnv2 31896 gsumpart 32202 cvmliftlem1 34271 cnviun 42391 coiun1 42393 eliunxp2 46999 |
Copyright terms: Public domain | W3C validator |