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 = (℩b(b ∈ NC ∧ ∃x ∈ A b = Nc ℘1x))

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 ∈ NC
7		vx	. . . . . . . . 9 setvar x
8	7	cv 1641	. . . . . . . 8 class x
9	8	cpw1 4135	. . . . . . 7 class ℘1x
10	9	cnc 6091	. . . . . 6 class Nc ℘1x
11	4, 10	wceq 1642	. . . . 5 wff b = Nc ℘1x
12	11, 7, 1	wrex 2615	. . . 4 wff ∃x ∈ A b = Nc ℘1x
13	6, 12	wa 358	. . 3 wff (b ∈ NC ∧ ∃x ∈ A b = Nc ℘1x)
14	13, 3	cio 4337	. 2 class (℩b(b ∈ NC ∧ ∃x ∈ A b = Nc ℘1x))
15	2, 14	wceq 1642	1 wff Tc A = (℩b(b ∈ NC ∧ ∃x ∈ A b = Nc ℘1x))

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