Definition df-cda 6066

Description: Define cardinal number addition. Definition of cardinal sum in [Mendelson] p. 258. See cdavali 6068 for its value and a description.

Assertion

Ref	Expression
df-cda	|- +c = {<.<.x, y>., z>. | z = ((x X. {(/)}) u. (y X. {1o}))}

Distinct variable group:   x,y,z

Detailed syntax breakdown of Definition df-cda

Step	Hyp	Ref	Expression
1		ccda 6065	. 2 class +c
2		vz	. . . . 5 set z
3	2	cv 1297	. . . 4 class z
4		vx	. . . . . . 7 set x
5	4	cv 1297	. . . . . 6 class x
6		c0 2875	. . . . . . 7 class (/)
7	6	csn 3044	. . . . . 6 class {(/)}
8	5, 7	cxp 3984	. . . . 5 class (x X. {(/)})
9		vy	. . . . . . 7 set y
10	9	cv 1297	. . . . . 6 class y
11		c1o 5172	. . . . . . 7 class 1o
12	11	csn 3044	. . . . . 6 class {1o}
13	10, 12	cxp 3984	. . . . 5 class (y X. {1o})
14	8, 13	cun 2591	. . . 4 class ((x X. {(/)}) u. (y X. {1o}))
15	3, 14	wceq 1298	. . 3 wff z = ((x X. {(/)}) u. (y X. {1o}))
16	15, 4, 9, 2	copab2 4885	. 2 class {<.<.x, y>., z>. | z = ((x X. {(/)}) u. (y X. {1o}))}
17	1, 16	wceq 1298	1 wff +c = {<.<.x, y>., z>. | z = ((x X. {(/)}) u. (y X. {1o}))}

This definition is referenced by:  cdaval 6067

Copyright terms: Public domain