Definition df-tc 6103

Description: Define the type-raising operation on a cardinal number. This is the unique cardinal containing the unit power classes of the elements of the given cardinal. Definition adapted from [Rosser] p. 528. (Contributed by Scott Fenton, 24-Feb-2015.)

Assertion

Ref	Expression
df-tc	|- Tc A = (iotab(b e. NC /\ E.x e. A b = Nc ~P1 x))

Distinct variable group:   A,b,x

Detailed syntax breakdown of Definition df-tc

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	ctc 6093	. 2 class Tc A
3		vb	. . . . . 6 setvar b
4	3	cv 1641	. . . . 5 class b
5		cncs 6088	. . . . 5 class NC
6	4, 5	wcel 1710	. . . 4 wff b e. NC
7		vx	. . . . . . . . 9 setvar x
8	7	cv 1641	. . . . . . . 8 class x
9	8	cpw1 4135	. . . . . . 7 class ~P1 x
10	9	cnc 6091	. . . . . 6 class Nc ~P1 x
11	4, 10	wceq 1642	. . . . 5 wff b = Nc ~P1 x
12	11, 7, 1	wrex 2615	. . . 4 wff E.x e. A b = Nc ~P1 x
13	6, 12	wa 358	. . 3 wff (b e. NC /\ E.x e. A b = Nc ~P1 x)
14	13, 3	cio 4337	. 2 class (iotab(b e. NC /\ E.x e. A b = Nc ~P1 x))
15	2, 14	wceq 1642	1 wff Tc A = (iotab(b e. NC /\ E.x e. A b = Nc ~P1 x))

This definition is referenced by:  tcex  6157  tceq  6158  tccl  6160  eqtc  6161  tcfnex  6244