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 
 |-  ( cf ` (/) ) C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ (/) /\ (/) C_ U. y ) ) }
2 0ss 
 |-  (/) C_ U. y
3 2 biantru 
 |-  ( y C_ (/) <-> ( y C_ (/) /\ (/) C_ U. y ) )
4 ss0b 
 |-  ( y C_ (/) <-> y = (/) )
5 3 4 bitr3i 
 |-  ( ( y C_ (/) /\ (/) C_ U. y ) <-> y = (/) )
6 5 anbi1ci 
 |-  ( ( x = ( card ` y ) /\ ( y C_ (/) /\ (/) C_ U. y ) ) <-> ( y = (/) /\ x = ( card ` y ) ) )
7 6 exbii 
 |-  ( E. y ( x = ( card ` y ) /\ ( y C_ (/) /\ (/) C_ U. y ) ) <-> E. y ( y = (/) /\ x = ( card ` y ) ) )
8 0ex 
 |-  (/) e. _V
9 fveq2 
 |-  ( y = (/) -> ( card ` y ) = ( card ` (/) ) )
10 9 eqeq2d 
 |-  ( y = (/) -> ( x = ( card ` y ) <-> x = ( card ` (/) ) ) )
11 8 10 ceqsexv 
 |-  ( E. y ( y = (/) /\ x = ( card ` y ) ) <-> x = ( card ` (/) ) )
12 card0 
 |-  ( card ` (/) ) = (/)
13 12 eqeq2i 
 |-  ( x = ( card ` (/) ) <-> x = (/) )
14 7 11 13 3bitri 
 |-  ( E. y ( x = ( card ` y ) /\ ( y C_ (/) /\ (/) C_ U. y ) ) <-> x = (/) )
15 14 abbii 
 |-  { x | E. y ( x = ( card ` y ) /\ ( y C_ (/) /\ (/) C_ U. y ) ) } = { x | x = (/) }
16 df-sn 
 |-  { (/) } = { x | x = (/) }
17 15 16 eqtr4i 
 |-  { x | E. y ( x = ( card ` y ) /\ ( y C_ (/) /\ (/) C_ U. y ) ) } = { (/) }
18 17 inteqi 
 |-  |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ (/) /\ (/) C_ U. y ) ) } = |^| { (/) }
19 8 intsn 
 |-  |^| { (/) } = (/)
20 18 19 eqtri 
 |-  |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ (/) /\ (/) C_ U. y ) ) } = (/)
21 1 20 sseqtri 
 |-  ( cf ` (/) ) C_ (/)
22 ss0b 
 |-  ( ( cf ` (/) ) C_ (/) <-> ( cf ` (/) ) = (/) )
23 21 22 mpbi 
 |-  ( cf ` (/) ) = (/)