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

Definition df-cf 7828
 Description: Define the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx (Roman numeral 30). See cfval 8127 for its value and a description. (Contributed by NM, 1-Apr-2004.)
Assertion
Ref Expression
df-cf
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-cf
StepHypRef Expression
1 ccf 7824 . 2
2 vx . . 3
3 con0 4581 . . 3
4 vy . . . . . . . . 9
54cv 1651 . . . . . . . 8
6 vz . . . . . . . . . 10
76cv 1651 . . . . . . . . 9
8 ccrd 7822 . . . . . . . . 9
97, 8cfv 5454 . . . . . . . 8
105, 9wceq 1652 . . . . . . 7
112cv 1651 . . . . . . . . 9
127, 11wss 3320 . . . . . . . 8
13 vv . . . . . . . . . . . 12
1413cv 1651 . . . . . . . . . . 11
15 vu . . . . . . . . . . . 12
1615cv 1651 . . . . . . . . . . 11
1714, 16wss 3320 . . . . . . . . . 10
1817, 15, 7wrex 2706 . . . . . . . . 9
1918, 13, 11wral 2705 . . . . . . . 8
2012, 19wa 359 . . . . . . 7
2110, 20wa 359 . . . . . 6
2221, 6wex 1550 . . . . 5
2322, 4cab 2422 . . . 4
2423cint 4050 . . 3
252, 3, 24cmpt 4266 . 2
261, 25wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  cfval  8127  cff  8128
 Copyright terms: Public domain W3C validator