Definition df-cf 3625

Description: Define the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx. See cfval 3701 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(s):   x,y,z,w,v,u

Detailed syntax breakdown of Definition df-cf

Step	Hyp	Ref	Expression
1		ccf 3622	. 2 class cf
2		vx	. . . . . 6 set x
3	2	cv 1089	. . . . 5 class x
4		con0 2199	. . . . 5 class On
5	3, 4	wcel 1092	. . . 4 wff x e. On
6		vy	. . . . . 6 set y
7	6	cv 1089	. . . . 5 class y
8		vz	. . . . . . . . . . 11 set z
9	8	cv 1089	. . . . . . . . . 10 class z
10		vw	. . . . . . . . . . . 12 set w
11	10	cv 1089	. . . . . . . . . . 11 class w
12		ccrd 3620	. . . . . . . . . . 11 class card
13	11, 12	cfv 2422	. . . . . . . . . 10 class (card` w)
14	9, 13	wceq 1091	. . . . . . . . 9 wff z = (card` w)
15	11, 3	wss 1487	. . . . . . . . . 10 wff w (_ x
16		vv	. . . . . . . . . . . . . 14 set v
17	16	cv 1089	. . . . . . . . . . . . 13 class v
18		vu	. . . . . . . . . . . . . 14 set u
19	18	cv 1089	. . . . . . . . . . . . 13 class u
20	17, 19	wss 1487	. . . . . . . . . . . 12 wff v (_ u
21	20, 18, 11	wrex 1202	. . . . . . . . . . 11 wff E.u e. w v (_ u
22	21, 16, 3	wral 1201	. . . . . . . . . 10 wff A.v e. x E.u e. w v (_ u
23	15, 22	wa 196	. . . . . . . . 9 wff (w (_ x /\ A.v e. x E.u e. w v (_ u)
24	14, 23	wa 196	. . . . . . . 8 wff (z = (card` w) /\ (w (_ x /\ A.v e. x E.u e. w v (_ u))
25	24, 10	wex 678	. . . . . . 7 wff E.w(z = (card` w) /\ (w (_ x /\ A.v e. x E.u e. w v (_ u))
26	25, 8	cab 1090	. . . . . 6 class {z | E.w(z = (card` w) /\ (w (_ x /\ A.v e. x E.u e. w v (_ u))}
27	26	cint 1965	. . . . 5 class |^|{z | E.w(z = (card` w) /\ (w (_ x /\ A.v e. x E.u e. w v (_ u))}
28	7, 27	wceq 1091	. . . 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 196	. . 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 2055	. 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 1091	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 3701  cffnon 3702

metamath.org