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