Metamath Proof Explorer


Theorem cf0

Description: Value of the cofinality function at 0. Exercise 2 of TakeutiZaring p. 102. (Contributed by NM, 16-Apr-2004)

Ref Expression
Assertion cf0 cf=

Proof

Step Hyp Ref Expression
1 cfub cfx|yx=cardyyy
2 0ss y
3 2 biantru yyy
4 ss0b yy=
5 3 4 bitr3i yyy=
6 5 anbi1ci x=cardyyyy=x=cardy
7 6 exbii yx=cardyyyyy=x=cardy
8 0ex V
9 fveq2 y=cardy=card
10 9 eqeq2d y=x=cardyx=card
11 8 10 ceqsexv yy=x=cardyx=card
12 card0 card=
13 12 eqeq2i x=cardx=
14 7 11 13 3bitri yx=cardyyyx=
15 14 abbii x|yx=cardyyy=x|x=
16 df-sn =x|x=
17 15 16 eqtr4i x|yx=cardyyy=
18 17 inteqi x|yx=cardyyy=
19 8 intsn =
20 18 19 eqtri x|yx=cardyyy=
21 1 20 sseqtri cf
22 ss0b cfcf=
23 21 22 mpbi cf=