![]() |
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 9119 | . 2 class (𝐴 ⊔ 𝐵) |
4 | c0 4172 | . . . . 5 class ∅ | |
5 | 4 | csn 4435 | . . . 4 class {∅} |
6 | 5, 1 | cxp 5401 | . . 3 class ({∅} × 𝐴) |
7 | c1o 7896 | . . . . 5 class 1o | |
8 | 7 | csn 4435 | . . . 4 class {1o} |
9 | 8, 2 | cxp 5401 | . . 3 class ({1o} × 𝐵) |
10 | 6, 9 | cun 3820 | . 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵)) |
11 | 3, 10 | wceq 1508 | 1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵)) |
Colors of variables: wff setvar class |
This definition is referenced by: djueq12 9125 nfdju 9128 djuex 9129 djuexb 9130 djulcl 9131 djurcl 9132 djur 9140 djuunxp 9142 eldju2ndl 9145 eldju2ndr 9146 djuun 9147 cdadju 9388 undjudom 9389 endjudisj 9390 djuen 9391 dju1dif 9394 dju1p1e2 9395 xp2dju 9398 djucomen 9399 djuassen 9400 xpdjuen 9401 mapdjuen 9402 djudom1 9404 djuxpdom 9407 djufi 9408 djuinf 9410 infdju1 9411 pwdjudom 9434 isfin4p1 9533 alephadd 9795 canthp1lem2 9871 |
Copyright terms: Public domain | W3C validator |