MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cf Unicode version

Definition df-cf 7574
Description: Define the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx (Roman numeral 30). See cfval 7873 for its value and a description. (Contributed by NM, 1-Apr-2004.)
Assertion
Ref Expression
df-cf  |-  cf  =  ( x  e.  On  |->  |^|
{ y  |  E. z ( y  =  ( card `  z
)  /\  ( z  C_  x  /\  A. v  e.  x  E. u  e.  z  v  C_  u ) ) } )
Distinct variable group:    v, u, x, y, z

Detailed syntax breakdown of Definition df-cf
StepHypRef Expression
1 ccf 7570 . 2  class  cf
2 vx . . 3  set  x
3 con0 4392 . . 3  class  On
4 vy . . . . . . . . 9  set  y
54cv 1622 . . . . . . . 8  class  y
6 vz . . . . . . . . . 10  set  z
76cv 1622 . . . . . . . . 9  class  z
8 ccrd 7568 . . . . . . . . 9  class  card
97, 8cfv 5255 . . . . . . . 8  class  ( card `  z )
105, 9wceq 1623 . . . . . . 7  wff  y  =  ( card `  z
)
112cv 1622 . . . . . . . . 9  class  x
127, 11wss 3152 . . . . . . . 8  wff  z  C_  x
13 vv . . . . . . . . . . . 12  set  v
1413cv 1622 . . . . . . . . . . 11  class  v
15 vu . . . . . . . . . . . 12  set  u
1615cv 1622 . . . . . . . . . . 11  class  u
1714, 16wss 3152 . . . . . . . . . 10  wff  v  C_  u
1817, 15, 7wrex 2544 . . . . . . . . 9  wff  E. u  e.  z  v  C_  u
1918, 13, 11wral 2543 . . . . . . . 8  wff  A. v  e.  x  E. u  e.  z  v  C_  u
2012, 19wa 358 . . . . . . 7  wff  ( z 
C_  x  /\  A. v  e.  x  E. u  e.  z  v  C_  u )
2110, 20wa 358 . . . . . 6  wff  ( y  =  ( card `  z
)  /\  ( z  C_  x  /\  A. v  e.  x  E. u  e.  z  v  C_  u ) )
2221, 6wex 1528 . . . . 5  wff  E. z
( y  =  (
card `  z )  /\  ( z  C_  x  /\  A. v  e.  x  E. u  e.  z 
v  C_  u )
)
2322, 4cab 2269 . . . 4  class  { y  |  E. z ( y  =  ( card `  z )  /\  (
z  C_  x  /\  A. v  e.  x  E. u  e.  z  v  C_  u ) ) }
2423cint 3862 . . 3  class  |^| { y  |  E. z ( y  =  ( card `  z )  /\  (
z  C_  x  /\  A. v  e.  x  E. u  e.  z  v  C_  u ) ) }
252, 3, 24cmpt 4077 . 2  class  ( x  e.  On  |->  |^| { y  |  E. z ( y  =  ( card `  z )  /\  (
z  C_  x  /\  A. v  e.  x  E. u  e.  z  v  C_  u ) ) } )
261, 25wceq 1623 1  wff  cf  =  ( x  e.  On  |->  |^|
{ y  |  E. z ( y  =  ( card `  z
)  /\  ( z  C_  x  /\  A. v  e.  x  E. u  e.  z  v  C_  u ) ) } )
Colors of variables: wff set class
This definition is referenced by:  cfval  7873  cff  7874
  Copyright terms: Public domain W3C validator