New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-tc GIF version

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
StepHypRef Expression
1 cA . . 3 class A
21ctc 6093 . 2 class Tc A
3 vb . . . . . 6 setvar b
43cv 1641 . . . . 5 class b
5 cncs 6088 . . . . 5 class NC
64, 5wcel 1710 . . . 4 wff b NC
7 vx . . . . . . . . 9 setvar x
87cv 1641 . . . . . . . 8 class x
98cpw1 4135 . . . . . . 7 class 1x
109cnc 6091 . . . . . 6 class Nc 1x
114, 10wceq 1642 . . . . 5 wff b = Nc 1x
1211, 7, 1wrex 2615 . . . 4 wff x A b = Nc 1x
136, 12wa 358 . . 3 wff (b NC x A b = Nc 1x)
1413, 3cio 4337 . 2 class (℩b(b NC x A b = Nc 1x))
152, 14wceq 1642 1 wff Tc A = (℩b(b NC x A b = Nc 1x))
 Colors of variables: wff setvar class This definition is referenced by:  tcex  6157  tceq  6158  tccl  6160  eqtc  6161  tcfnex  6244
 Copyright terms: Public domain W3C validator