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