Definition df-cf 4828

Description: Define the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx (Roman numeral 30). See cfval 4918 for its value and a description.

Assertion

Ref	Expression
df-cf	|- cf = {<.x, y>. | (x e. On /\ y = |^|{z | E.w(z = (card` w) /\ (w (_ x /\ A.v e. x E.u e. w v (_ u))})}

Distinct variable group:   x,y,z,w,v,u

Detailed syntax breakdown of Definition df-cf

Step	Hyp	Ref	Expression
1		ccf 4825	. 2 class cf
2		vx	. . . . . 6 set x
3	2	cv 957	. . . . 5 class x
4		con0 2954	. . . . 5 class On
5	3, 4	wcel 960	. . . 4 wff x e. On
6		vy	. . . . . 6 set y
7	6	cv 957	. . . . 5 class y
8		vz	. . . . . . . . . . 11 set z
9	8	cv 957	. . . . . . . . . 10 class z
10		vw	. . . . . . . . . . . 12 set w
11	10	cv 957	. . . . . . . . . . 11 class w
12		ccrd 4823	. . . . . . . . . . 11 class card
13	11, 12	cfv 3188	. . . . . . . . . 10 class (card` w)
14	9, 13	wceq 958	. . . . . . . . 9 wff z = (card` w)
15	11, 3	wss 2050	. . . . . . . . . 10 wff w (_ x
16		vv	. . . . . . . . . . . . . 14 set v
17	16	cv 957	. . . . . . . . . . . . 13 class v
18		vu	. . . . . . . . . . . . . 14 set u
19	18	cv 957	. . . . . . . . . . . . 13 class u
20	17, 19	wss 2050	. . . . . . . . . . . 12 wff v (_ u
21	20, 18, 11	wrex 1649	. . . . . . . . . . 11 wff E.u e. w v (_ u
22	21, 16, 3	wral 1648	. . . . . . . . . 10 wff A.v e. x E.u e. w v (_ u
23	15, 22	wa 223	. . . . . . . . 9 wff (w (_ x /\ A.v e. x E.u e. w v (_ u)
24	14, 23	wa 223	. . . . . . . 8 wff (z = (card` w) /\ (w (_ x /\ A.v e. x E.u e. w v (_ u))
25	24, 10	wex 982	. . . . . . 7 wff E.w(z = (card` w) /\ (w (_ x /\ A.v e. x E.u e. w v (_ u))
26	25, 8	cab 1466	. . . . . 6 class {z | E.w(z = (card` w) /\ (w (_ x /\ A.v e. x E.u e. w v (_ u))}
27	26	cint 2537	. . . . 5 class |^|{z | E.w(z = (card` w) /\ (w (_ x /\ A.v e. x E.u e. w v (_ u))}
28	7, 27	wceq 958	. . . 4 wff y = |^|{z | E.w(z = (card` w) /\ (w (_ x /\ A.v e. x E.u e. w v (_ u))}
29	5, 28	wa 223	. . 3 wff (x e. On /\ y = |^|{z | E.w(z = (card` w) /\ (w (_ x /\ A.v e. x E.u e. w v (_ u))})
30	29, 2, 6	copab 2671	. 2 class {<.x, y>. | (x e. On /\ y = |^|{z | E.w(z = (card` w) /\ (w (_ x /\ A.v e. x E.u e. w v (_ u))})}
31	1, 30	wceq 958	1 wff cf = {<.x, y>. | (x e. On /\ y = |^|{z | E.w(z = (card` w) /\ (w (_ x /\ A.v e. x E.u e. w v (_ u))})}

This definition is referenced by:  cfval 4918  cffnon 4919

Copyright terms: Public domain