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