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 9882
Description: Define the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx (Roman numeral 30). See cfval 10188 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 9878 . 2 class cf
2 vx . . 3 setvar π‘₯
3 con0 6318 . . 3 class On
4 vy . . . . . . . . 9 setvar 𝑦
54cv 1541 . . . . . . . 8 class 𝑦
6 vz . . . . . . . . . 10 setvar 𝑧
76cv 1541 . . . . . . . . 9 class 𝑧
8 ccrd 9876 . . . . . . . . 9 class card
97, 8cfv 6497 . . . . . . . 8 class (cardβ€˜π‘§)
105, 9wceq 1542 . . . . . . 7 wff 𝑦 = (cardβ€˜π‘§)
112cv 1541 . . . . . . . . 9 class π‘₯
127, 11wss 3911 . . . . . . . 8 wff 𝑧 βŠ† π‘₯
13 vv . . . . . . . . . . . 12 setvar 𝑣
1413cv 1541 . . . . . . . . . . 11 class 𝑣
15 vu . . . . . . . . . . . 12 setvar 𝑒
1615cv 1541 . . . . . . . . . . 11 class 𝑒
1714, 16wss 3911 . . . . . . . . . 10 wff 𝑣 βŠ† 𝑒
1817, 15, 7wrex 3070 . . . . . . . . 9 wff βˆƒπ‘’ ∈ 𝑧 𝑣 βŠ† 𝑒
1918, 13, 11wral 3061 . . . . . . . 8 wff βˆ€π‘£ ∈ π‘₯ βˆƒπ‘’ ∈ 𝑧 𝑣 βŠ† 𝑒
2012, 19wa 397 . . . . . . 7 wff (𝑧 βŠ† π‘₯ ∧ βˆ€π‘£ ∈ π‘₯ βˆƒπ‘’ ∈ 𝑧 𝑣 βŠ† 𝑒)
2110, 20wa 397 . . . . . 6 wff (𝑦 = (cardβ€˜π‘§) ∧ (𝑧 βŠ† π‘₯ ∧ βˆ€π‘£ ∈ π‘₯ βˆƒπ‘’ ∈ 𝑧 𝑣 βŠ† 𝑒))
2221, 6wex 1782 . . . . 5 wff βˆƒπ‘§(𝑦 = (cardβ€˜π‘§) ∧ (𝑧 βŠ† π‘₯ ∧ βˆ€π‘£ ∈ π‘₯ βˆƒπ‘’ ∈ 𝑧 𝑣 βŠ† 𝑒))
2322, 4cab 2710 . . . 4 class {𝑦 ∣ βˆƒπ‘§(𝑦 = (cardβ€˜π‘§) ∧ (𝑧 βŠ† π‘₯ ∧ βˆ€π‘£ ∈ π‘₯ βˆƒπ‘’ ∈ 𝑧 𝑣 βŠ† 𝑒))}
2423cint 4908 . . 3 class ∩ {𝑦 ∣ βˆƒπ‘§(𝑦 = (cardβ€˜π‘§) ∧ (𝑧 βŠ† π‘₯ ∧ βˆ€π‘£ ∈ π‘₯ βˆƒπ‘’ ∈ 𝑧 𝑣 βŠ† 𝑒))}
252, 3, 24cmpt 5189 . 2 class (π‘₯ ∈ On ↦ ∩ {𝑦 ∣ βˆƒπ‘§(𝑦 = (cardβ€˜π‘§) ∧ (𝑧 βŠ† π‘₯ ∧ βˆ€π‘£ ∈ π‘₯ βˆƒπ‘’ ∈ 𝑧 𝑣 βŠ† 𝑒))})
261, 25wceq 1542 1 wff cf = (π‘₯ ∈ On ↦ ∩ {𝑦 ∣ βˆƒπ‘§(𝑦 = (cardβ€˜π‘§) ∧ (𝑧 βŠ† π‘₯ ∧ βˆ€π‘£ ∈ π‘₯ βˆƒπ‘’ ∈ 𝑧 𝑣 βŠ† 𝑒))})
Colors of variables: wff setvar class
This definition is referenced by:  cfval  10188  cff  10189
  Copyright terms: Public domain W3C validator