Step |
Hyp |
Ref |
Expression |
1 |
|
alephfnon |
|- aleph Fn On |
2 |
|
fveq2 |
|- ( x = (/) -> ( aleph ` x ) = ( aleph ` (/) ) ) |
3 |
2
|
eleq1d |
|- ( x = (/) -> ( ( aleph ` x ) e. On <-> ( aleph ` (/) ) e. On ) ) |
4 |
|
fveq2 |
|- ( x = y -> ( aleph ` x ) = ( aleph ` y ) ) |
5 |
4
|
eleq1d |
|- ( x = y -> ( ( aleph ` x ) e. On <-> ( aleph ` y ) e. On ) ) |
6 |
|
fveq2 |
|- ( x = suc y -> ( aleph ` x ) = ( aleph ` suc y ) ) |
7 |
6
|
eleq1d |
|- ( x = suc y -> ( ( aleph ` x ) e. On <-> ( aleph ` suc y ) e. On ) ) |
8 |
|
aleph0 |
|- ( aleph ` (/) ) = _om |
9 |
|
omelon |
|- _om e. On |
10 |
8 9
|
eqeltri |
|- ( aleph ` (/) ) e. On |
11 |
|
alephsuc |
|- ( y e. On -> ( aleph ` suc y ) = ( har ` ( aleph ` y ) ) ) |
12 |
|
harcl |
|- ( har ` ( aleph ` y ) ) e. On |
13 |
11 12
|
eqeltrdi |
|- ( y e. On -> ( aleph ` suc y ) e. On ) |
14 |
13
|
a1d |
|- ( y e. On -> ( ( aleph ` y ) e. On -> ( aleph ` suc y ) e. On ) ) |
15 |
|
vex |
|- x e. _V |
16 |
|
iunon |
|- ( ( x e. _V /\ A. y e. x ( aleph ` y ) e. On ) -> U_ y e. x ( aleph ` y ) e. On ) |
17 |
15 16
|
mpan |
|- ( A. y e. x ( aleph ` y ) e. On -> U_ y e. x ( aleph ` y ) e. On ) |
18 |
|
alephlim |
|- ( ( x e. _V /\ Lim x ) -> ( aleph ` x ) = U_ y e. x ( aleph ` y ) ) |
19 |
15 18
|
mpan |
|- ( Lim x -> ( aleph ` x ) = U_ y e. x ( aleph ` y ) ) |
20 |
19
|
eleq1d |
|- ( Lim x -> ( ( aleph ` x ) e. On <-> U_ y e. x ( aleph ` y ) e. On ) ) |
21 |
17 20
|
syl5ibr |
|- ( Lim x -> ( A. y e. x ( aleph ` y ) e. On -> ( aleph ` x ) e. On ) ) |
22 |
3 5 7 5 10 14 21
|
tfinds |
|- ( y e. On -> ( aleph ` y ) e. On ) |
23 |
22
|
rgen |
|- A. y e. On ( aleph ` y ) e. On |
24 |
|
ffnfv |
|- ( aleph : On --> On <-> ( aleph Fn On /\ A. y e. On ( aleph ` y ) e. On ) ) |
25 |
1 23 24
|
mpbir2an |
|- aleph : On --> On |
26 |
|
0elon |
|- (/) e. On |
27 |
25 26
|
f0cli |
|- ( aleph ` A ) e. On |