This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 | ∃ z y = card ⁡ z ∧ z ⊆ x ∧ ∀ w ∈ x ∃ v ∈ z w ⊆ 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 ∈ z w ⊆ v → y ∈ On
6 5 exlimiv ⊢ ∃ z y = card ⁡ z ∧ z ⊆ x ∧ ∀ w ∈ x ∃ v ∈ z w ⊆ v → y ∈ On
7 6 abssi ⊢ y | ∃ z y = card ⁡ z ∧ z ⊆ x ∧ ∀ w ∈ x ∃ v ∈ z w ⊆ v ⊆ On
8 cflem ⊢ x ∈ On → ∃ y ∃ z y = card ⁡ z ∧ z ⊆ x ∧ ∀ w ∈ x ∃ v ∈ z w ⊆ v
9 abn0 ⊢ y | ∃ z y = card ⁡ z ∧ z ⊆ x ∧ ∀ w ∈ x ∃ v ∈ z w ⊆ v ≠ ∅ ↔ ∃ y ∃ z y = card ⁡ z ∧ z ⊆ x ∧ ∀ w ∈ x ∃ v ∈ z w ⊆ v
10 8 9 sylibr ⊢ x ∈ On → y | ∃ z y = card ⁡ z ∧ z ⊆ x ∧ ∀ w ∈ x ∃ v ∈ z w ⊆ v ≠ ∅
11 oninton ⊢ y | ∃ z y = card ⁡ z ∧ z ⊆ x ∧ ∀ w ∈ x ∃ v ∈ z w ⊆ v ⊆ On ∧ y | ∃ z y = card ⁡ z ∧ z ⊆ x ∧ ∀ w ∈ x ∃ v ∈ z w ⊆ v ≠ ∅ → ⋂ y | ∃ z y = card ⁡ z ∧ z ⊆ x ∧ ∀ w ∈ x ∃ v ∈ z w ⊆ v ∈ On
12 7 10 11 sylancr ⊢ x ∈ On → ⋂ y | ∃ z y = card ⁡ z ∧ z ⊆ x ∧ ∀ w ∈ x ∃ v ∈ z w ⊆ v ∈ On
13 1 12 fmpti ⊢ cf : On ⟶ On