Metamath Proof Explorer


Theorem cflim3

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

Ref Expression
Hypothesis cflim3.1 A V
Assertion cflim3 Lim A cf A = x x 𝒫 A | x = A card x

Proof

Step Hyp Ref Expression
1 cflim3.1 A V
2 limord Lim A Ord A
3 1 elon A On Ord A
4 2 3 sylibr Lim A A On
5 cfval A On cf A = y | x y = card x x A z A w x z w
6 4 5 syl Lim A cf A = y | x y = card x x A z A w x z w
7 fvex card x V
8 7 dfiin2 x x 𝒫 A | x = A card x = y | x x 𝒫 A | x = A y = card x
9 df-rex x x 𝒫 A | x = A y = card x x x x 𝒫 A | x = A y = card x
10 ancom x x 𝒫 A | x = A y = card x y = card x x x 𝒫 A | x = A
11 rabid x x 𝒫 A | x = A x 𝒫 A x = A
12 velpw x 𝒫 A x A
13 12 anbi1i x 𝒫 A x = A x A x = A
14 coflim Lim A x A x = A z A w x z w
15 14 pm5.32da Lim A x A x = A x A z A w x z w
16 13 15 syl5bb Lim A x 𝒫 A x = A x A z A w x z w
17 11 16 syl5bb Lim A x x 𝒫 A | x = A x A z A w x z w
18 17 anbi2d Lim A y = card x x x 𝒫 A | x = A y = card x x A z A w x z w
19 10 18 syl5bb Lim A x x 𝒫 A | x = A y = card x y = card x x A z A w x z w
20 19 exbidv Lim A x x x 𝒫 A | x = A y = card x x y = card x x A z A w x z w
21 9 20 syl5bb Lim A x x 𝒫 A | x = A y = card x x y = card x x A z A w x z w
22 21 abbidv Lim A y | x x 𝒫 A | x = A y = card x = y | x y = card x x A z A w x z w
23 22 inteqd Lim A y | x x 𝒫 A | x = A y = card x = y | x y = card x x A z A w x z w
24 8 23 eqtr2id Lim A y | x y = card x x A z A w x z w = x x 𝒫 A | x = A card x
25 6 24 eqtrd Lim A cf A = x x 𝒫 A | x = A card x