Metamath Proof Explorer

Theorem cfval

Description: Value of the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx (Roman numeral 30). The cofinality of an ordinal number A is the cardinality (size) of the smallest unbounded subset y of the ordinal number. Unbounded means that for every member of A , there is a member of y that is at least as large. Cofinality is a measure of how "reachable from below" an ordinal is. (Contributed by NM, 1-Apr-2004) (Revised by Mario Carneiro, 15-Sep-2013)

Ref Expression
Assertion cfval ⊢ A ∈ On → cf ⁡ A = ⋂ x | ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w

Proof

Step Hyp Ref Expression
1 cflem ⊢ A ∈ On → ∃ x ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w
2 intexab ⊢ ∃ x ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w ↔ ⋂ x | ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w ∈ V
3 1 2 sylib ⊢ A ∈ On → ⋂ x | ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w ∈ V
4 sseq2 ⊢ v = A → y ⊆ v ↔ y ⊆ A
5 raleq ⊢ v = A → ∀ z ∈ v ∃ w ∈ y z ⊆ w ↔ ∀ z ∈ A ∃ w ∈ y z ⊆ w
6 4 5 anbi12d ⊢ v = A → y ⊆ v ∧ ∀ z ∈ v ∃ w ∈ y z ⊆ w ↔ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w
7 6 anbi2d ⊢ v = A → x = card ⁡ y ∧ y ⊆ v ∧ ∀ z ∈ v ∃ w ∈ y z ⊆ w ↔ x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w
8 7 exbidv ⊢ v = A → ∃ y x = card ⁡ y ∧ y ⊆ v ∧ ∀ z ∈ v ∃ w ∈ y z ⊆ w ↔ ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w
9 8 abbidv ⊢ v = A → x | ∃ y x = card ⁡ y ∧ y ⊆ v ∧ ∀ z ∈ v ∃ w ∈ y z ⊆ w = x | ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w
10 9 inteqd ⊢ v = A → ⋂ x | ∃ y x = card ⁡ y ∧ y ⊆ v ∧ ∀ z ∈ v ∃ w ∈ y z ⊆ w = ⋂ x | ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w
11 df-cf ⊢ cf = v ∈ On ⟼ ⋂ x | ∃ y x = card ⁡ y ∧ y ⊆ v ∧ ∀ z ∈ v ∃ w ∈ y z ⊆ w
12 10 11 fvmptg ⊢ A ∈ On ∧ ⋂ x | ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w ∈ V → cf ⁡ A = ⋂ x | ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w
13 3 12 mpdan ⊢ A ∈ On → cf ⁡ A = ⋂ x | ∃ y x = card ⁡ y ∧ y ⊆ A ∧ ∀ z ∈ A ∃ w ∈ y z ⊆ w