Step |
Hyp |
Ref |
Expression |
1 |
|
alephfnon |
|- aleph Fn On |
2 |
|
fnfun |
|- ( aleph Fn On -> Fun aleph ) |
3 |
1 2
|
ax-mp |
|- Fun aleph |
4 |
|
simpl |
|- ( ( A e. _V /\ Lim A ) -> A e. _V ) |
5 |
|
resfunexg |
|- ( ( Fun aleph /\ A e. _V ) -> ( aleph |` A ) e. _V ) |
6 |
3 4 5
|
sylancr |
|- ( ( A e. _V /\ Lim A ) -> ( aleph |` A ) e. _V ) |
7 |
|
limelon |
|- ( ( A e. _V /\ Lim A ) -> A e. On ) |
8 |
|
onss |
|- ( A e. On -> A C_ On ) |
9 |
7 8
|
syl |
|- ( ( A e. _V /\ Lim A ) -> A C_ On ) |
10 |
|
fnssres |
|- ( ( aleph Fn On /\ A C_ On ) -> ( aleph |` A ) Fn A ) |
11 |
1 9 10
|
sylancr |
|- ( ( A e. _V /\ Lim A ) -> ( aleph |` A ) Fn A ) |
12 |
|
fvres |
|- ( y e. A -> ( ( aleph |` A ) ` y ) = ( aleph ` y ) ) |
13 |
12
|
adantl |
|- ( ( A e. On /\ y e. A ) -> ( ( aleph |` A ) ` y ) = ( aleph ` y ) ) |
14 |
|
alephord2i |
|- ( A e. On -> ( y e. A -> ( aleph ` y ) e. ( aleph ` A ) ) ) |
15 |
14
|
imp |
|- ( ( A e. On /\ y e. A ) -> ( aleph ` y ) e. ( aleph ` A ) ) |
16 |
13 15
|
eqeltrd |
|- ( ( A e. On /\ y e. A ) -> ( ( aleph |` A ) ` y ) e. ( aleph ` A ) ) |
17 |
7 16
|
sylan |
|- ( ( ( A e. _V /\ Lim A ) /\ y e. A ) -> ( ( aleph |` A ) ` y ) e. ( aleph ` A ) ) |
18 |
17
|
ralrimiva |
|- ( ( A e. _V /\ Lim A ) -> A. y e. A ( ( aleph |` A ) ` y ) e. ( aleph ` A ) ) |
19 |
|
fnfvrnss |
|- ( ( ( aleph |` A ) Fn A /\ A. y e. A ( ( aleph |` A ) ` y ) e. ( aleph ` A ) ) -> ran ( aleph |` A ) C_ ( aleph ` A ) ) |
20 |
11 18 19
|
syl2anc |
|- ( ( A e. _V /\ Lim A ) -> ran ( aleph |` A ) C_ ( aleph ` A ) ) |
21 |
|
df-f |
|- ( ( aleph |` A ) : A --> ( aleph ` A ) <-> ( ( aleph |` A ) Fn A /\ ran ( aleph |` A ) C_ ( aleph ` A ) ) ) |
22 |
11 20 21
|
sylanbrc |
|- ( ( A e. _V /\ Lim A ) -> ( aleph |` A ) : A --> ( aleph ` A ) ) |
23 |
|
alephsmo |
|- Smo aleph |
24 |
1
|
fndmi |
|- dom aleph = On |
25 |
7 24
|
eleqtrrdi |
|- ( ( A e. _V /\ Lim A ) -> A e. dom aleph ) |
26 |
|
smores |
|- ( ( Smo aleph /\ A e. dom aleph ) -> Smo ( aleph |` A ) ) |
27 |
23 25 26
|
sylancr |
|- ( ( A e. _V /\ Lim A ) -> Smo ( aleph |` A ) ) |
28 |
|
alephlim |
|- ( ( A e. _V /\ Lim A ) -> ( aleph ` A ) = U_ y e. A ( aleph ` y ) ) |
29 |
28
|
eleq2d |
|- ( ( A e. _V /\ Lim A ) -> ( x e. ( aleph ` A ) <-> x e. U_ y e. A ( aleph ` y ) ) ) |
30 |
|
eliun |
|- ( x e. U_ y e. A ( aleph ` y ) <-> E. y e. A x e. ( aleph ` y ) ) |
31 |
|
alephon |
|- ( aleph ` y ) e. On |
32 |
31
|
onelssi |
|- ( x e. ( aleph ` y ) -> x C_ ( aleph ` y ) ) |
33 |
32
|
reximi |
|- ( E. y e. A x e. ( aleph ` y ) -> E. y e. A x C_ ( aleph ` y ) ) |
34 |
30 33
|
sylbi |
|- ( x e. U_ y e. A ( aleph ` y ) -> E. y e. A x C_ ( aleph ` y ) ) |
35 |
29 34
|
syl6bi |
|- ( ( A e. _V /\ Lim A ) -> ( x e. ( aleph ` A ) -> E. y e. A x C_ ( aleph ` y ) ) ) |
36 |
35
|
ralrimiv |
|- ( ( A e. _V /\ Lim A ) -> A. x e. ( aleph ` A ) E. y e. A x C_ ( aleph ` y ) ) |
37 |
|
feq1 |
|- ( f = ( aleph |` A ) -> ( f : A --> ( aleph ` A ) <-> ( aleph |` A ) : A --> ( aleph ` A ) ) ) |
38 |
|
smoeq |
|- ( f = ( aleph |` A ) -> ( Smo f <-> Smo ( aleph |` A ) ) ) |
39 |
|
fveq1 |
|- ( f = ( aleph |` A ) -> ( f ` y ) = ( ( aleph |` A ) ` y ) ) |
40 |
39 12
|
sylan9eq |
|- ( ( f = ( aleph |` A ) /\ y e. A ) -> ( f ` y ) = ( aleph ` y ) ) |
41 |
40
|
sseq2d |
|- ( ( f = ( aleph |` A ) /\ y e. A ) -> ( x C_ ( f ` y ) <-> x C_ ( aleph ` y ) ) ) |
42 |
41
|
rexbidva |
|- ( f = ( aleph |` A ) -> ( E. y e. A x C_ ( f ` y ) <-> E. y e. A x C_ ( aleph ` y ) ) ) |
43 |
42
|
ralbidv |
|- ( f = ( aleph |` A ) -> ( A. x e. ( aleph ` A ) E. y e. A x C_ ( f ` y ) <-> A. x e. ( aleph ` A ) E. y e. A x C_ ( aleph ` y ) ) ) |
44 |
37 38 43
|
3anbi123d |
|- ( f = ( aleph |` A ) -> ( ( f : A --> ( aleph ` A ) /\ Smo f /\ A. x e. ( aleph ` A ) E. y e. A x C_ ( f ` y ) ) <-> ( ( aleph |` A ) : A --> ( aleph ` A ) /\ Smo ( aleph |` A ) /\ A. x e. ( aleph ` A ) E. y e. A x C_ ( aleph ` y ) ) ) ) |
45 |
44
|
spcegv |
|- ( ( aleph |` A ) e. _V -> ( ( ( aleph |` A ) : A --> ( aleph ` A ) /\ Smo ( aleph |` A ) /\ A. x e. ( aleph ` A ) E. y e. A x C_ ( aleph ` y ) ) -> E. f ( f : A --> ( aleph ` A ) /\ Smo f /\ A. x e. ( aleph ` A ) E. y e. A x C_ ( f ` y ) ) ) ) |
46 |
45
|
imp |
|- ( ( ( aleph |` A ) e. _V /\ ( ( aleph |` A ) : A --> ( aleph ` A ) /\ Smo ( aleph |` A ) /\ A. x e. ( aleph ` A ) E. y e. A x C_ ( aleph ` y ) ) ) -> E. f ( f : A --> ( aleph ` A ) /\ Smo f /\ A. x e. ( aleph ` A ) E. y e. A x C_ ( f ` y ) ) ) |
47 |
6 22 27 36 46
|
syl13anc |
|- ( ( A e. _V /\ Lim A ) -> E. f ( f : A --> ( aleph ` A ) /\ Smo f /\ A. x e. ( aleph ` A ) E. y e. A x C_ ( f ` y ) ) ) |
48 |
|
alephon |
|- ( aleph ` A ) e. On |
49 |
|
cfcof |
|- ( ( ( aleph ` A ) e. On /\ A e. On ) -> ( E. f ( f : A --> ( aleph ` A ) /\ Smo f /\ A. x e. ( aleph ` A ) E. y e. A x C_ ( f ` y ) ) -> ( cf ` ( aleph ` A ) ) = ( cf ` A ) ) ) |
50 |
48 7 49
|
sylancr |
|- ( ( A e. _V /\ Lim A ) -> ( E. f ( f : A --> ( aleph ` A ) /\ Smo f /\ A. x e. ( aleph ` A ) E. y e. A x C_ ( f ` y ) ) -> ( cf ` ( aleph ` A ) ) = ( cf ` A ) ) ) |
51 |
47 50
|
mpd |
|- ( ( A e. _V /\ Lim A ) -> ( cf ` ( aleph ` A ) ) = ( cf ` A ) ) |
52 |
51
|
expcom |
|- ( Lim A -> ( A e. _V -> ( cf ` ( aleph ` A ) ) = ( cf ` A ) ) ) |
53 |
|
cf0 |
|- ( cf ` (/) ) = (/) |
54 |
|
fvprc |
|- ( -. A e. _V -> ( aleph ` A ) = (/) ) |
55 |
54
|
fveq2d |
|- ( -. A e. _V -> ( cf ` ( aleph ` A ) ) = ( cf ` (/) ) ) |
56 |
|
fvprc |
|- ( -. A e. _V -> ( cf ` A ) = (/) ) |
57 |
53 55 56
|
3eqtr4a |
|- ( -. A e. _V -> ( cf ` ( aleph ` A ) ) = ( cf ` A ) ) |
58 |
52 57
|
pm2.61d1 |
|- ( Lim A -> ( cf ` ( aleph ` A ) ) = ( cf ` A ) ) |