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 9282
Description: Define cardinal number addition. Definition of cardinal sum in [Mendelson] p. 258. See cdaval 9284 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 9281 . 2 class +𝑐
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cvv 3402 . . 3 class V
52cv 1636 . . . . 5 class 𝑥
6 c0 4127 . . . . . 6 class
76csn 4381 . . . . 5 class {∅}
85, 7cxp 5320 . . . 4 class (𝑥 × {∅})
93cv 1636 . . . . 5 class 𝑦
10 c1o 7796 . . . . . 6 class 1𝑜
1110csn 4381 . . . . 5 class {1𝑜}
129, 11cxp 5320 . . . 4 class (𝑦 × {1𝑜})
138, 12cun 3778 . . 3 class ((𝑥 × {∅}) ∪ (𝑦 × {1𝑜}))
142, 3, 4, 4, 13cmpt2 6883 . 2 class (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 × {∅}) ∪ (𝑦 × {1𝑜})))
151, 14wceq 1637 1 wff +𝑐 = (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 × {∅}) ∪ (𝑦 × {1𝑜})))
Colors of variables: wff setvar class
This definition is referenced by:  cdafn  9283  cdaval  9284
  Copyright terms: Public domain W3C validator