MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cda Structured version   Visualization version   GIF version

Definition df-cda 9213
Description: Define cardinal number addition. Definition of cardinal sum in [Mendelson] p. 258. See cdaval 9215 for its value and a description. (Contributed by NM, 24-Sep-2004.)
Assertion
Ref Expression
df-cda +𝑐 = (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 × {∅}) ∪ (𝑦 × {1𝑜})))
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-cda
StepHypRef Expression
1 ccda 9212 . 2 class +𝑐
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cvv 3355 . . 3 class V
52cv 1633 . . . . 5 class 𝑥
6 c0 4073 . . . . . 6 class
76csn 4326 . . . . 5 class {∅}
85, 7cxp 5261 . . . 4 class (𝑥 × {∅})
93cv 1633 . . . . 5 class 𝑦
10 c1o 7727 . . . . . 6 class 1𝑜
1110csn 4326 . . . . 5 class {1𝑜}
129, 11cxp 5261 . . . 4 class (𝑦 × {1𝑜})
138, 12cun 3727 . . 3 class ((𝑥 × {∅}) ∪ (𝑦 × {1𝑜}))
142, 3, 4, 4, 13cmpt2 6814 . 2 class (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 × {∅}) ∪ (𝑦 × {1𝑜})))
151, 14wceq 1634 1 wff +𝑐 = (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 × {∅}) ∪ (𝑦 × {1𝑜})))
Colors of variables: wff setvar class
This definition is referenced by:  cdafn  9214  cdaval  9215
  Copyright terms: Public domain W3C validator