![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-dju | Structured version Visualization version GIF version |
Description: Disjoint union of two classes. This is a way of creating a set which contains elements corresponding to each element of 𝐴 or 𝐵, tagging each one with whether it came from 𝐴 or 𝐵. (Contributed by Jim Kingdon, 20-Jun-2022.) |
Ref | Expression |
---|---|
df-dju | ⊢ (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | 1, 2 | cdju 9889 | . 2 class (𝐴 ⊔ 𝐵) |
4 | c0 4314 | . . . . 5 class ∅ | |
5 | 4 | csn 4620 | . . . 4 class {∅} |
6 | 5, 1 | cxp 5664 | . . 3 class ({∅} × 𝐴) |
7 | c1o 8454 | . . . . 5 class 1o | |
8 | 7 | csn 4620 | . . . 4 class {1o} |
9 | 8, 2 | cxp 5664 | . . 3 class ({1o} × 𝐵) |
10 | 6, 9 | cun 3938 | . 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵)) |
11 | 3, 10 | wceq 1533 | 1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵)) |
Colors of variables: wff setvar class |
This definition is referenced by: djueq12 9895 nfdju 9898 djuex 9899 djuexb 9900 djulcl 9901 djurcl 9902 djur 9910 djuunxp 9912 eldju2ndl 9915 eldju2ndr 9916 djuun 9917 undjudom 10158 endjudisj 10159 djuen 10160 dju1dif 10163 dju1p1e2 10164 xp2dju 10167 djucomen 10168 djuassen 10169 xpdjuen 10170 mapdjuen 10171 djudom1 10173 djuxpdom 10176 djufi 10177 djuinf 10179 infdju1 10180 ficardadju 10190 pwdjudom 10207 isfin4p1 10306 alephadd 10568 canthp1lem2 10644 |
Copyright terms: Public domain | W3C validator |