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 ∈ On ∧ y = ∩{z∣∃w(z = (card ‘w) ∧ (w ⊆ x ∧ ∀v ∈ x ∃u ∈ 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 ∈ 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 ∃u ∈ w v ⊆ u
22	21, 16, 3	wral 1201	. . . . . . . . . 10 wff ∀v ∈ x ∃u ∈ w v ⊆ u
23	15, 22	wa 196	. . . . . . . . 9 wff (w ⊆ x ∧ ∀v ∈ x ∃u ∈ w v ⊆ u)
24	14, 23	wa 196	. . . . . . . 8 wff (z = (card ‘w) ∧ (w ⊆ x ∧ ∀v ∈ x ∃u ∈ w v ⊆ u))
25	24, 10	wex 678	. . . . . . 7 wff ∃w(z = (card ‘w) ∧ (w ⊆ x ∧ ∀v ∈ x ∃u ∈ w v ⊆ u))
26	25, 8	cab 1090	. . . . . 6 class {z∣∃w(z = (card ‘w) ∧ (w ⊆ x ∧ ∀v ∈ x ∃u ∈ w v ⊆ u))}
27	26	cint 1965	. . . . 5 class ∩{z∣∃w(z = (card ‘w) ∧ (w ⊆ x ∧ ∀v ∈ x ∃u ∈ w v ⊆ u))}
28	7, 27	wceq 1091	. . . 4 wff y = ∩{z∣∃w(z = (card ‘w) ∧ (w ⊆ x ∧ ∀v ∈ x ∃u ∈ w v ⊆ u))}
29	5, 28	wa 196	. . 3 wff (x ∈ On ∧ y = ∩{z∣∃w(z = (card ‘w) ∧ (w ⊆ x ∧ ∀v ∈ x ∃u ∈ w v ⊆ u))})
30	29, 2, 6	copab 2055	. 2 class {⟨x, y⟩∣(x ∈ On ∧ y = ∩{z∣∃w(z = (card ‘w) ∧ (w ⊆ x ∧ ∀v ∈ x ∃u ∈ w v ⊆ u))})}
31	1, 30	wceq 1091	1 wff cf = {⟨x, y⟩∣(x ∈ On ∧ y = ∩{z∣∃w(z = (card ‘w) ∧ (w ⊆ x ∧ ∀v ∈ x ∃u ∈ w v ⊆ u))})}

This definition is referenced by:  cfval 3701  cffnon 3702

metamath.org