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

Definition df-cf 8393
 Description: Define the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx (Roman numeral 30). See cfval 8695 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 8389 . 2
2 vx . . 3
3 con0 5430 . . 3
4 vy . . . . . . . . 9
54cv 1451 . . . . . . . 8
6 vz . . . . . . . . . 10
76cv 1451 . . . . . . . . 9
8 ccrd 8387 . . . . . . . . 9
97, 8cfv 5589 . . . . . . . 8
105, 9wceq 1452 . . . . . . 7
112cv 1451 . . . . . . . . 9
127, 11wss 3390 . . . . . . . 8
13 vv . . . . . . . . . . . 12
1413cv 1451 . . . . . . . . . . 11
15 vu . . . . . . . . . . . 12
1615cv 1451 . . . . . . . . . . 11
1714, 16wss 3390 . . . . . . . . . 10
1817, 15, 7wrex 2757 . . . . . . . . 9
1918, 13, 11wral 2756 . . . . . . . 8
2012, 19wa 376 . . . . . . 7
2110, 20wa 376 . . . . . 6
2221, 6wex 1671 . . . . 5
2322, 4cab 2457 . . . 4
2423cint 4226 . . 3
252, 3, 24cmpt 4454 . 2
261, 25wceq 1452 1
 Colors of variables: wff setvar class This definition is referenced by:  cfval  8695  cff  8696
 Copyright terms: Public domain W3C validator