Definition df-aleph 5863

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 5874, alephsuc 6014, and alephlim 5875. 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 5860	. 2 class aleph
2		vy	. . . . . 6 set y
3	2	cv 1297	. . . . 5 class y
4		vx	. . . . . . . . 9 set x
5	4	cv 1297	. . . . . . . 8 class x
6		vz	. . . . . . . . 9 set z
7	6	cv 1297	. . . . . . . 8 class z
8		csdm 5425	. . . . . . . 8 class ~<
9	5, 7, 8	wbr 3338	. . . . . . 7 wff x ~< z
10		con0 3657	. . . . . . 7 class On
11	9, 6, 10	crab 2108	. . . . . 6 class {z e. On | x ~< z}
12	11	cint 3214	. . . . 5 class |^|{z e. On | x ~< z}
13	3, 12	wceq 1298	. . . 4 wff y = |^|{z e. On | x ~< z}
14	13, 4, 2	copab 3395	. . 3 class {<.x, y>. | y = |^|{z e. On | x ~< z}}
15		com 3949	. . 3 class om
16	14, 15	crdg 5139	. 2 class rec({<.x, y>. | y = |^|{z e. On | x ~< z}}, om)
17	1, 16	wceq 1298	1 wff aleph = rec({<.x, y>. | y = |^|{z e. On | x ~< z}}, om)

This definition is referenced by:  alephfnon 5873  aleph0 5874  alephlim 5875  alephon 5876  omsubsuc 5877  alephsuc 6014  omsubsucOLD 15386

Copyright terms: Public domain