Metamath Proof Explorer


Theorem cflim3

Description: Another expression for the cofinality function. (Contributed by Mario Carneiro, 28-Feb-2013)

Ref Expression
Hypothesis cflim3.1 𝐴 ∈ V
Assertion cflim3 ( Lim 𝐴 → ( cf ‘ 𝐴 ) = 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } ( card ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 cflim3.1 𝐴 ∈ V
2 limord ( Lim 𝐴 → Ord 𝐴 )
3 1 elon ( 𝐴 ∈ On ↔ Ord 𝐴 )
4 2 3 sylibr ( Lim 𝐴𝐴 ∈ On )
5 cfval ( 𝐴 ∈ On → ( cf ‘ 𝐴 ) = { 𝑦 ∣ ∃ 𝑥 ( 𝑦 = ( card ‘ 𝑥 ) ∧ ( 𝑥𝐴 ∧ ∀ 𝑧𝐴𝑤𝑥 𝑧𝑤 ) ) } )
6 4 5 syl ( Lim 𝐴 → ( cf ‘ 𝐴 ) = { 𝑦 ∣ ∃ 𝑥 ( 𝑦 = ( card ‘ 𝑥 ) ∧ ( 𝑥𝐴 ∧ ∀ 𝑧𝐴𝑤𝑥 𝑧𝑤 ) ) } )
7 fvex ( card ‘ 𝑥 ) ∈ V
8 7 dfiin2 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } ( card ‘ 𝑥 ) = { 𝑦 ∣ ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) }
9 df-rex ( ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) ↔ ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } ∧ 𝑦 = ( card ‘ 𝑥 ) ) )
10 ancom ( ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } ∧ 𝑦 = ( card ‘ 𝑥 ) ) ↔ ( 𝑦 = ( card ‘ 𝑥 ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } ) )
11 rabid ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } ↔ ( 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 ) )
12 velpw ( 𝑥 ∈ 𝒫 𝐴𝑥𝐴 )
13 12 anbi1i ( ( 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 ) ↔ ( 𝑥𝐴 𝑥 = 𝐴 ) )
14 coflim ( ( Lim 𝐴𝑥𝐴 ) → ( 𝑥 = 𝐴 ↔ ∀ 𝑧𝐴𝑤𝑥 𝑧𝑤 ) )
15 14 pm5.32da ( Lim 𝐴 → ( ( 𝑥𝐴 𝑥 = 𝐴 ) ↔ ( 𝑥𝐴 ∧ ∀ 𝑧𝐴𝑤𝑥 𝑧𝑤 ) ) )
16 13 15 bitrid ( Lim 𝐴 → ( ( 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 ) ↔ ( 𝑥𝐴 ∧ ∀ 𝑧𝐴𝑤𝑥 𝑧𝑤 ) ) )
17 11 16 bitrid ( Lim 𝐴 → ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } ↔ ( 𝑥𝐴 ∧ ∀ 𝑧𝐴𝑤𝑥 𝑧𝑤 ) ) )
18 17 anbi2d ( Lim 𝐴 → ( ( 𝑦 = ( card ‘ 𝑥 ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } ) ↔ ( 𝑦 = ( card ‘ 𝑥 ) ∧ ( 𝑥𝐴 ∧ ∀ 𝑧𝐴𝑤𝑥 𝑧𝑤 ) ) ) )
19 10 18 bitrid ( Lim 𝐴 → ( ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } ∧ 𝑦 = ( card ‘ 𝑥 ) ) ↔ ( 𝑦 = ( card ‘ 𝑥 ) ∧ ( 𝑥𝐴 ∧ ∀ 𝑧𝐴𝑤𝑥 𝑧𝑤 ) ) ) )
20 19 exbidv ( Lim 𝐴 → ( ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } ∧ 𝑦 = ( card ‘ 𝑥 ) ) ↔ ∃ 𝑥 ( 𝑦 = ( card ‘ 𝑥 ) ∧ ( 𝑥𝐴 ∧ ∀ 𝑧𝐴𝑤𝑥 𝑧𝑤 ) ) ) )
21 9 20 bitrid ( Lim 𝐴 → ( ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) ↔ ∃ 𝑥 ( 𝑦 = ( card ‘ 𝑥 ) ∧ ( 𝑥𝐴 ∧ ∀ 𝑧𝐴𝑤𝑥 𝑧𝑤 ) ) ) )
22 21 abbidv ( Lim 𝐴 → { 𝑦 ∣ ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) } = { 𝑦 ∣ ∃ 𝑥 ( 𝑦 = ( card ‘ 𝑥 ) ∧ ( 𝑥𝐴 ∧ ∀ 𝑧𝐴𝑤𝑥 𝑧𝑤 ) ) } )
23 22 inteqd ( Lim 𝐴 { 𝑦 ∣ ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) } = { 𝑦 ∣ ∃ 𝑥 ( 𝑦 = ( card ‘ 𝑥 ) ∧ ( 𝑥𝐴 ∧ ∀ 𝑧𝐴𝑤𝑥 𝑧𝑤 ) ) } )
24 8 23 eqtr2id ( Lim 𝐴 { 𝑦 ∣ ∃ 𝑥 ( 𝑦 = ( card ‘ 𝑥 ) ∧ ( 𝑥𝐴 ∧ ∀ 𝑧𝐴𝑤𝑥 𝑧𝑤 ) ) } = 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } ( card ‘ 𝑥 ) )
25 6 24 eqtrd ( Lim 𝐴 → ( cf ‘ 𝐴 ) = 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } ( card ‘ 𝑥 ) )