Metamath Proof Explorer


Theorem cflim2

Description: The cofinality function is a limit ordinal iff its argument is. (Contributed by Mario Carneiro, 28-Feb-2013) (Revised by Mario Carneiro, 15-Sep-2013)

Ref Expression
Hypothesis cflim2.1
|- A e. _V
Assertion cflim2
|- ( Lim A <-> Lim ( cf ` A ) )

Proof

Step Hyp Ref Expression
1 cflim2.1
 |-  A e. _V
2 rabid
 |-  ( y e. { y e. ~P A | U. y = A } <-> ( y e. ~P A /\ U. y = A ) )
3 velpw
 |-  ( y e. ~P A <-> y C_ A )
4 limord
 |-  ( Lim A -> Ord A )
5 ordsson
 |-  ( Ord A -> A C_ On )
6 sstr
 |-  ( ( y C_ A /\ A C_ On ) -> y C_ On )
7 6 expcom
 |-  ( A C_ On -> ( y C_ A -> y C_ On ) )
8 4 5 7 3syl
 |-  ( Lim A -> ( y C_ A -> y C_ On ) )
9 8 imp
 |-  ( ( Lim A /\ y C_ A ) -> y C_ On )
10 9 3adant3
 |-  ( ( Lim A /\ y C_ A /\ U. y = A ) -> y C_ On )
11 ssel2
 |-  ( ( y C_ On /\ s e. y ) -> s e. On )
12 eloni
 |-  ( s e. On -> Ord s )
13 ordirr
 |-  ( Ord s -> -. s e. s )
14 11 12 13 3syl
 |-  ( ( y C_ On /\ s e. y ) -> -. s e. s )
15 ssel
 |-  ( y C_ s -> ( s e. y -> s e. s ) )
16 15 com12
 |-  ( s e. y -> ( y C_ s -> s e. s ) )
17 16 adantl
 |-  ( ( y C_ On /\ s e. y ) -> ( y C_ s -> s e. s ) )
18 14 17 mtod
 |-  ( ( y C_ On /\ s e. y ) -> -. y C_ s )
19 10 18 sylan
 |-  ( ( ( Lim A /\ y C_ A /\ U. y = A ) /\ s e. y ) -> -. y C_ s )
20 simpl2
 |-  ( ( ( Lim A /\ y C_ A /\ U. y = A ) /\ s e. y ) -> y C_ A )
21 sstr
 |-  ( ( y C_ A /\ A C_ s ) -> y C_ s )
22 20 21 sylan
 |-  ( ( ( ( Lim A /\ y C_ A /\ U. y = A ) /\ s e. y ) /\ A C_ s ) -> y C_ s )
23 19 22 mtand
 |-  ( ( ( Lim A /\ y C_ A /\ U. y = A ) /\ s e. y ) -> -. A C_ s )
24 simpl3
 |-  ( ( ( Lim A /\ y C_ A /\ U. y = A ) /\ s e. y ) -> U. y = A )
25 24 sseq1d
 |-  ( ( ( Lim A /\ y C_ A /\ U. y = A ) /\ s e. y ) -> ( U. y C_ s <-> A C_ s ) )
26 23 25 mtbird
 |-  ( ( ( Lim A /\ y C_ A /\ U. y = A ) /\ s e. y ) -> -. U. y C_ s )
27 unissb
 |-  ( U. y C_ s <-> A. t e. y t C_ s )
28 26 27 sylnib
 |-  ( ( ( Lim A /\ y C_ A /\ U. y = A ) /\ s e. y ) -> -. A. t e. y t C_ s )
29 28 nrexdv
 |-  ( ( Lim A /\ y C_ A /\ U. y = A ) -> -. E. s e. y A. t e. y t C_ s )
30 ssel
 |-  ( y C_ On -> ( s e. y -> s e. On ) )
31 ssel
 |-  ( y C_ On -> ( t e. y -> t e. On ) )
32 ontri1
 |-  ( ( t e. On /\ s e. On ) -> ( t C_ s <-> -. s e. t ) )
33 32 ancoms
 |-  ( ( s e. On /\ t e. On ) -> ( t C_ s <-> -. s e. t ) )
34 vex
 |-  t e. _V
35 vex
 |-  s e. _V
36 34 35 brcnv
 |-  ( t `' _E s <-> s _E t )
37 epel
 |-  ( s _E t <-> s e. t )
38 36 37 bitri
 |-  ( t `' _E s <-> s e. t )
39 38 notbii
 |-  ( -. t `' _E s <-> -. s e. t )
40 33 39 bitr4di
 |-  ( ( s e. On /\ t e. On ) -> ( t C_ s <-> -. t `' _E s ) )
41 40 a1i
 |-  ( y C_ On -> ( ( s e. On /\ t e. On ) -> ( t C_ s <-> -. t `' _E s ) ) )
42 30 31 41 syl2and
 |-  ( y C_ On -> ( ( s e. y /\ t e. y ) -> ( t C_ s <-> -. t `' _E s ) ) )
43 42 impl
 |-  ( ( ( y C_ On /\ s e. y ) /\ t e. y ) -> ( t C_ s <-> -. t `' _E s ) )
44 43 ralbidva
 |-  ( ( y C_ On /\ s e. y ) -> ( A. t e. y t C_ s <-> A. t e. y -. t `' _E s ) )
45 44 rexbidva
 |-  ( y C_ On -> ( E. s e. y A. t e. y t C_ s <-> E. s e. y A. t e. y -. t `' _E s ) )
46 10 45 syl
 |-  ( ( Lim A /\ y C_ A /\ U. y = A ) -> ( E. s e. y A. t e. y t C_ s <-> E. s e. y A. t e. y -. t `' _E s ) )
47 29 46 mtbid
 |-  ( ( Lim A /\ y C_ A /\ U. y = A ) -> -. E. s e. y A. t e. y -. t `' _E s )
48 vex
 |-  y e. _V
49 48 a1i
 |-  ( ( ( Lim A /\ y C_ A /\ U. y = A ) /\ ( card ` y ) e. _om ) -> y e. _V )
50 epweon
 |-  _E We On
51 wess
 |-  ( y C_ On -> ( _E We On -> _E We y ) )
52 50 51 mpi
 |-  ( y C_ On -> _E We y )
53 weso
 |-  ( _E We y -> _E Or y )
54 52 53 syl
 |-  ( y C_ On -> _E Or y )
55 cnvso
 |-  ( _E Or y <-> `' _E Or y )
56 54 55 sylib
 |-  ( y C_ On -> `' _E Or y )
57 onssnum
 |-  ( ( y e. _V /\ y C_ On ) -> y e. dom card )
58 48 57 mpan
 |-  ( y C_ On -> y e. dom card )
59 cardid2
 |-  ( y e. dom card -> ( card ` y ) ~~ y )
60 ensym
 |-  ( ( card ` y ) ~~ y -> y ~~ ( card ` y ) )
61 58 59 60 3syl
 |-  ( y C_ On -> y ~~ ( card ` y ) )
62 nnsdom
 |-  ( ( card ` y ) e. _om -> ( card ` y ) ~< _om )
63 ensdomtr
 |-  ( ( y ~~ ( card ` y ) /\ ( card ` y ) ~< _om ) -> y ~< _om )
64 61 62 63 syl2an
 |-  ( ( y C_ On /\ ( card ` y ) e. _om ) -> y ~< _om )
65 isfinite
 |-  ( y e. Fin <-> y ~< _om )
66 64 65 sylibr
 |-  ( ( y C_ On /\ ( card ` y ) e. _om ) -> y e. Fin )
67 wofi
 |-  ( ( `' _E Or y /\ y e. Fin ) -> `' _E We y )
68 56 66 67 syl2an2r
 |-  ( ( y C_ On /\ ( card ` y ) e. _om ) -> `' _E We y )
69 10 68 sylan
 |-  ( ( ( Lim A /\ y C_ A /\ U. y = A ) /\ ( card ` y ) e. _om ) -> `' _E We y )
70 wefr
 |-  ( `' _E We y -> `' _E Fr y )
71 69 70 syl
 |-  ( ( ( Lim A /\ y C_ A /\ U. y = A ) /\ ( card ` y ) e. _om ) -> `' _E Fr y )
72 ssidd
 |-  ( ( ( Lim A /\ y C_ A /\ U. y = A ) /\ ( card ` y ) e. _om ) -> y C_ y )
73 unieq
 |-  ( y = (/) -> U. y = U. (/) )
74 uni0
 |-  U. (/) = (/)
75 73 74 eqtrdi
 |-  ( y = (/) -> U. y = (/) )
76 eqeq1
 |-  ( U. y = A -> ( U. y = (/) <-> A = (/) ) )
77 75 76 syl5ib
 |-  ( U. y = A -> ( y = (/) -> A = (/) ) )
78 nlim0
 |-  -. Lim (/)
79 limeq
 |-  ( A = (/) -> ( Lim A <-> Lim (/) ) )
80 78 79 mtbiri
 |-  ( A = (/) -> -. Lim A )
81 77 80 syl6
 |-  ( U. y = A -> ( y = (/) -> -. Lim A ) )
82 81 necon2ad
 |-  ( U. y = A -> ( Lim A -> y =/= (/) ) )
83 82 impcom
 |-  ( ( Lim A /\ U. y = A ) -> y =/= (/) )
84 83 3adant2
 |-  ( ( Lim A /\ y C_ A /\ U. y = A ) -> y =/= (/) )
85 84 adantr
 |-  ( ( ( Lim A /\ y C_ A /\ U. y = A ) /\ ( card ` y ) e. _om ) -> y =/= (/) )
86 fri
 |-  ( ( ( y e. _V /\ `' _E Fr y ) /\ ( y C_ y /\ y =/= (/) ) ) -> E. s e. y A. t e. y -. t `' _E s )
87 49 71 72 85 86 syl22anc
 |-  ( ( ( Lim A /\ y C_ A /\ U. y = A ) /\ ( card ` y ) e. _om ) -> E. s e. y A. t e. y -. t `' _E s )
88 47 87 mtand
 |-  ( ( Lim A /\ y C_ A /\ U. y = A ) -> -. ( card ` y ) e. _om )
89 cardon
 |-  ( card ` y ) e. On
90 eloni
 |-  ( ( card ` y ) e. On -> Ord ( card ` y ) )
91 ordom
 |-  Ord _om
92 ordtri1
 |-  ( ( Ord _om /\ Ord ( card ` y ) ) -> ( _om C_ ( card ` y ) <-> -. ( card ` y ) e. _om ) )
93 91 92 mpan
 |-  ( Ord ( card ` y ) -> ( _om C_ ( card ` y ) <-> -. ( card ` y ) e. _om ) )
94 89 90 93 mp2b
 |-  ( _om C_ ( card ` y ) <-> -. ( card ` y ) e. _om )
95 88 94 sylibr
 |-  ( ( Lim A /\ y C_ A /\ U. y = A ) -> _om C_ ( card ` y ) )
96 3 95 syl3an2b
 |-  ( ( Lim A /\ y e. ~P A /\ U. y = A ) -> _om C_ ( card ` y ) )
97 96 3expb
 |-  ( ( Lim A /\ ( y e. ~P A /\ U. y = A ) ) -> _om C_ ( card ` y ) )
98 2 97 sylan2b
 |-  ( ( Lim A /\ y e. { y e. ~P A | U. y = A } ) -> _om C_ ( card ` y ) )
99 98 ralrimiva
 |-  ( Lim A -> A. y e. { y e. ~P A | U. y = A } _om C_ ( card ` y ) )
100 ssiin
 |-  ( _om C_ |^|_ y e. { y e. ~P A | U. y = A } ( card ` y ) <-> A. y e. { y e. ~P A | U. y = A } _om C_ ( card ` y ) )
101 99 100 sylibr
 |-  ( Lim A -> _om C_ |^|_ y e. { y e. ~P A | U. y = A } ( card ` y ) )
102 1 cflim3
 |-  ( Lim A -> ( cf ` A ) = |^|_ y e. { y e. ~P A | U. y = A } ( card ` y ) )
103 101 102 sseqtrrd
 |-  ( Lim A -> _om C_ ( cf ` A ) )
104 fvex
 |-  ( card ` y ) e. _V
105 104 dfiin2
 |-  |^|_ y e. { y e. ~P A | U. y = A } ( card ` y ) = |^| { x | E. y e. { y e. ~P A | U. y = A } x = ( card ` y ) }
106 102 105 eqtrdi
 |-  ( Lim A -> ( cf ` A ) = |^| { x | E. y e. { y e. ~P A | U. y = A } x = ( card ` y ) } )
107 cardlim
 |-  ( _om C_ ( card ` y ) <-> Lim ( card ` y ) )
108 sseq2
 |-  ( x = ( card ` y ) -> ( _om C_ x <-> _om C_ ( card ` y ) ) )
109 limeq
 |-  ( x = ( card ` y ) -> ( Lim x <-> Lim ( card ` y ) ) )
110 108 109 bibi12d
 |-  ( x = ( card ` y ) -> ( ( _om C_ x <-> Lim x ) <-> ( _om C_ ( card ` y ) <-> Lim ( card ` y ) ) ) )
111 107 110 mpbiri
 |-  ( x = ( card ` y ) -> ( _om C_ x <-> Lim x ) )
112 111 rexlimivw
 |-  ( E. y e. { y e. ~P A | U. y = A } x = ( card ` y ) -> ( _om C_ x <-> Lim x ) )
113 112 ss2abi
 |-  { x | E. y e. { y e. ~P A | U. y = A } x = ( card ` y ) } C_ { x | ( _om C_ x <-> Lim x ) }
114 eleq1
 |-  ( x = ( card ` y ) -> ( x e. On <-> ( card ` y ) e. On ) )
115 89 114 mpbiri
 |-  ( x = ( card ` y ) -> x e. On )
116 115 rexlimivw
 |-  ( E. y e. { y e. ~P A | U. y = A } x = ( card ` y ) -> x e. On )
117 116 abssi
 |-  { x | E. y e. { y e. ~P A | U. y = A } x = ( card ` y ) } C_ On
118 fvex
 |-  ( cf ` A ) e. _V
119 106 118 eqeltrrdi
 |-  ( Lim A -> |^| { x | E. y e. { y e. ~P A | U. y = A } x = ( card ` y ) } e. _V )
120 intex
 |-  ( { x | E. y e. { y e. ~P A | U. y = A } x = ( card ` y ) } =/= (/) <-> |^| { x | E. y e. { y e. ~P A | U. y = A } x = ( card ` y ) } e. _V )
121 119 120 sylibr
 |-  ( Lim A -> { x | E. y e. { y e. ~P A | U. y = A } x = ( card ` y ) } =/= (/) )
122 onint
 |-  ( ( { x | E. y e. { y e. ~P A | U. y = A } x = ( card ` y ) } C_ On /\ { x | E. y e. { y e. ~P A | U. y = A } x = ( card ` y ) } =/= (/) ) -> |^| { x | E. y e. { y e. ~P A | U. y = A } x = ( card ` y ) } e. { x | E. y e. { y e. ~P A | U. y = A } x = ( card ` y ) } )
123 117 121 122 sylancr
 |-  ( Lim A -> |^| { x | E. y e. { y e. ~P A | U. y = A } x = ( card ` y ) } e. { x | E. y e. { y e. ~P A | U. y = A } x = ( card ` y ) } )
124 113 123 sselid
 |-  ( Lim A -> |^| { x | E. y e. { y e. ~P A | U. y = A } x = ( card ` y ) } e. { x | ( _om C_ x <-> Lim x ) } )
125 106 124 eqeltrd
 |-  ( Lim A -> ( cf ` A ) e. { x | ( _om C_ x <-> Lim x ) } )
126 sseq2
 |-  ( x = ( cf ` A ) -> ( _om C_ x <-> _om C_ ( cf ` A ) ) )
127 limeq
 |-  ( x = ( cf ` A ) -> ( Lim x <-> Lim ( cf ` A ) ) )
128 126 127 bibi12d
 |-  ( x = ( cf ` A ) -> ( ( _om C_ x <-> Lim x ) <-> ( _om C_ ( cf ` A ) <-> Lim ( cf ` A ) ) ) )
129 118 128 elab
 |-  ( ( cf ` A ) e. { x | ( _om C_ x <-> Lim x ) } <-> ( _om C_ ( cf ` A ) <-> Lim ( cf ` A ) ) )
130 125 129 sylib
 |-  ( Lim A -> ( _om C_ ( cf ` A ) <-> Lim ( cf ` A ) ) )
131 103 130 mpbid
 |-  ( Lim A -> Lim ( cf ` A ) )
132 eloni
 |-  ( A e. On -> Ord A )
133 ordzsl
 |-  ( Ord A <-> ( A = (/) \/ E. x e. On A = suc x \/ Lim A ) )
134 132 133 sylib
 |-  ( A e. On -> ( A = (/) \/ E. x e. On A = suc x \/ Lim A ) )
135 df-3or
 |-  ( ( A = (/) \/ E. x e. On A = suc x \/ Lim A ) <-> ( ( A = (/) \/ E. x e. On A = suc x ) \/ Lim A ) )
136 orcom
 |-  ( ( ( A = (/) \/ E. x e. On A = suc x ) \/ Lim A ) <-> ( Lim A \/ ( A = (/) \/ E. x e. On A = suc x ) ) )
137 df-or
 |-  ( ( Lim A \/ ( A = (/) \/ E. x e. On A = suc x ) ) <-> ( -. Lim A -> ( A = (/) \/ E. x e. On A = suc x ) ) )
138 135 136 137 3bitri
 |-  ( ( A = (/) \/ E. x e. On A = suc x \/ Lim A ) <-> ( -. Lim A -> ( A = (/) \/ E. x e. On A = suc x ) ) )
139 134 138 sylib
 |-  ( A e. On -> ( -. Lim A -> ( A = (/) \/ E. x e. On A = suc x ) ) )
140 fveq2
 |-  ( A = (/) -> ( cf ` A ) = ( cf ` (/) ) )
141 cf0
 |-  ( cf ` (/) ) = (/)
142 140 141 eqtrdi
 |-  ( A = (/) -> ( cf ` A ) = (/) )
143 limeq
 |-  ( ( cf ` A ) = (/) -> ( Lim ( cf ` A ) <-> Lim (/) ) )
144 142 143 syl
 |-  ( A = (/) -> ( Lim ( cf ` A ) <-> Lim (/) ) )
145 78 144 mtbiri
 |-  ( A = (/) -> -. Lim ( cf ` A ) )
146 1n0
 |-  1o =/= (/)
147 df1o2
 |-  1o = { (/) }
148 147 unieqi
 |-  U. 1o = U. { (/) }
149 0ex
 |-  (/) e. _V
150 149 unisn
 |-  U. { (/) } = (/)
151 148 150 eqtri
 |-  U. 1o = (/)
152 146 151 neeqtrri
 |-  1o =/= U. 1o
153 limuni
 |-  ( Lim 1o -> 1o = U. 1o )
154 153 necon3ai
 |-  ( 1o =/= U. 1o -> -. Lim 1o )
155 152 154 ax-mp
 |-  -. Lim 1o
156 fveq2
 |-  ( A = suc x -> ( cf ` A ) = ( cf ` suc x ) )
157 cfsuc
 |-  ( x e. On -> ( cf ` suc x ) = 1o )
158 156 157 sylan9eqr
 |-  ( ( x e. On /\ A = suc x ) -> ( cf ` A ) = 1o )
159 limeq
 |-  ( ( cf ` A ) = 1o -> ( Lim ( cf ` A ) <-> Lim 1o ) )
160 158 159 syl
 |-  ( ( x e. On /\ A = suc x ) -> ( Lim ( cf ` A ) <-> Lim 1o ) )
161 155 160 mtbiri
 |-  ( ( x e. On /\ A = suc x ) -> -. Lim ( cf ` A ) )
162 161 rexlimiva
 |-  ( E. x e. On A = suc x -> -. Lim ( cf ` A ) )
163 145 162 jaoi
 |-  ( ( A = (/) \/ E. x e. On A = suc x ) -> -. Lim ( cf ` A ) )
164 139 163 syl6
 |-  ( A e. On -> ( -. Lim A -> -. Lim ( cf ` A ) ) )
165 164 con4d
 |-  ( A e. On -> ( Lim ( cf ` A ) -> Lim A ) )
166 cff
 |-  cf : On --> On
167 166 fdmi
 |-  dom cf = On
168 167 eleq2i
 |-  ( A e. dom cf <-> A e. On )
169 ndmfv
 |-  ( -. A e. dom cf -> ( cf ` A ) = (/) )
170 168 169 sylnbir
 |-  ( -. A e. On -> ( cf ` A ) = (/) )
171 170 143 syl
 |-  ( -. A e. On -> ( Lim ( cf ` A ) <-> Lim (/) ) )
172 78 171 mtbiri
 |-  ( -. A e. On -> -. Lim ( cf ` A ) )
173 172 pm2.21d
 |-  ( -. A e. On -> ( Lim ( cf ` A ) -> Lim A ) )
174 165 173 pm2.61i
 |-  ( Lim ( cf ` A ) -> Lim A )
175 131 174 impbii
 |-  ( Lim A <-> Lim ( cf ` A ) )