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

Definition df-cf 8343
Description: Define the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx (Roman numeral 30). See cfval 8648 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 8339 . 2
2 vx . . 3
3 con0 4883 . . 3
4 vy . . . . . . . . 9
54cv 1394 . . . . . . . 8
6 vz . . . . . . . . . 10
76cv 1394 . . . . . . . . 9
8 ccrd 8337 . . . . . . . . 9
97, 8cfv 5593 . . . . . . . 8
105, 9wceq 1395 . . . . . . 7
112cv 1394 . . . . . . . . 9
127, 11wss 3475 . . . . . . . 8
13 vv . . . . . . . . . . . 12
1413cv 1394 . . . . . . . . . . 11
15 vu . . . . . . . . . . . 12
1615cv 1394 . . . . . . . . . . 11
1714, 16wss 3475 . . . . . . . . . 10
1817, 15, 7wrex 2808 . . . . . . . . 9
1918, 13, 11wral 2807 . . . . . . . 8
2012, 19wa 369 . . . . . . 7
2110, 20wa 369 . . . . . 6
2221, 6wex 1612 . . . . 5
2322, 4cab 2442 . . . 4
2423cint 4286 . . 3
252, 3, 24cmpt 4510 . 2
261, 25wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  cfval  8648  cff  8649
  Copyright terms: Public domain W3C validator