Step |
Hyp |
Ref |
Expression |
1 |
|
alephfplem.1 |
|- H = ( rec ( aleph , _om ) |` _om ) |
2 |
1
|
alephfplem4 |
|- U. ( H " _om ) e. ran aleph |
3 |
|
isinfcard |
|- ( ( _om C_ U. ( H " _om ) /\ ( card ` U. ( H " _om ) ) = U. ( H " _om ) ) <-> U. ( H " _om ) e. ran aleph ) |
4 |
|
cardalephex |
|- ( _om C_ U. ( H " _om ) -> ( ( card ` U. ( H " _om ) ) = U. ( H " _om ) <-> E. z e. On U. ( H " _om ) = ( aleph ` z ) ) ) |
5 |
4
|
biimpa |
|- ( ( _om C_ U. ( H " _om ) /\ ( card ` U. ( H " _om ) ) = U. ( H " _om ) ) -> E. z e. On U. ( H " _om ) = ( aleph ` z ) ) |
6 |
3 5
|
sylbir |
|- ( U. ( H " _om ) e. ran aleph -> E. z e. On U. ( H " _om ) = ( aleph ` z ) ) |
7 |
|
alephle |
|- ( z e. On -> z C_ ( aleph ` z ) ) |
8 |
|
alephon |
|- ( aleph ` z ) e. On |
9 |
8
|
onirri |
|- -. ( aleph ` z ) e. ( aleph ` z ) |
10 |
|
frfnom |
|- ( rec ( aleph , _om ) |` _om ) Fn _om |
11 |
1
|
fneq1i |
|- ( H Fn _om <-> ( rec ( aleph , _om ) |` _om ) Fn _om ) |
12 |
10 11
|
mpbir |
|- H Fn _om |
13 |
|
fnfun |
|- ( H Fn _om -> Fun H ) |
14 |
|
eluniima |
|- ( Fun H -> ( z e. U. ( H " _om ) <-> E. v e. _om z e. ( H ` v ) ) ) |
15 |
12 13 14
|
mp2b |
|- ( z e. U. ( H " _om ) <-> E. v e. _om z e. ( H ` v ) ) |
16 |
|
alephsson |
|- ran aleph C_ On |
17 |
1
|
alephfplem3 |
|- ( v e. _om -> ( H ` v ) e. ran aleph ) |
18 |
16 17
|
sselid |
|- ( v e. _om -> ( H ` v ) e. On ) |
19 |
|
alephord2i |
|- ( ( H ` v ) e. On -> ( z e. ( H ` v ) -> ( aleph ` z ) e. ( aleph ` ( H ` v ) ) ) ) |
20 |
18 19
|
syl |
|- ( v e. _om -> ( z e. ( H ` v ) -> ( aleph ` z ) e. ( aleph ` ( H ` v ) ) ) ) |
21 |
1
|
alephfplem2 |
|- ( v e. _om -> ( H ` suc v ) = ( aleph ` ( H ` v ) ) ) |
22 |
|
peano2 |
|- ( v e. _om -> suc v e. _om ) |
23 |
|
fnfvelrn |
|- ( ( H Fn _om /\ suc v e. _om ) -> ( H ` suc v ) e. ran H ) |
24 |
12 23
|
mpan |
|- ( suc v e. _om -> ( H ` suc v ) e. ran H ) |
25 |
|
fnima |
|- ( H Fn _om -> ( H " _om ) = ran H ) |
26 |
12 25
|
ax-mp |
|- ( H " _om ) = ran H |
27 |
24 26
|
eleqtrrdi |
|- ( suc v e. _om -> ( H ` suc v ) e. ( H " _om ) ) |
28 |
22 27
|
syl |
|- ( v e. _om -> ( H ` suc v ) e. ( H " _om ) ) |
29 |
21 28
|
eqeltrrd |
|- ( v e. _om -> ( aleph ` ( H ` v ) ) e. ( H " _om ) ) |
30 |
|
elssuni |
|- ( ( aleph ` ( H ` v ) ) e. ( H " _om ) -> ( aleph ` ( H ` v ) ) C_ U. ( H " _om ) ) |
31 |
29 30
|
syl |
|- ( v e. _om -> ( aleph ` ( H ` v ) ) C_ U. ( H " _om ) ) |
32 |
31
|
sseld |
|- ( v e. _om -> ( ( aleph ` z ) e. ( aleph ` ( H ` v ) ) -> ( aleph ` z ) e. U. ( H " _om ) ) ) |
33 |
20 32
|
syld |
|- ( v e. _om -> ( z e. ( H ` v ) -> ( aleph ` z ) e. U. ( H " _om ) ) ) |
34 |
33
|
rexlimiv |
|- ( E. v e. _om z e. ( H ` v ) -> ( aleph ` z ) e. U. ( H " _om ) ) |
35 |
15 34
|
sylbi |
|- ( z e. U. ( H " _om ) -> ( aleph ` z ) e. U. ( H " _om ) ) |
36 |
|
eleq2 |
|- ( U. ( H " _om ) = ( aleph ` z ) -> ( z e. U. ( H " _om ) <-> z e. ( aleph ` z ) ) ) |
37 |
|
eleq2 |
|- ( U. ( H " _om ) = ( aleph ` z ) -> ( ( aleph ` z ) e. U. ( H " _om ) <-> ( aleph ` z ) e. ( aleph ` z ) ) ) |
38 |
36 37
|
imbi12d |
|- ( U. ( H " _om ) = ( aleph ` z ) -> ( ( z e. U. ( H " _om ) -> ( aleph ` z ) e. U. ( H " _om ) ) <-> ( z e. ( aleph ` z ) -> ( aleph ` z ) e. ( aleph ` z ) ) ) ) |
39 |
35 38
|
mpbii |
|- ( U. ( H " _om ) = ( aleph ` z ) -> ( z e. ( aleph ` z ) -> ( aleph ` z ) e. ( aleph ` z ) ) ) |
40 |
9 39
|
mtoi |
|- ( U. ( H " _om ) = ( aleph ` z ) -> -. z e. ( aleph ` z ) ) |
41 |
7 40
|
anim12i |
|- ( ( z e. On /\ U. ( H " _om ) = ( aleph ` z ) ) -> ( z C_ ( aleph ` z ) /\ -. z e. ( aleph ` z ) ) ) |
42 |
|
eloni |
|- ( z e. On -> Ord z ) |
43 |
8
|
onordi |
|- Ord ( aleph ` z ) |
44 |
|
ordtri4 |
|- ( ( Ord z /\ Ord ( aleph ` z ) ) -> ( z = ( aleph ` z ) <-> ( z C_ ( aleph ` z ) /\ -. z e. ( aleph ` z ) ) ) ) |
45 |
42 43 44
|
sylancl |
|- ( z e. On -> ( z = ( aleph ` z ) <-> ( z C_ ( aleph ` z ) /\ -. z e. ( aleph ` z ) ) ) ) |
46 |
45
|
adantr |
|- ( ( z e. On /\ U. ( H " _om ) = ( aleph ` z ) ) -> ( z = ( aleph ` z ) <-> ( z C_ ( aleph ` z ) /\ -. z e. ( aleph ` z ) ) ) ) |
47 |
41 46
|
mpbird |
|- ( ( z e. On /\ U. ( H " _om ) = ( aleph ` z ) ) -> z = ( aleph ` z ) ) |
48 |
|
eqeq2 |
|- ( U. ( H " _om ) = ( aleph ` z ) -> ( z = U. ( H " _om ) <-> z = ( aleph ` z ) ) ) |
49 |
48
|
adantl |
|- ( ( z e. On /\ U. ( H " _om ) = ( aleph ` z ) ) -> ( z = U. ( H " _om ) <-> z = ( aleph ` z ) ) ) |
50 |
47 49
|
mpbird |
|- ( ( z e. On /\ U. ( H " _om ) = ( aleph ` z ) ) -> z = U. ( H " _om ) ) |
51 |
50
|
eqcomd |
|- ( ( z e. On /\ U. ( H " _om ) = ( aleph ` z ) ) -> U. ( H " _om ) = z ) |
52 |
51
|
fveq2d |
|- ( ( z e. On /\ U. ( H " _om ) = ( aleph ` z ) ) -> ( aleph ` U. ( H " _om ) ) = ( aleph ` z ) ) |
53 |
|
eqeq2 |
|- ( U. ( H " _om ) = ( aleph ` z ) -> ( ( aleph ` U. ( H " _om ) ) = U. ( H " _om ) <-> ( aleph ` U. ( H " _om ) ) = ( aleph ` z ) ) ) |
54 |
53
|
adantl |
|- ( ( z e. On /\ U. ( H " _om ) = ( aleph ` z ) ) -> ( ( aleph ` U. ( H " _om ) ) = U. ( H " _om ) <-> ( aleph ` U. ( H " _om ) ) = ( aleph ` z ) ) ) |
55 |
52 54
|
mpbird |
|- ( ( z e. On /\ U. ( H " _om ) = ( aleph ` z ) ) -> ( aleph ` U. ( H " _om ) ) = U. ( H " _om ) ) |
56 |
55
|
rexlimiva |
|- ( E. z e. On U. ( H " _om ) = ( aleph ` z ) -> ( aleph ` U. ( H " _om ) ) = U. ( H " _om ) ) |
57 |
2 6 56
|
mp2b |
|- ( aleph ` U. ( H " _om ) ) = U. ( H " _om ) |