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 = ( 𝑥 ∈ On ↦ ∩ { 𝑦 ∣ ∃ 𝑧 ( 𝑦 = ( card ‘ 𝑧 ) ∧ ( 𝑧 ⊆ 𝑥 ∧ ∀ 𝑣 ∈ 𝑥 ∃ 𝑢 ∈ 𝑧 𝑣 ⊆ 𝑢 ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccf ⊢ cf
1 vx ⊢ 𝑥
2 con0 ⊢ On
3 vy ⊢ 𝑦
4 vz ⊢ 𝑧
5 3 cv ⊢ 𝑦
6 ccrd ⊢ card
7 4 cv ⊢ 𝑧
8 7 6 cfv ⊢ ( card ‘ 𝑧 )
9 5 8 wceq ⊢ 𝑦 = ( card ‘ 𝑧 )
10 1 cv ⊢ 𝑥
11 7 10 wss ⊢ 𝑧 ⊆ 𝑥
12 vv ⊢ 𝑣
13 vu ⊢ 𝑢
14 12 cv ⊢ 𝑣
15 13 cv ⊢ 𝑢
16 14 15 wss ⊢ 𝑣 ⊆ 𝑢
17 16 13 7 wrex ⊢ ∃ 𝑢 ∈ 𝑧 𝑣 ⊆ 𝑢
18 17 12 10 wral ⊢ ∀ 𝑣 ∈ 𝑥 ∃ 𝑢 ∈ 𝑧 𝑣 ⊆ 𝑢
19 11 18 wa ⊢ ( 𝑧 ⊆ 𝑥 ∧ ∀ 𝑣 ∈ 𝑥 ∃ 𝑢 ∈ 𝑧 𝑣 ⊆ 𝑢 )
20 9 19 wa ⊢ ( 𝑦 = ( card ‘ 𝑧 ) ∧ ( 𝑧 ⊆ 𝑥 ∧ ∀ 𝑣 ∈ 𝑥 ∃ 𝑢 ∈ 𝑧 𝑣 ⊆ 𝑢 ) )
21 20 4 wex ⊢ ∃ 𝑧 ( 𝑦 = ( card ‘ 𝑧 ) ∧ ( 𝑧 ⊆ 𝑥 ∧ ∀ 𝑣 ∈ 𝑥 ∃ 𝑢 ∈ 𝑧 𝑣 ⊆ 𝑢 ) )
22 21 3 cab ⊢ { 𝑦 ∣ ∃ 𝑧 ( 𝑦 = ( card ‘ 𝑧 ) ∧ ( 𝑧 ⊆ 𝑥 ∧ ∀ 𝑣 ∈ 𝑥 ∃ 𝑢 ∈ 𝑧 𝑣 ⊆ 𝑢 ) ) }
23 22 cint ⊢ ∩ { 𝑦 ∣ ∃ 𝑧 ( 𝑦 = ( card ‘ 𝑧 ) ∧ ( 𝑧 ⊆ 𝑥 ∧ ∀ 𝑣 ∈ 𝑥 ∃ 𝑢 ∈ 𝑧 𝑣 ⊆ 𝑢 ) ) }
24 1 2 23 cmpt ⊢ ( 𝑥 ∈ On ↦ ∩ { 𝑦 ∣ ∃ 𝑧 ( 𝑦 = ( card ‘ 𝑧 ) ∧ ( 𝑧 ⊆ 𝑥 ∧ ∀ 𝑣 ∈ 𝑥 ∃ 𝑢 ∈ 𝑧 𝑣 ⊆ 𝑢 ) ) } )
25 0 24 wceq ⊢ cf = ( 𝑥 ∈ On ↦ ∩ { 𝑦 ∣ ∃ 𝑧 ( 𝑦 = ( card ‘ 𝑧 ) ∧ ( 𝑧 ⊆ 𝑥 ∧ ∀ 𝑣 ∈ 𝑥 ∃ 𝑢 ∈ 𝑧 𝑣 ⊆ 𝑢 ) ) } )