Definition df-cf 8767

Description: Define the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx (Roman numeral 30). See cfval 9069 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

Step	Hyp	Ref	Expression
1		ccf 8763	. 2 class cf
2		vx	. . 3 setvar x
3		con0 5723	. . 3 class On
4		vy	. . . . . . . . 9 setvar y
5	4	cv 1482	. . . . . . . 8 class y
6		vz	. . . . . . . . . 10 setvar z
7	6	cv 1482	. . . . . . . . 9 class z
8		ccrd 8761	. . . . . . . . 9 class card
9	7, 8	cfv 5888	. . . . . . . 8 class ( card ` z )
10	5, 9	wceq 1483	. . . . . . 7 wff y = ( card ` z )
11	2	cv 1482	. . . . . . . . 9 class x
12	7, 11	wss 3574	. . . . . . . 8 wff z C_ x
13		vv	. . . . . . . . . . . 12 setvar v
14	13	cv 1482	. . . . . . . . . . 11 class v
15		vu	. . . . . . . . . . . 12 setvar u
16	15	cv 1482	. . . . . . . . . . 11 class u
17	14, 16	wss 3574	. . . . . . . . . 10 wff v C_ u
18	17, 15, 7	wrex 2913	. . . . . . . . 9 wff E. u e. z v C_ u
19	18, 13, 11	wral 2912	. . . . . . . 8 wff A. v e. x E. u e. z v C_ u
20	12, 19	wa 384	. . . . . . 7 wff ( z C_ x /\ A. v e. x E. u e. z v C_ u )
21	10, 20	wa 384	. . . . . 6 wff ( y = ( card ` z ) /\ ( z C_ x /\ A. v e. x E. u e. z v C_ u ) )
22	21, 6	wex 1704	. . . . 5 wff E. z ( y = ( card ` z ) /\ ( z C_ x /\ A. v e. x E. u e. z v C_ u ) )
23	22, 4	cab 2608	. . . 4 class { y | E. z ( y = ( card ` z ) /\ ( z C_ x /\ A. v e. x E. u e. z v C_ u ) ) }
24	23	cint 4475	. . 3 class |^| { y | E. z ( y = ( card ` z ) /\ ( z C_ x /\ A. v e. x E. u e. z v C_ u ) ) }
25	2, 3, 24	cmpt 4729	. 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 ) ) } )
26	1, 25	wceq 1483	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 ) ) } )

This definition is referenced by:  cfval  9069  cff  9070