Metamath Proof Explorer

Definition df-cf

Description: Define the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx (Roman numeral 30). See cfval for its value and a description. (Contributed by NM, 1-Apr-2004)

Ref Expression
Assertion 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 ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccf 
 |-  cf
1 vx 
 |-  x
2 con0 
 |-  On
3 vy 
 |-  y
4 vz 
 |-  z
5 3 cv 
 |-  y
6 ccrd 
 |-  card
7 4 cv 
 |-  z
8 7 6 cfv 
 |-  ( card ` z )
9 5 8 wceq 
 |-  y = ( card ` z )
10 1 cv 
 |-  x
11 7 10 wss 
 |-  z C_ x
12 vv 
 |-  v
13 vu 
 |-  u
14 12 cv 
 |-  v
15 13 cv 
 |-  u
16 14 15 wss 
 |-  v C_ u
17 16 13 7 wrex 
 |-  E. u e. z v C_ u
18 17 12 10 wral 
 |-  A. v e. x E. u e. z v C_ u
19 11 18 wa 
 |-  ( z C_ x /\ A. v e. x E. u e. z v C_ u )
20 9 19 wa 
 |-  ( y = ( card ` z ) /\ ( z C_ x /\ A. v e. x E. u e. z v C_ u ) )
21 20 4 wex 
 |-  E. z ( y = ( card ` z ) /\ ( z C_ x /\ A. v e. x E. u e. z v C_ u ) )
22 21 3 cab 
 |-  { y | E. z ( y = ( card ` z ) /\ ( z C_ x /\ A. v e. x E. u e. z v C_ u ) ) }
23 22 cint 
 |-  |^| { y | E. z ( y = ( card ` z ) /\ ( z C_ x /\ A. v e. x E. u e. z v C_ u ) ) }
24 1 2 23 cmpt 
 |-  ( x e. On |-> |^| { y | E. z ( y = ( card ` z ) /\ ( z C_ x /\ A. v e. x E. u e. z v C_ u ) ) } )
25 0 24 wceq 
 |-  cf = ( x e. On |-> |^| { y | E. z ( y = ( card ` z ) /\ ( z C_ x /\ A. v e. x E. u e. z v C_ u ) ) } )