Metamath Proof Explorer

Definition df-cf

Description: Define the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx (Roman numeral 30). See cfval for its value and a description. (Contributed by NM, 1-Apr-2004)

Ref Expression
Assertion df-cf ⊢cf=x∈On⟼⋂y|∃zy=card⁡z∧z⊆x∧∀v∈x∃u∈zv⊆u

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccf classcf
1 vx setvarx
2 con0 classOn
3 vy setvary
4 vz setvarz
5 3 cv setvary
6 ccrd classcard
7 4 cv setvarz
8 7 6 cfv classcard⁡z
9 5 8 wceq wffy=card⁡z
10 1 cv setvarx
11 7 10 wss wffz⊆x
12 vv setvarv
13 vu setvaru
14 12 cv setvarv
15 13 cv setvaru
16 14 15 wss wffv⊆u
17 16 13 7 wrex wff∃u∈zv⊆u
18 17 12 10 wral wff∀v∈x∃u∈zv⊆u
19 11 18 wa wffz⊆x∧∀v∈x∃u∈zv⊆u
20 9 19 wa wffy=card⁡z∧z⊆x∧∀v∈x∃u∈zv⊆u
21 20 4 wex wff∃zy=card⁡z∧z⊆x∧∀v∈x∃u∈zv⊆u
22 21 3 cab classy|∃zy=card⁡z∧z⊆x∧∀v∈x∃u∈zv⊆u
23 22 cint class⋂y|∃zy=card⁡z∧z⊆x∧∀v∈x∃u∈zv⊆u
24 1 2 23 cmpt classx∈On⟼⋂y|∃zy=card⁡z∧z⊆x∧∀v∈x∃u∈zv⊆u
25 0 24 wceq wffcf=x∈On⟼⋂y|∃zy=card⁡z∧z⊆x∧∀v∈x∃u∈zv⊆u