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