Metamath Proof Explorer

Theorem cff

Description: Cofinality is a function on the class of ordinal numbers to the class of cardinal numbers. (Contributed by Mario Carneiro, 15-Sep-2013)

Ref Expression
Assertion cff ⊢cf:On⟶On

Proof

Step Hyp Ref Expression
1 df-cf ⊢cf=x∈On⟼⋂y|∃zy=card⁡z∧z⊆x∧∀w∈x∃v∈zw⊆v
2 cardon ⊢card⁡z∈On
3 eleq1 ⊢y=card⁡z→y∈On↔card⁡z∈On
4 2 3 mpbiri ⊢y=card⁡z→y∈On
5 4 adantr ⊢y=card⁡z∧z⊆x∧∀w∈x∃v∈zw⊆v→y∈On
6 5 exlimiv ⊢∃zy=card⁡z∧z⊆x∧∀w∈x∃v∈zw⊆v→y∈On
7 6 abssi ⊢y|∃zy=card⁡z∧z⊆x∧∀w∈x∃v∈zw⊆v⊆On
8 cflem ⊢x∈On→∃y∃zy=card⁡z∧z⊆x∧∀w∈x∃v∈zw⊆v
9 abn0 ⊢y|∃zy=card⁡z∧z⊆x∧∀w∈x∃v∈zw⊆v≠∅↔∃y∃zy=card⁡z∧z⊆x∧∀w∈x∃v∈zw⊆v
10 8 9 sylibr ⊢x∈On→y|∃zy=card⁡z∧z⊆x∧∀w∈x∃v∈zw⊆v≠∅
11 oninton ⊢y|∃zy=card⁡z∧z⊆x∧∀w∈x∃v∈zw⊆v⊆On∧y|∃zy=card⁡z∧z⊆x∧∀w∈x∃v∈zw⊆v≠∅→⋂y|∃zy=card⁡z∧z⊆x∧∀w∈x∃v∈zw⊆v∈On
12 7 10 11 sylancr ⊢x∈On→⋂y|∃zy=card⁡z∧z⊆x∧∀w∈x∃v∈zw⊆v∈On
13 1 12 fmpti ⊢cf:On⟶On