Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cf Structured version   Visualization version   GIF version

Definition df-cf 9223
 Description: Define the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx (Roman numeral 30). See cfval 9522 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
StepHypRef Expression
1 ccf 9219 . 2 class cf
2 vx . . 3 setvar 𝑥
3 con0 6073 . . 3 class On
4 vy . . . . . . . . 9 setvar 𝑦
54cv 1524 . . . . . . . 8 class 𝑦
6 vz . . . . . . . . . 10 setvar 𝑧
76cv 1524 . . . . . . . . 9 class 𝑧
8 ccrd 9217 . . . . . . . . 9 class card
97, 8cfv 6232 . . . . . . . 8 class (card‘𝑧)
105, 9wceq 1525 . . . . . . 7 wff 𝑦 = (card‘𝑧)
112cv 1524 . . . . . . . . 9 class 𝑥
127, 11wss 3865 . . . . . . . 8 wff 𝑧𝑥
13 vv . . . . . . . . . . . 12 setvar 𝑣
1413cv 1524 . . . . . . . . . . 11 class 𝑣
15 vu . . . . . . . . . . . 12 setvar 𝑢
1615cv 1524 . . . . . . . . . . 11 class 𝑢
1714, 16wss 3865 . . . . . . . . . 10 wff 𝑣𝑢
1817, 15, 7wrex 3108 . . . . . . . . 9 wff 𝑢𝑧 𝑣𝑢
1918, 13, 11wral 3107 . . . . . . . 8 wff 𝑣𝑥𝑢𝑧 𝑣𝑢
2012, 19wa 396 . . . . . . 7 wff (𝑧𝑥 ∧ ∀𝑣𝑥𝑢𝑧 𝑣𝑢)
2110, 20wa 396 . . . . . 6 wff (𝑦 = (card‘𝑧) ∧ (𝑧𝑥 ∧ ∀𝑣𝑥𝑢𝑧 𝑣𝑢))
2221, 6wex 1765 . . . . 5 wff 𝑧(𝑦 = (card‘𝑧) ∧ (𝑧𝑥 ∧ ∀𝑣𝑥𝑢𝑧 𝑣𝑢))
2322, 4cab 2777 . . . 4 class {𝑦 ∣ ∃𝑧(𝑦 = (card‘𝑧) ∧ (𝑧𝑥 ∧ ∀𝑣𝑥𝑢𝑧 𝑣𝑢))}
2423cint 4788 . . 3 class {𝑦 ∣ ∃𝑧(𝑦 = (card‘𝑧) ∧ (𝑧𝑥 ∧ ∀𝑣𝑥𝑢𝑧 𝑣𝑢))}
252, 3, 24cmpt 5047 . 2 class (𝑥 ∈ On ↦ {𝑦 ∣ ∃𝑧(𝑦 = (card‘𝑧) ∧ (𝑧𝑥 ∧ ∀𝑣𝑥𝑢𝑧 𝑣𝑢))})
261, 25wceq 1525 1 wff cf = (𝑥 ∈ On ↦ {𝑦 ∣ ∃𝑧(𝑦 = (card‘𝑧) ∧ (𝑧𝑥 ∧ ∀𝑣𝑥𝑢𝑧 𝑣𝑢))})
 Colors of variables: wff setvar class This definition is referenced by:  cfval  9522  cff  9523
 Copyright terms: Public domain W3C validator