![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-cda | Structured version Visualization version GIF version |
Description: Define cardinal number addition. Definition of cardinal sum in [Mendelson] p. 258. See cdaval 9030 for its value and a description. (Contributed by NM, 24-Sep-2004.) |
Ref | Expression |
---|---|
df-cda | ⊢ +𝑐 = (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 × {∅}) ∪ (𝑦 × {1𝑜}))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ccda 9027 | . 2 class +𝑐 | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | cvv 3231 | . . 3 class V | |
5 | 2 | cv 1522 | . . . . 5 class 𝑥 |
6 | c0 3948 | . . . . . 6 class ∅ | |
7 | 6 | csn 4210 | . . . . 5 class {∅} |
8 | 5, 7 | cxp 5141 | . . . 4 class (𝑥 × {∅}) |
9 | 3 | cv 1522 | . . . . 5 class 𝑦 |
10 | c1o 7598 | . . . . . 6 class 1𝑜 | |
11 | 10 | csn 4210 | . . . . 5 class {1𝑜} |
12 | 9, 11 | cxp 5141 | . . . 4 class (𝑦 × {1𝑜}) |
13 | 8, 12 | cun 3605 | . . 3 class ((𝑥 × {∅}) ∪ (𝑦 × {1𝑜})) |
14 | 2, 3, 4, 4, 13 | cmpt2 6692 | . 2 class (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 × {∅}) ∪ (𝑦 × {1𝑜}))) |
15 | 1, 14 | wceq 1523 | 1 wff +𝑐 = (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 × {∅}) ∪ (𝑦 × {1𝑜}))) |
Colors of variables: wff setvar class |
This definition is referenced by: cdafn 9029 cdaval 9030 |
Copyright terms: Public domain | W3C validator |