Metamath Proof Explorer

Theorem cfeq0

Description: Only the ordinal zero has cofinality zero. (Contributed by NM, 24-Apr-2004) (Revised by Mario Carneiro, 12-Feb-2013)

Ref Expression
Assertion cfeq0 
|- ( A e. On -> ( ( cf ` A ) = (/) <-> A = (/) ) )

Proof

Step Hyp Ref Expression
1 cfval 
 |-  ( A e. On -> ( cf ` A ) = |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } )
2 1 eqeq1d 
 |-  ( A e. On -> ( ( cf ` A ) = (/) <-> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } = (/) ) )
3 vex 
 |-  v e. _V
4 eqeq1 
 |-  ( x = v -> ( x = ( card ` y ) <-> v = ( card ` y ) ) )
5 4 anbi1d 
 |-  ( x = v -> ( ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) <-> ( v = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) )
6 5 exbidv 
 |-  ( x = v -> ( E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) <-> E. y ( v = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) )
7 3 6 elab 
 |-  ( v e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } <-> E. y ( v = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) )
8 fveq2 
 |-  ( v = ( card ` y ) -> ( card ` v ) = ( card ` ( card ` y ) ) )
9 cardidm 
 |-  ( card ` ( card ` y ) ) = ( card ` y )
10 8 9 eqtrdi 
 |-  ( v = ( card ` y ) -> ( card ` v ) = ( card ` y ) )
11 eqeq2 
 |-  ( v = ( card ` y ) -> ( ( card ` v ) = v <-> ( card ` v ) = ( card ` y ) ) )
12 10 11 mpbird 
 |-  ( v = ( card ` y ) -> ( card ` v ) = v )
13 12 adantr 
 |-  ( ( v = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> ( card ` v ) = v )
14 13 exlimiv 
 |-  ( E. y ( v = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> ( card ` v ) = v )
15 7 14 sylbi 
 |-  ( v e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } -> ( card ` v ) = v )
16 cardon 
 |-  ( card ` v ) e. On
17 15 16 eqeltrrdi 
 |-  ( v e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } -> v e. On )
18 17 ssriv 
 |-  { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } C_ On
19 onint0 
 |-  ( { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } C_ On -> ( |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } = (/) <-> (/) e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } ) )
20 18 19 ax-mp 
 |-  ( |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } = (/) <-> (/) e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } )
21 0ex 
 |-  (/) e. _V
22 eqeq1 
 |-  ( x = (/) -> ( x = ( card ` y ) <-> (/) = ( card ` y ) ) )
23 22 anbi1d 
 |-  ( x = (/) -> ( ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) <-> ( (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) )
24 23 exbidv 
 |-  ( x = (/) -> ( E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) <-> E. y ( (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) )
25 21 24 elab 
 |-  ( (/) e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } <-> E. y ( (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) )
26 onss 
 |-  ( A e. On -> A C_ On )
27 sstr 
 |-  ( ( y C_ A /\ A C_ On ) -> y C_ On )
28 27 ancoms 
 |-  ( ( A C_ On /\ y C_ A ) -> y C_ On )
29 26 28 sylan 
 |-  ( ( A e. On /\ y C_ A ) -> y C_ On )
30 29 3adant2 
 |-  ( ( A e. On /\ (/) = ( card ` y ) /\ y C_ A ) -> y C_ On )
31 30 3adant3r 
 |-  ( ( A e. On /\ (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> y C_ On )
32 simp2 
 |-  ( ( A e. On /\ (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> (/) = ( card ` y ) )
33 simp3 
 |-  ( ( A e. On /\ (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> ( y C_ A /\ A. z e. A E. w e. y z C_ w ) )
34 eqcom 
 |-  ( (/) = ( card ` y ) <-> ( card ` y ) = (/) )
35 vex 
 |-  y e. _V
36 onssnum 
 |-  ( ( y e. _V /\ y C_ On ) -> y e. dom card )
37 35 36 mpan 
 |-  ( y C_ On -> y e. dom card )
38 cardnueq0 
 |-  ( y e. dom card -> ( ( card ` y ) = (/) <-> y = (/) ) )
39 37 38 syl 
 |-  ( y C_ On -> ( ( card ` y ) = (/) <-> y = (/) ) )
40 34 39 bitrid 
 |-  ( y C_ On -> ( (/) = ( card ` y ) <-> y = (/) ) )
41 40 biimpa 
 |-  ( ( y C_ On /\ (/) = ( card ` y ) ) -> y = (/) )
42 sseq1 
 |-  ( y = (/) -> ( y C_ A <-> (/) C_ A ) )
43 rexeq 
 |-  ( y = (/) -> ( E. w e. y z C_ w <-> E. w e. (/) z C_ w ) )
44 43 ralbidv 
 |-  ( y = (/) -> ( A. z e. A E. w e. y z C_ w <-> A. z e. A E. w e. (/) z C_ w ) )
45 42 44 anbi12d 
 |-  ( y = (/) -> ( ( y C_ A /\ A. z e. A E. w e. y z C_ w ) <-> ( (/) C_ A /\ A. z e. A E. w e. (/) z C_ w ) ) )
46 45 biimpa 
 |-  ( ( y = (/) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> ( (/) C_ A /\ A. z e. A E. w e. (/) z C_ w ) )
47 41 46 sylan 
 |-  ( ( ( y C_ On /\ (/) = ( card ` y ) ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> ( (/) C_ A /\ A. z e. A E. w e. (/) z C_ w ) )
48 rex0 
 |-  -. E. w e. (/) z C_ w
49 48 rgenw 
 |-  A. z e. A -. E. w e. (/) z C_ w
50 r19.2z 
 |-  ( ( A =/= (/) /\ A. z e. A -. E. w e. (/) z C_ w ) -> E. z e. A -. E. w e. (/) z C_ w )
51 49 50 mpan2 
 |-  ( A =/= (/) -> E. z e. A -. E. w e. (/) z C_ w )
52 rexnal 
 |-  ( E. z e. A -. E. w e. (/) z C_ w <-> -. A. z e. A E. w e. (/) z C_ w )
53 51 52 sylib 
 |-  ( A =/= (/) -> -. A. z e. A E. w e. (/) z C_ w )
54 53 necon4ai 
 |-  ( A. z e. A E. w e. (/) z C_ w -> A = (/) )
55 47 54 simpl2im 
 |-  ( ( ( y C_ On /\ (/) = ( card ` y ) ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> A = (/) )
56 31 32 33 55 syl21anc 
 |-  ( ( A e. On /\ (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> A = (/) )
57 56 3expib 
 |-  ( A e. On -> ( ( (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> A = (/) ) )
58 57 exlimdv 
 |-  ( A e. On -> ( E. y ( (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> A = (/) ) )
59 25 58 syl5bi 
 |-  ( A e. On -> ( (/) e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } -> A = (/) ) )
60 20 59 syl5bi 
 |-  ( A e. On -> ( |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } = (/) -> A = (/) ) )
61 2 60 sylbid 
 |-  ( A e. On -> ( ( cf ` A ) = (/) -> A = (/) ) )
62 fveq2 
 |-  ( A = (/) -> ( cf ` A ) = ( cf ` (/) ) )
63 cf0 
 |-  ( cf ` (/) ) = (/)
64 62 63 eqtrdi 
 |-  ( A = (/) -> ( cf ` A ) = (/) )
65 61 64 impbid1 
 |-  ( A e. On -> ( ( cf ` A ) = (/) <-> A = (/) ) )