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 syl5bb
 |-  ( 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 )