Definition df-aleph 4789

Description: Define the aleph function. Our definition expresses Definition 12 of [Suppes] p. 229 in a closed form, from which we derive the recursive definition as theorems aleph0 4835, alephsuc 4838, and alephlim 4836. The aleph function provides a one-to-one, onto mapping from the ordinal numbers to the infinite cardinal numbers. Roughly, any aleph is the smallest infinite cardinal number whose size is strictly greater than any aleph before it.

Assertion

Ref	Expression
df-aleph	|- aleph = rec({<.x, y>. | y = |^|{z e. On | x ~< z}}, om)

Distinct variable group:   x,y,z

Detailed syntax breakdown of Definition df-aleph

Step	Hyp	Ref	Expression
1		cale 4786	. 2 class aleph
2		vy	. . . . . 6 set y
3	2	cv 952	. . . . 5 class y
4		vx	. . . . . . . . 9 set x
5	4	cv 952	. . . . . . . 8 class x
6		vz	. . . . . . . . 9 set z
7	6	cv 952	. . . . . . . 8 class z
8		csdm 4350	. . . . . . . 8 class ~<
9	5, 7, 8	wbr 2609	. . . . . . 7 wff x ~< z
10		con0 2938	. . . . . . 7 class On
11	9, 6, 10	crab 1640	. . . . . 6 class {z e. On | x ~< z}
12	11	cint 2523	. . . . 5 class |^|{z e. On | x ~< z}
13	3, 12	wceq 953	. . . 4 wff y = |^|{z e. On | x ~< z}
14	13, 4, 2	copab 2656	. . 3 class {<.x, y>. | y = |^|{z e. On | x ~< z}}
15		com 3121	. . 3 class om
16	14, 15	crdg 3916	. 2 class rec({<.x, y>. | y = |^|{z e. On | x ~< z}}, om)
17	1, 16	wceq 953	1 wff aleph = rec({<.x, y>. | y = |^|{z e. On | x ~< z}}, om)

This definition is referenced by:  alephfnon 4834  aleph0 4835  alephlim 4836  alephon 4837  alephsuc 4838

Copyright terms: Public domain