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 8846
Description: Define cardinal number addition. Definition of cardinal sum in [Mendelson] p. 258. See cdaval 8848 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 8845 . 2 class +𝑐
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cvv 3168 . . 3 class V
52cv 1473 . . . . 5 class 𝑥
6 c0 3869 . . . . . 6 class
76csn 4120 . . . . 5 class {∅}
85, 7cxp 5022 . . . 4 class (𝑥 × {∅})
93cv 1473 . . . . 5 class 𝑦
10 c1o 7413 . . . . . 6 class 1𝑜
1110csn 4120 . . . . 5 class {1𝑜}
129, 11cxp 5022 . . . 4 class (𝑦 × {1𝑜})
138, 12cun 3533 . . 3 class ((𝑥 × {∅}) ∪ (𝑦 × {1𝑜}))
142, 3, 4, 4, 13cmpt2 6525 . 2 class (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 × {∅}) ∪ (𝑦 × {1𝑜})))
151, 14wceq 1474 1 wff +𝑐 = (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 × {∅}) ∪ (𝑦 × {1𝑜})))
Colors of variables: wff setvar class
This definition is referenced by:  cdafn  8847  cdaval  8848
  Copyright terms: Public domain W3C validator