Definition df-cf 9981

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

Assertion

Ref	Expression
df-cf	⊢ cf = (𝑥 ∈ On ↦ ∩ {𝑦 ∣ ∃𝑧(𝑦 = (card‘𝑧) ∧ (𝑧 ⊆ 𝑥 ∧ ∀𝑣 ∈ 𝑥 ∃𝑢 ∈ 𝑧 𝑣 ⊆ 𝑢))})

Distinct variable group:   𝑣,𝑢,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-cf

Step	Hyp	Ref	Expression
1		ccf 9977	. 2 class cf
2		vx	. . 3 setvar 𝑥
3		con0 6384	. . 3 class On
4		vy	. . . . . . . . 9 setvar 𝑦
5	4	cv 1539	. . . . . . . 8 class 𝑦
6		vz	. . . . . . . . . 10 setvar 𝑧
7	6	cv 1539	. . . . . . . . 9 class 𝑧
8		ccrd 9975	. . . . . . . . 9 class card
9	7, 8	cfv 6561	. . . . . . . 8 class (card‘𝑧)
10	5, 9	wceq 1540	. . . . . . 7 wff 𝑦 = (card‘𝑧)
11	2	cv 1539	. . . . . . . . 9 class 𝑥
12	7, 11	wss 3951	. . . . . . . 8 wff 𝑧 ⊆ 𝑥
13		vv	. . . . . . . . . . . 12 setvar 𝑣
14	13	cv 1539	. . . . . . . . . . 11 class 𝑣
15		vu	. . . . . . . . . . . 12 setvar 𝑢
16	15	cv 1539	. . . . . . . . . . 11 class 𝑢
17	14, 16	wss 3951	. . . . . . . . . 10 wff 𝑣 ⊆ 𝑢
18	17, 15, 7	wrex 3070	. . . . . . . . 9 wff ∃𝑢 ∈ 𝑧 𝑣 ⊆ 𝑢
19	18, 13, 11	wral 3061	. . . . . . . 8 wff ∀𝑣 ∈ 𝑥 ∃𝑢 ∈ 𝑧 𝑣 ⊆ 𝑢
20	12, 19	wa 395	. . . . . . 7 wff (𝑧 ⊆ 𝑥 ∧ ∀𝑣 ∈ 𝑥 ∃𝑢 ∈ 𝑧 𝑣 ⊆ 𝑢)
21	10, 20	wa 395	. . . . . 6 wff (𝑦 = (card‘𝑧) ∧ (𝑧 ⊆ 𝑥 ∧ ∀𝑣 ∈ 𝑥 ∃𝑢 ∈ 𝑧 𝑣 ⊆ 𝑢))
22	21, 6	wex 1779	. . . . 5 wff ∃𝑧(𝑦 = (card‘𝑧) ∧ (𝑧 ⊆ 𝑥 ∧ ∀𝑣 ∈ 𝑥 ∃𝑢 ∈ 𝑧 𝑣 ⊆ 𝑢))
23	22, 4	cab 2714	. . . 4 class {𝑦 ∣ ∃𝑧(𝑦 = (card‘𝑧) ∧ (𝑧 ⊆ 𝑥 ∧ ∀𝑣 ∈ 𝑥 ∃𝑢 ∈ 𝑧 𝑣 ⊆ 𝑢))}
24	23	cint 4946	. . 3 class ∩ {𝑦 ∣ ∃𝑧(𝑦 = (card‘𝑧) ∧ (𝑧 ⊆ 𝑥 ∧ ∀𝑣 ∈ 𝑥 ∃𝑢 ∈ 𝑧 𝑣 ⊆ 𝑢))}
25	2, 3, 24	cmpt 5225	. 2 class (𝑥 ∈ On ↦ ∩ {𝑦 ∣ ∃𝑧(𝑦 = (card‘𝑧) ∧ (𝑧 ⊆ 𝑥 ∧ ∀𝑣 ∈ 𝑥 ∃𝑢 ∈ 𝑧 𝑣 ⊆ 𝑢))})
26	1, 25	wceq 1540	1 wff cf = (𝑥 ∈ On ↦ ∩ {𝑦 ∣ ∃𝑧(𝑦 = (card‘𝑧) ∧ (𝑧 ⊆ 𝑥 ∧ ∀𝑣 ∈ 𝑥 ∃𝑢 ∈ 𝑧 𝑣 ⊆ 𝑢))})

This definition is referenced by:  cfval  10287  cff  10288