Metamath Proof Explorer

Theorem cfsuc

Description: Value of the cofinality function at a successor ordinal. Exercise 3 of TakeutiZaring p. 102. (Contributed by NM, 23-Apr-2004) (Revised by Mario Carneiro, 12-Feb-2013)

Ref Expression
Assertion cfsuc 
|- ( A e. On -> ( cf ` suc A ) = 1o )

Proof

Step Hyp Ref Expression
1 sucelon 
 |-  ( A e. On <-> suc A e. On )
2 cfval 
 |-  ( suc A e. On -> ( cf ` suc A ) = |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) } )
3 1 2 sylbi 
 |-  ( A e. On -> ( cf ` suc A ) = |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) } )
4 cardsn 
 |-  ( A e. On -> ( card ` { A } ) = 1o )
5 4 eqcomd 
 |-  ( A e. On -> 1o = ( card ` { A } ) )
6 snidg 
 |-  ( A e. On -> A e. { A } )
7 elsuci 
 |-  ( z e. suc A -> ( z e. A \/ z = A ) )
8 onelss 
 |-  ( A e. On -> ( z e. A -> z C_ A ) )
9 eqimss 
 |-  ( z = A -> z C_ A )
10 9 a1i 
 |-  ( A e. On -> ( z = A -> z C_ A ) )
11 8 10 jaod 
 |-  ( A e. On -> ( ( z e. A \/ z = A ) -> z C_ A ) )
12 7 11 syl5 
 |-  ( A e. On -> ( z e. suc A -> z C_ A ) )
13 sseq2 
 |-  ( w = A -> ( z C_ w <-> z C_ A ) )
14 13 rspcev 
 |-  ( ( A e. { A } /\ z C_ A ) -> E. w e. { A } z C_ w )
15 6 12 14 syl6an 
 |-  ( A e. On -> ( z e. suc A -> E. w e. { A } z C_ w ) )
16 15 ralrimiv 
 |-  ( A e. On -> A. z e. suc A E. w e. { A } z C_ w )
17 ssun2 
 |-  { A } C_ ( A u. { A } )
18 df-suc 
 |-  suc A = ( A u. { A } )
19 17 18 sseqtrri 
 |-  { A } C_ suc A
20 16 19 jctil 
 |-  ( A e. On -> ( { A } C_ suc A /\ A. z e. suc A E. w e. { A } z C_ w ) )
21 snex 
 |-  { A } e. _V
22 fveq2 
 |-  ( y = { A } -> ( card ` y ) = ( card ` { A } ) )
23 22 eqeq2d 
 |-  ( y = { A } -> ( 1o = ( card ` y ) <-> 1o = ( card ` { A } ) ) )
24 sseq1 
 |-  ( y = { A } -> ( y C_ suc A <-> { A } C_ suc A ) )
25 rexeq 
 |-  ( y = { A } -> ( E. w e. y z C_ w <-> E. w e. { A } z C_ w ) )
26 25 ralbidv 
 |-  ( y = { A } -> ( A. z e. suc A E. w e. y z C_ w <-> A. z e. suc A E. w e. { A } z C_ w ) )
27 24 26 anbi12d 
 |-  ( y = { A } -> ( ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) <-> ( { A } C_ suc A /\ A. z e. suc A E. w e. { A } z C_ w ) ) )
28 23 27 anbi12d 
 |-  ( y = { A } -> ( ( 1o = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) <-> ( 1o = ( card ` { A } ) /\ ( { A } C_ suc A /\ A. z e. suc A E. w e. { A } z C_ w ) ) ) )
29 21 28 spcev 
 |-  ( ( 1o = ( card ` { A } ) /\ ( { A } C_ suc A /\ A. z e. suc A E. w e. { A } z C_ w ) ) -> E. y ( 1o = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) )
30 5 20 29 syl2anc 
 |-  ( A e. On -> E. y ( 1o = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) )
31 1oex 
 |-  1o e. _V
32 eqeq1 
 |-  ( x = 1o -> ( x = ( card ` y ) <-> 1o = ( card ` y ) ) )
33 32 anbi1d 
 |-  ( x = 1o -> ( ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) <-> ( 1o = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) ) )
34 33 exbidv 
 |-  ( x = 1o -> ( E. y ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) <-> E. y ( 1o = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) ) )
35 31 34 elab 
 |-  ( 1o e. { x | E. y ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) } <-> E. y ( 1o = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) )
36 30 35 sylibr 
 |-  ( A e. On -> 1o e. { x | E. y ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) } )
37 el1o 
 |-  ( v e. 1o <-> v = (/) )
38 eqcom 
 |-  ( (/) = ( card ` y ) <-> ( card ` y ) = (/) )
39 vex 
 |-  y e. _V
40 onssnum 
 |-  ( ( y e. _V /\ y C_ On ) -> y e. dom card )
41 39 40 mpan 
 |-  ( y C_ On -> y e. dom card )
42 cardnueq0 
 |-  ( y e. dom card -> ( ( card ` y ) = (/) <-> y = (/) ) )
43 41 42 syl 
 |-  ( y C_ On -> ( ( card ` y ) = (/) <-> y = (/) ) )
44 38 43 bitrid 
 |-  ( y C_ On -> ( (/) = ( card ` y ) <-> y = (/) ) )
45 44 biimpa 
 |-  ( ( y C_ On /\ (/) = ( card ` y ) ) -> y = (/) )
46 rex0 
 |-  -. E. w e. (/) z C_ w
47 46 a1i 
 |-  ( z e. suc A -> -. E. w e. (/) z C_ w )
48 47 nrex 
 |-  -. E. z e. suc A E. w e. (/) z C_ w
49 nsuceq0 
 |-  suc A =/= (/)
50 r19.2z 
 |-  ( ( suc A =/= (/) /\ A. z e. suc A E. w e. (/) z C_ w ) -> E. z e. suc A E. w e. (/) z C_ w )
51 49 50 mpan 
 |-  ( A. z e. suc A E. w e. (/) z C_ w -> E. z e. suc A E. w e. (/) z C_ w )
52 48 51 mto 
 |-  -. A. z e. suc A E. w e. (/) z C_ w
53 rexeq 
 |-  ( y = (/) -> ( E. w e. y z C_ w <-> E. w e. (/) z C_ w ) )
54 53 ralbidv 
 |-  ( y = (/) -> ( A. z e. suc A E. w e. y z C_ w <-> A. z e. suc A E. w e. (/) z C_ w ) )
55 52 54 mtbiri 
 |-  ( y = (/) -> -. A. z e. suc A E. w e. y z C_ w )
56 45 55 syl 
 |-  ( ( y C_ On /\ (/) = ( card ` y ) ) -> -. A. z e. suc A E. w e. y z C_ w )
57 56 intnand 
 |-  ( ( y C_ On /\ (/) = ( card ` y ) ) -> -. ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) )
58 imnan 
 |-  ( ( ( y C_ On /\ (/) = ( card ` y ) ) -> -. ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) <-> -. ( ( y C_ On /\ (/) = ( card ` y ) ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) )
59 57 58 mpbi 
 |-  -. ( ( y C_ On /\ (/) = ( card ` y ) ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) )
60 suceloni 
 |-  ( A e. On -> suc A e. On )
61 onss 
 |-  ( suc A e. On -> suc A C_ On )
62 sstr 
 |-  ( ( y C_ suc A /\ suc A C_ On ) -> y C_ On )
63 61 62 sylan2 
 |-  ( ( y C_ suc A /\ suc A e. On ) -> y C_ On )
64 60 63 sylan2 
 |-  ( ( y C_ suc A /\ A e. On ) -> y C_ On )
65 64 ancoms 
 |-  ( ( A e. On /\ y C_ suc A ) -> y C_ On )
66 65 adantrr 
 |-  ( ( A e. On /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) -> y C_ On )
67 66 3adant2 
 |-  ( ( A e. On /\ (/) = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) -> y C_ On )
68 simp2 
 |-  ( ( A e. On /\ (/) = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) -> (/) = ( card ` y ) )
69 simp3 
 |-  ( ( A e. On /\ (/) = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) -> ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) )
70 67 68 69 jca31 
 |-  ( ( A e. On /\ (/) = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) -> ( ( y C_ On /\ (/) = ( card ` y ) ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) )
71 70 3expib 
 |-  ( A e. On -> ( ( (/) = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) -> ( ( y C_ On /\ (/) = ( card ` y ) ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) ) )
72 59 71 mtoi 
 |-  ( A e. On -> -. ( (/) = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) )
73 72 nexdv 
 |-  ( A e. On -> -. E. y ( (/) = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) )
74 0ex 
 |-  (/) e. _V
75 eqeq1 
 |-  ( x = (/) -> ( x = ( card ` y ) <-> (/) = ( card ` y ) ) )
76 75 anbi1d 
 |-  ( x = (/) -> ( ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) <-> ( (/) = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) ) )
77 76 exbidv 
 |-  ( x = (/) -> ( E. y ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) <-> E. y ( (/) = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) ) )
78 74 77 elab 
 |-  ( (/) e. { x | E. y ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) } <-> E. y ( (/) = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) )
79 73 78 sylnibr 
 |-  ( A e. On -> -. (/) e. { x | E. y ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) } )
80 79 adantr 
 |-  ( ( A e. On /\ v = (/) ) -> -. (/) e. { x | E. y ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) } )
81 eleq1 
 |-  ( v = (/) -> ( v e. { x | E. y ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) } <-> (/) e. { x | E. y ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) } ) )
82 81 adantl 
 |-  ( ( A e. On /\ v = (/) ) -> ( v e. { x | E. y ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) } <-> (/) e. { x | E. y ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) } ) )
83 80 82 mtbird 
 |-  ( ( A e. On /\ v = (/) ) -> -. v e. { x | E. y ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) } )
84 37 83 sylan2b 
 |-  ( ( A e. On /\ v e. 1o ) -> -. v e. { x | E. y ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) } )
85 84 ralrimiva 
 |-  ( A e. On -> A. v e. 1o -. v e. { x | E. y ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) } )
86 cardon 
 |-  ( card ` y ) e. On
87 eleq1 
 |-  ( x = ( card ` y ) -> ( x e. On <-> ( card ` y ) e. On ) )
88 86 87 mpbiri 
 |-  ( x = ( card ` y ) -> x e. On )
89 88 adantr 
 |-  ( ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) -> x e. On )
90 89 exlimiv 
 |-  ( E. y ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) -> x e. On )
91 90 abssi 
 |-  { x | E. y ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) } C_ On
92 oneqmini 
 |-  ( { x | E. y ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) } C_ On -> ( ( 1o e. { x | E. y ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) } /\ A. v e. 1o -. v e. { x | E. y ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) } ) -> 1o = |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) } ) )
93 91 92 ax-mp 
 |-  ( ( 1o e. { x | E. y ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) } /\ A. v e. 1o -. v e. { x | E. y ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) } ) -> 1o = |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) } )
94 36 85 93 syl2anc 
 |-  ( A e. On -> 1o = |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ suc A /\ A. z e. suc A E. w e. y z C_ w ) ) } )
95 3 94 eqtr4d 
 |-  ( A e. On -> ( cf ` suc A ) = 1o )