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

Definition df-cda 8987
 Description: Define cardinal number addition. Definition of cardinal sum in [Mendelson] p. 258. See cdaval 8989 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 8986 . 2 class +𝑐
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cvv 3198 . . 3 class V
52cv 1481 . . . . 5 class 𝑥
6 c0 3913 . . . . . 6 class
76csn 4175 . . . . 5 class {∅}
85, 7cxp 5110 . . . 4 class (𝑥 × {∅})
93cv 1481 . . . . 5 class 𝑦
10 c1o 7550 . . . . . 6 class 1𝑜
1110csn 4175 . . . . 5 class {1𝑜}
129, 11cxp 5110 . . . 4 class (𝑦 × {1𝑜})
138, 12cun 3570 . . 3 class ((𝑥 × {∅}) ∪ (𝑦 × {1𝑜}))
142, 3, 4, 4, 13cmpt2 6649 . 2 class (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 × {∅}) ∪ (𝑦 × {1𝑜})))
151, 14wceq 1482 1 wff +𝑐 = (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 × {∅}) ∪ (𝑦 × {1𝑜})))
 Colors of variables: wff setvar class This definition is referenced by:  cdafn  8988  cdaval  8989
 Copyright terms: Public domain W3C validator