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 = ( 𝑥 ∈ On ↦ ∩ { 𝑦 ∣ ∃ 𝑧 ( 𝑦 = ( card ‘ 𝑧 ) ∧ ( 𝑧 ⊆ 𝑥 ∧ ∀ 𝑤 ∈ 𝑥 ∃ 𝑣 ∈ 𝑧 𝑤 ⊆ 𝑣 ) ) } )
2 cardon ⊢ ( card ‘ 𝑧 ) ∈ On
3 eleq1 ⊢ ( 𝑦 = ( card ‘ 𝑧 ) → ( 𝑦 ∈ On ↔ ( card ‘ 𝑧 ) ∈ On ) )
4 2 3 mpbiri ⊢ ( 𝑦 = ( card ‘ 𝑧 ) → 𝑦 ∈ On )
5 4 adantr ⊢ ( ( 𝑦 = ( card ‘ 𝑧 ) ∧ ( 𝑧 ⊆ 𝑥 ∧ ∀ 𝑤 ∈ 𝑥 ∃ 𝑣 ∈ 𝑧 𝑤 ⊆ 𝑣 ) ) → 𝑦 ∈ On )
6 5 exlimiv ⊢ ( ∃ 𝑧 ( 𝑦 = ( card ‘ 𝑧 ) ∧ ( 𝑧 ⊆ 𝑥 ∧ ∀ 𝑤 ∈ 𝑥 ∃ 𝑣 ∈ 𝑧 𝑤 ⊆ 𝑣 ) ) → 𝑦 ∈ On )
7 6 abssi ⊢ { 𝑦 ∣ ∃ 𝑧 ( 𝑦 = ( card ‘ 𝑧 ) ∧ ( 𝑧 ⊆ 𝑥 ∧ ∀ 𝑤 ∈ 𝑥 ∃ 𝑣 ∈ 𝑧 𝑤 ⊆ 𝑣 ) ) } ⊆ On
8 cflem ⊢ ( 𝑥 ∈ On → ∃ 𝑦 ∃ 𝑧 ( 𝑦 = ( card ‘ 𝑧 ) ∧ ( 𝑧 ⊆ 𝑥 ∧ ∀ 𝑤 ∈ 𝑥 ∃ 𝑣 ∈ 𝑧 𝑤 ⊆ 𝑣 ) ) )
9 abn0 ⊢ ( { 𝑦 ∣ ∃ 𝑧 ( 𝑦 = ( card ‘ 𝑧 ) ∧ ( 𝑧 ⊆ 𝑥 ∧ ∀ 𝑤 ∈ 𝑥 ∃ 𝑣 ∈ 𝑧 𝑤 ⊆ 𝑣 ) ) } ≠ ∅ ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑦 = ( card ‘ 𝑧 ) ∧ ( 𝑧 ⊆ 𝑥 ∧ ∀ 𝑤 ∈ 𝑥 ∃ 𝑣 ∈ 𝑧 𝑤 ⊆ 𝑣 ) ) )
10 8 9 sylibr ⊢ ( 𝑥 ∈ On → { 𝑦 ∣ ∃ 𝑧 ( 𝑦 = ( card ‘ 𝑧 ) ∧ ( 𝑧 ⊆ 𝑥 ∧ ∀ 𝑤 ∈ 𝑥 ∃ 𝑣 ∈ 𝑧 𝑤 ⊆ 𝑣 ) ) } ≠ ∅ )
11 oninton ⊢ ( ( { 𝑦 ∣ ∃ 𝑧 ( 𝑦 = ( card ‘ 𝑧 ) ∧ ( 𝑧 ⊆ 𝑥 ∧ ∀ 𝑤 ∈ 𝑥 ∃ 𝑣 ∈ 𝑧 𝑤 ⊆ 𝑣 ) ) } ⊆ On ∧ { 𝑦 ∣ ∃ 𝑧 ( 𝑦 = ( card ‘ 𝑧 ) ∧ ( 𝑧 ⊆ 𝑥 ∧ ∀ 𝑤 ∈ 𝑥 ∃ 𝑣 ∈ 𝑧 𝑤 ⊆ 𝑣 ) ) } ≠ ∅ ) → ∩ { 𝑦 ∣ ∃ 𝑧 ( 𝑦 = ( card ‘ 𝑧 ) ∧ ( 𝑧 ⊆ 𝑥 ∧ ∀ 𝑤 ∈ 𝑥 ∃ 𝑣 ∈ 𝑧 𝑤 ⊆ 𝑣 ) ) } ∈ On )
12 7 10 11 sylancr ⊢ ( 𝑥 ∈ On → ∩ { 𝑦 ∣ ∃ 𝑧 ( 𝑦 = ( card ‘ 𝑧 ) ∧ ( 𝑧 ⊆ 𝑥 ∧ ∀ 𝑤 ∈ 𝑥 ∃ 𝑣 ∈ 𝑧 𝑤 ⊆ 𝑣 ) ) } ∈ On )
13 1 12 fmpti ⊢ cf : On ⟶ On