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 ‘ 𝑧 ) ∧ ( 𝑧 ⊆ 𝑥 ∧ ∀ 𝑣 ∈ 𝑥 ∃ 𝑢 ∈ 𝑧 𝑣 ⊆ 𝑢 ) ) } )