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

Definition df-cf 8650
Description: Define the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx (Roman numeral 30). See cfval 8952 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 8646 . 2 class cf
2 vx . . 3 setvar 𝑥
3 con0 5640 . . 3 class On
4 vy . . . . . . . . 9 setvar 𝑦
54cv 1474 . . . . . . . 8 class 𝑦
6 vz . . . . . . . . . 10 setvar 𝑧
76cv 1474 . . . . . . . . 9 class 𝑧
8 ccrd 8644 . . . . . . . . 9 class card
97, 8cfv 5804 . . . . . . . 8 class (card‘𝑧)
105, 9wceq 1475 . . . . . . 7 wff 𝑦 = (card‘𝑧)
112cv 1474 . . . . . . . . 9 class 𝑥
127, 11wss 3540 . . . . . . . 8 wff 𝑧𝑥
13 vv . . . . . . . . . . . 12 setvar 𝑣
1413cv 1474 . . . . . . . . . . 11 class 𝑣
15 vu . . . . . . . . . . . 12 setvar 𝑢
1615cv 1474 . . . . . . . . . . 11 class 𝑢
1714, 16wss 3540 . . . . . . . . . 10 wff 𝑣𝑢
1817, 15, 7wrex 2897 . . . . . . . . 9 wff 𝑢𝑧 𝑣𝑢
1918, 13, 11wral 2896 . . . . . . . 8 wff 𝑣𝑥𝑢𝑧 𝑣𝑢
2012, 19wa 383 . . . . . . 7 wff (𝑧𝑥 ∧ ∀𝑣𝑥𝑢𝑧 𝑣𝑢)
2110, 20wa 383 . . . . . 6 wff (𝑦 = (card‘𝑧) ∧ (𝑧𝑥 ∧ ∀𝑣𝑥𝑢𝑧 𝑣𝑢))
2221, 6wex 1695 . . . . 5 wff 𝑧(𝑦 = (card‘𝑧) ∧ (𝑧𝑥 ∧ ∀𝑣𝑥𝑢𝑧 𝑣𝑢))
2322, 4cab 2596 . . . 4 class {𝑦 ∣ ∃𝑧(𝑦 = (card‘𝑧) ∧ (𝑧𝑥 ∧ ∀𝑣𝑥𝑢𝑧 𝑣𝑢))}
2423cint 4410 . . 3 class {𝑦 ∣ ∃𝑧(𝑦 = (card‘𝑧) ∧ (𝑧𝑥 ∧ ∀𝑣𝑥𝑢𝑧 𝑣𝑢))}
252, 3, 24cmpt 4643 . 2 class (𝑥 ∈ On ↦ {𝑦 ∣ ∃𝑧(𝑦 = (card‘𝑧) ∧ (𝑧𝑥 ∧ ∀𝑣𝑥𝑢𝑧 𝑣𝑢))})
261, 25wceq 1475 1 wff cf = (𝑥 ∈ On ↦ {𝑦 ∣ ∃𝑧(𝑦 = (card‘𝑧) ∧ (𝑧𝑥 ∧ ∀𝑣𝑥𝑢𝑧 𝑣𝑢))})
Colors of variables: wff setvar class
This definition is referenced by:  cfval  8952  cff  8953
  Copyright terms: Public domain W3C validator