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

Metamath Proof Explorer

Definition df-cf

Description: Define the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx (Roman numeral 30). See cfval for its value and a description. (Contributed by NM, 1-Apr-2004)

Ref Expression
Assertion df-cf ⊢ cf = x ∈ On ⟼ ⋂ y | ∃ z y = card ⁡ z ∧ z ⊆ x ∧ ∀ v ∈ x ∃ u ∈ z v ⊆ u

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccf class cf
1 vx setvar x
2 con0 class On
3 vy setvar y
4 vz setvar z
5 3 cv setvar y
6 ccrd class card
7 4 cv setvar z
8 7 6 cfv class card ⁡ z
9 5 8 wceq wff y = card ⁡ z
10 1 cv setvar x
11 7 10 wss wff z ⊆ x
12 vv setvar v
13 vu setvar u
14 12 cv setvar v
15 13 cv setvar u
16 14 15 wss wff v ⊆ u
17 16 13 7 wrex wff ∃ u ∈ z v ⊆ u
18 17 12 10 wral wff ∀ v ∈ x ∃ u ∈ z v ⊆ u
19 11 18 wa wff z ⊆ x ∧ ∀ v ∈ x ∃ u ∈ z v ⊆ u
20 9 19 wa wff y = card ⁡ z ∧ z ⊆ x ∧ ∀ v ∈ x ∃ u ∈ z v ⊆ u
21 20 4 wex wff ∃ z y = card ⁡ z ∧ z ⊆ x ∧ ∀ v ∈ x ∃ u ∈ z v ⊆ u
22 21 3 cab class y | ∃ z y = card ⁡ z ∧ z ⊆ x ∧ ∀ v ∈ x ∃ u ∈ z v ⊆ u
23 22 cint class ⋂ y | ∃ z y = card ⁡ z ∧ z ⊆ x ∧ ∀ v ∈ x ∃ u ∈ z v ⊆ u
24 1 2 23 cmpt class x ∈ On ⟼ ⋂ y | ∃ z y = card ⁡ z ∧ z ⊆ x ∧ ∀ v ∈ x ∃ u ∈ z v ⊆ u
25 0 24 wceq wff cf = x ∈ On ⟼ ⋂ y | ∃ z y = card ⁡ z ∧ z ⊆ x ∧ ∀ v ∈ x ∃ u ∈ z v ⊆ u