![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > unixp | Structured version Visualization version GIF version |
Description: The double class union of a nonempty Cartesian product is the union of it members. (Contributed by NM, 17-Sep-2006.) |
Ref | Expression |
---|---|
unixp | ⊢ ((𝐴 × 𝐵) ≠ ∅ → ∪ ∪ (𝐴 × 𝐵) = (𝐴 ∪ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relxp 5717 | . . 3 ⊢ Rel (𝐴 × 𝐵) | |
2 | relfld 6305 | . . 3 ⊢ (Rel (𝐴 × 𝐵) → ∪ ∪ (𝐴 × 𝐵) = (dom (𝐴 × 𝐵) ∪ ran (𝐴 × 𝐵))) | |
3 | 1, 2 | ax-mp 5 | . 2 ⊢ ∪ ∪ (𝐴 × 𝐵) = (dom (𝐴 × 𝐵) ∪ ran (𝐴 × 𝐵)) |
4 | xpeq2 5720 | . . . . 5 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = (𝐴 × ∅)) | |
5 | xp0 6188 | . . . . 5 ⊢ (𝐴 × ∅) = ∅ | |
6 | 4, 5 | eqtrdi 2790 | . . . 4 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = ∅) |
7 | 6 | necon3i 2975 | . . 3 ⊢ ((𝐴 × 𝐵) ≠ ∅ → 𝐵 ≠ ∅) |
8 | xpeq1 5713 | . . . . 5 ⊢ (𝐴 = ∅ → (𝐴 × 𝐵) = (∅ × 𝐵)) | |
9 | 0xp 5797 | . . . . 5 ⊢ (∅ × 𝐵) = ∅ | |
10 | 8, 9 | eqtrdi 2790 | . . . 4 ⊢ (𝐴 = ∅ → (𝐴 × 𝐵) = ∅) |
11 | 10 | necon3i 2975 | . . 3 ⊢ ((𝐴 × 𝐵) ≠ ∅ → 𝐴 ≠ ∅) |
12 | dmxp 5952 | . . . 4 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴) | |
13 | rnxp 6200 | . . . 4 ⊢ (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵) | |
14 | uneq12 4180 | . . . 4 ⊢ ((dom (𝐴 × 𝐵) = 𝐴 ∧ ran (𝐴 × 𝐵) = 𝐵) → (dom (𝐴 × 𝐵) ∪ ran (𝐴 × 𝐵)) = (𝐴 ∪ 𝐵)) | |
15 | 12, 13, 14 | syl2an 595 | . . 3 ⊢ ((𝐵 ≠ ∅ ∧ 𝐴 ≠ ∅) → (dom (𝐴 × 𝐵) ∪ ran (𝐴 × 𝐵)) = (𝐴 ∪ 𝐵)) |
16 | 7, 11, 15 | syl2anc 583 | . 2 ⊢ ((𝐴 × 𝐵) ≠ ∅ → (dom (𝐴 × 𝐵) ∪ ran (𝐴 × 𝐵)) = (𝐴 ∪ 𝐵)) |
17 | 3, 16 | eqtrid 2786 | 1 ⊢ ((𝐴 × 𝐵) ≠ ∅ → ∪ ∪ (𝐴 × 𝐵) = (𝐴 ∪ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ≠ wne 2942 ∪ cun 3968 ∅c0 4347 ∪ cuni 4931 × cxp 5697 dom cdm 5699 ran crn 5700 Rel wrel 5704 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2105 ax-9 2113 ax-11 2153 ax-12 2173 ax-ext 2705 ax-sep 5320 ax-nul 5327 ax-pr 5450 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-sb 2065 df-clab 2712 df-cleq 2726 df-clel 2813 df-ne 2943 df-ral 3064 df-rex 3073 df-rab 3439 df-v 3484 df-dif 3973 df-un 3975 df-ss 3987 df-nul 4348 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-br 5170 df-opab 5232 df-xp 5705 df-rel 5706 df-cnv 5707 df-dm 5709 df-rn 5710 |
This theorem is referenced by: unixpid 6314 rankxpl 9940 rankxplim2 9945 rankxplim3 9946 rankxpsuc 9947 |
Copyright terms: Public domain | W3C validator |