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

Definition df-cf 8393
Description: Define the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx (Roman numeral 30). See cfval 8695 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 8389 . 2  class  cf
2 vx . . 3  setvar  x
3 con0 5430 . . 3  class  On
4 vy . . . . . . . . 9  setvar  y
54cv 1451 . . . . . . . 8  class  y
6 vz . . . . . . . . . 10  setvar  z
76cv 1451 . . . . . . . . 9  class  z
8 ccrd 8387 . . . . . . . . 9  class  card
97, 8cfv 5589 . . . . . . . 8  class  ( card `  z )
105, 9wceq 1452 . . . . . . 7  wff  y  =  ( card `  z
)
112cv 1451 . . . . . . . . 9  class  x
127, 11wss 3390 . . . . . . . 8  wff  z  C_  x
13 vv . . . . . . . . . . . 12  setvar  v
1413cv 1451 . . . . . . . . . . 11  class  v
15 vu . . . . . . . . . . . 12  setvar  u
1615cv 1451 . . . . . . . . . . 11  class  u
1714, 16wss 3390 . . . . . . . . . 10  wff  v  C_  u
1817, 15, 7wrex 2757 . . . . . . . . 9  wff  E. u  e.  z  v  C_  u
1918, 13, 11wral 2756 . . . . . . . 8  wff  A. v  e.  x  E. u  e.  z  v  C_  u
2012, 19wa 376 . . . . . . 7  wff  ( z 
C_  x  /\  A. v  e.  x  E. u  e.  z  v  C_  u )
2110, 20wa 376 . . . . . 6  wff  ( y  =  ( card `  z
)  /\  ( z  C_  x  /\  A. v  e.  x  E. u  e.  z  v  C_  u ) )
2221, 6wex 1671 . . . . 5  wff  E. z
( y  =  (
card `  z )  /\  ( z  C_  x  /\  A. v  e.  x  E. u  e.  z 
v  C_  u )
)
2322, 4cab 2457 . . . 4  class  { y  |  E. z ( y  =  ( card `  z )  /\  (
z  C_  x  /\  A. v  e.  x  E. u  e.  z  v  C_  u ) ) }
2423cint 4226 . . 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 4454 . 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 1452 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 setvar class
This definition is referenced by:  cfval  8695  cff  8696
  Copyright terms: Public domain W3C validator