Metamath Proof Explorer


Theorem alephfp

Description: The aleph function has a fixed point. Similar to Proposition 11.18 of TakeutiZaring p. 104, except that we construct an actual example of a fixed point rather than just showing its existence. See alephfp2 for an abbreviated version just showing existence. (Contributed by NM, 6-Nov-2004) (Proof shortened by Mario Carneiro, 15-May-2015)

Ref Expression
Hypothesis alephfplem.1
|- H = ( rec ( aleph , _om ) |` _om )
Assertion alephfp
|- ( aleph ` U. ( H " _om ) ) = U. ( H " _om )

Proof

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 )