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 ( 𝐴 ∈ On → ( cf ‘ 𝐴 ) = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦𝐴 ∧ ∀ 𝑧𝐴𝑤𝑦 𝑧𝑤 ) ) } )

Proof

Step Hyp Ref Expression
1 cflem ( 𝐴 ∈ On → ∃ 𝑥𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦𝐴 ∧ ∀ 𝑧𝐴𝑤𝑦 𝑧𝑤 ) ) )
2 intexab ( ∃ 𝑥𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦𝐴 ∧ ∀ 𝑧𝐴𝑤𝑦 𝑧𝑤 ) ) ↔ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦𝐴 ∧ ∀ 𝑧𝐴𝑤𝑦 𝑧𝑤 ) ) } ∈ V )
3 1 2 sylib ( 𝐴 ∈ On → { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦𝐴 ∧ ∀ 𝑧𝐴𝑤𝑦 𝑧𝑤 ) ) } ∈ V )
4 sseq2 ( 𝑣 = 𝐴 → ( 𝑦𝑣𝑦𝐴 ) )
5 raleq ( 𝑣 = 𝐴 → ( ∀ 𝑧𝑣𝑤𝑦 𝑧𝑤 ↔ ∀ 𝑧𝐴𝑤𝑦 𝑧𝑤 ) )
6 4 5 anbi12d ( 𝑣 = 𝐴 → ( ( 𝑦𝑣 ∧ ∀ 𝑧𝑣𝑤𝑦 𝑧𝑤 ) ↔ ( 𝑦𝐴 ∧ ∀ 𝑧𝐴𝑤𝑦 𝑧𝑤 ) ) )
7 6 anbi2d ( 𝑣 = 𝐴 → ( ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦𝑣 ∧ ∀ 𝑧𝑣𝑤𝑦 𝑧𝑤 ) ) ↔ ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦𝐴 ∧ ∀ 𝑧𝐴𝑤𝑦 𝑧𝑤 ) ) ) )
8 7 exbidv ( 𝑣 = 𝐴 → ( ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦𝑣 ∧ ∀ 𝑧𝑣𝑤𝑦 𝑧𝑤 ) ) ↔ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦𝐴 ∧ ∀ 𝑧𝐴𝑤𝑦 𝑧𝑤 ) ) ) )
9 8 abbidv ( 𝑣 = 𝐴 → { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦𝑣 ∧ ∀ 𝑧𝑣𝑤𝑦 𝑧𝑤 ) ) } = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦𝐴 ∧ ∀ 𝑧𝐴𝑤𝑦 𝑧𝑤 ) ) } )
10 9 inteqd ( 𝑣 = 𝐴 { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦𝑣 ∧ ∀ 𝑧𝑣𝑤𝑦 𝑧𝑤 ) ) } = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦𝐴 ∧ ∀ 𝑧𝐴𝑤𝑦 𝑧𝑤 ) ) } )
11 df-cf cf = ( 𝑣 ∈ On ↦ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦𝑣 ∧ ∀ 𝑧𝑣𝑤𝑦 𝑧𝑤 ) ) } )
12 10 11 fvmptg ( ( 𝐴 ∈ On ∧ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦𝐴 ∧ ∀ 𝑧𝐴𝑤𝑦 𝑧𝑤 ) ) } ∈ V ) → ( cf ‘ 𝐴 ) = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦𝐴 ∧ ∀ 𝑧𝐴𝑤𝑦 𝑧𝑤 ) ) } )
13 3 12 mpdan ( 𝐴 ∈ On → ( cf ‘ 𝐴 ) = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦𝐴 ∧ ∀ 𝑧𝐴𝑤𝑦 𝑧𝑤 ) ) } )