Metamath Proof Explorer

Theorem cardaleph

Description: Given any transfinite cardinal number A , there is exactly one aleph that is equal to it. Here we compute that alephexplicitly. (Contributed by NM, 9-Nov-2003) (Revised by Mario Carneiro, 2-Feb-2013)

Ref Expression
Assertion cardaleph 
|- ( ( _om C_ A /\ ( card ` A ) = A ) -> A = ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) )

Proof

Step Hyp Ref Expression
1 cardon 
 |-  ( card ` A ) e. On
2 eleq1 
 |-  ( ( card ` A ) = A -> ( ( card ` A ) e. On <-> A e. On ) )
3 1 2 mpbii 
 |-  ( ( card ` A ) = A -> A e. On )
4 alephle 
 |-  ( A e. On -> A C_ ( aleph ` A ) )
5 fveq2 
 |-  ( x = A -> ( aleph ` x ) = ( aleph ` A ) )
6 5 sseq2d 
 |-  ( x = A -> ( A C_ ( aleph ` x ) <-> A C_ ( aleph ` A ) ) )
7 6 rspcev 
 |-  ( ( A e. On /\ A C_ ( aleph ` A ) ) -> E. x e. On A C_ ( aleph ` x ) )
8 4 7 mpdan 
 |-  ( A e. On -> E. x e. On A C_ ( aleph ` x ) )
9 nfcv 
 |-  F/_ x A
10 nfcv 
 |-  F/_ x aleph
11 nfrab1 
 |-  F/_ x { x e. On | A C_ ( aleph ` x ) }
12 11 nfint 
 |-  F/_ x |^| { x e. On | A C_ ( aleph ` x ) }
13 10 12 nffv 
 |-  F/_ x ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } )
14 9 13 nfss 
 |-  F/ x A C_ ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } )
15 fveq2 
 |-  ( x = |^| { x e. On | A C_ ( aleph ` x ) } -> ( aleph ` x ) = ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) )
16 15 sseq2d 
 |-  ( x = |^| { x e. On | A C_ ( aleph ` x ) } -> ( A C_ ( aleph ` x ) <-> A C_ ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
17 14 16 onminsb 
 |-  ( E. x e. On A C_ ( aleph ` x ) -> A C_ ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) )
18 3 8 17 3syl 
 |-  ( ( card ` A ) = A -> A C_ ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) )
19 18 a1i 
 |-  ( |^| { x e. On | A C_ ( aleph ` x ) } = (/) -> ( ( card ` A ) = A -> A C_ ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
20 fveq2 
 |-  ( |^| { x e. On | A C_ ( aleph ` x ) } = (/) -> ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) = ( aleph ` (/) ) )
21 aleph0 
 |-  ( aleph ` (/) ) = _om
22 20 21 eqtrdi 
 |-  ( |^| { x e. On | A C_ ( aleph ` x ) } = (/) -> ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) = _om )
23 22 sseq1d 
 |-  ( |^| { x e. On | A C_ ( aleph ` x ) } = (/) -> ( ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) C_ A <-> _om C_ A ) )
24 23 biimprd 
 |-  ( |^| { x e. On | A C_ ( aleph ` x ) } = (/) -> ( _om C_ A -> ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) C_ A ) )
25 19 24 anim12d 
 |-  ( |^| { x e. On | A C_ ( aleph ` x ) } = (/) -> ( ( ( card ` A ) = A /\ _om C_ A ) -> ( A C_ ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) /\ ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) C_ A ) ) )
26 eqss 
 |-  ( A = ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) <-> ( A C_ ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) /\ ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) C_ A ) )
27 25 26 syl6ibr 
 |-  ( |^| { x e. On | A C_ ( aleph ` x ) } = (/) -> ( ( ( card ` A ) = A /\ _om C_ A ) -> A = ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
28 27 com12 
 |-  ( ( ( card ` A ) = A /\ _om C_ A ) -> ( |^| { x e. On | A C_ ( aleph ` x ) } = (/) -> A = ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
29 28 ancoms 
 |-  ( ( _om C_ A /\ ( card ` A ) = A ) -> ( |^| { x e. On | A C_ ( aleph ` x ) } = (/) -> A = ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
30 fveq2 
 |-  ( x = y -> ( aleph ` x ) = ( aleph ` y ) )
31 30 sseq2d 
 |-  ( x = y -> ( A C_ ( aleph ` x ) <-> A C_ ( aleph ` y ) ) )
32 31 onnminsb 
 |-  ( y e. On -> ( y e. |^| { x e. On | A C_ ( aleph ` x ) } -> -. A C_ ( aleph ` y ) ) )
33 vex 
 |-  y e. _V
34 33 sucid 
 |-  y e. suc y
35 eleq2 
 |-  ( |^| { x e. On | A C_ ( aleph ` x ) } = suc y -> ( y e. |^| { x e. On | A C_ ( aleph ` x ) } <-> y e. suc y ) )
36 34 35 mpbiri 
 |-  ( |^| { x e. On | A C_ ( aleph ` x ) } = suc y -> y e. |^| { x e. On | A C_ ( aleph ` x ) } )
37 32 36 impel 
 |-  ( ( y e. On /\ |^| { x e. On | A C_ ( aleph ` x ) } = suc y ) -> -. A C_ ( aleph ` y ) )
38 37 adantl 
 |-  ( ( ( card ` A ) = A /\ ( y e. On /\ |^| { x e. On | A C_ ( aleph ` x ) } = suc y ) ) -> -. A C_ ( aleph ` y ) )
39 fveq2 
 |-  ( |^| { x e. On | A C_ ( aleph ` x ) } = suc y -> ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) = ( aleph ` suc y ) )
40 alephsuc 
 |-  ( y e. On -> ( aleph ` suc y ) = ( har ` ( aleph ` y ) ) )
41 39 40 sylan9eqr 
 |-  ( ( y e. On /\ |^| { x e. On | A C_ ( aleph ` x ) } = suc y ) -> ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) = ( har ` ( aleph ` y ) ) )
42 41 eleq2d 
 |-  ( ( y e. On /\ |^| { x e. On | A C_ ( aleph ` x ) } = suc y ) -> ( A e. ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) <-> A e. ( har ` ( aleph ` y ) ) ) )
43 42 biimpd 
 |-  ( ( y e. On /\ |^| { x e. On | A C_ ( aleph ` x ) } = suc y ) -> ( A e. ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) -> A e. ( har ` ( aleph ` y ) ) ) )
44 elharval 
 |-  ( A e. ( har ` ( aleph ` y ) ) <-> ( A e. On /\ A ~<_ ( aleph ` y ) ) )
45 44 simprbi 
 |-  ( A e. ( har ` ( aleph ` y ) ) -> A ~<_ ( aleph ` y ) )
46 onenon 
 |-  ( A e. On -> A e. dom card )
47 3 46 syl 
 |-  ( ( card ` A ) = A -> A e. dom card )
48 alephon 
 |-  ( aleph ` y ) e. On
49 onenon 
 |-  ( ( aleph ` y ) e. On -> ( aleph ` y ) e. dom card )
50 48 49 ax-mp 
 |-  ( aleph ` y ) e. dom card
51 carddom2 
 |-  ( ( A e. dom card /\ ( aleph ` y ) e. dom card ) -> ( ( card ` A ) C_ ( card ` ( aleph ` y ) ) <-> A ~<_ ( aleph ` y ) ) )
52 47 50 51 sylancl 
 |-  ( ( card ` A ) = A -> ( ( card ` A ) C_ ( card ` ( aleph ` y ) ) <-> A ~<_ ( aleph ` y ) ) )
53 sseq1 
 |-  ( ( card ` A ) = A -> ( ( card ` A ) C_ ( card ` ( aleph ` y ) ) <-> A C_ ( card ` ( aleph ` y ) ) ) )
54 alephcard 
 |-  ( card ` ( aleph ` y ) ) = ( aleph ` y )
55 54 sseq2i 
 |-  ( A C_ ( card ` ( aleph ` y ) ) <-> A C_ ( aleph ` y ) )
56 53 55 bitrdi 
 |-  ( ( card ` A ) = A -> ( ( card ` A ) C_ ( card ` ( aleph ` y ) ) <-> A C_ ( aleph ` y ) ) )
57 52 56 bitr3d 
 |-  ( ( card ` A ) = A -> ( A ~<_ ( aleph ` y ) <-> A C_ ( aleph ` y ) ) )
58 45 57 syl5ib 
 |-  ( ( card ` A ) = A -> ( A e. ( har ` ( aleph ` y ) ) -> A C_ ( aleph ` y ) ) )
59 43 58 sylan9r 
 |-  ( ( ( card ` A ) = A /\ ( y e. On /\ |^| { x e. On | A C_ ( aleph ` x ) } = suc y ) ) -> ( A e. ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) -> A C_ ( aleph ` y ) ) )
60 38 59 mtod 
 |-  ( ( ( card ` A ) = A /\ ( y e. On /\ |^| { x e. On | A C_ ( aleph ` x ) } = suc y ) ) -> -. A e. ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) )
61 60 rexlimdvaa 
 |-  ( ( card ` A ) = A -> ( E. y e. On |^| { x e. On | A C_ ( aleph ` x ) } = suc y -> -. A e. ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
62 onintrab2 
 |-  ( E. x e. On A C_ ( aleph ` x ) <-> |^| { x e. On | A C_ ( aleph ` x ) } e. On )
63 8 62 sylib 
 |-  ( A e. On -> |^| { x e. On | A C_ ( aleph ` x ) } e. On )
64 onelon 
 |-  ( ( |^| { x e. On | A C_ ( aleph ` x ) } e. On /\ y e. |^| { x e. On | A C_ ( aleph ` x ) } ) -> y e. On )
65 63 64 sylan 
 |-  ( ( A e. On /\ y e. |^| { x e. On | A C_ ( aleph ` x ) } ) -> y e. On )
66 32 adantld 
 |-  ( y e. On -> ( ( A e. On /\ y e. |^| { x e. On | A C_ ( aleph ` x ) } ) -> -. A C_ ( aleph ` y ) ) )
67 65 66 mpcom 
 |-  ( ( A e. On /\ y e. |^| { x e. On | A C_ ( aleph ` x ) } ) -> -. A C_ ( aleph ` y ) )
68 48 onelssi 
 |-  ( A e. ( aleph ` y ) -> A C_ ( aleph ` y ) )
69 67 68 nsyl 
 |-  ( ( A e. On /\ y e. |^| { x e. On | A C_ ( aleph ` x ) } ) -> -. A e. ( aleph ` y ) )
70 69 nrexdv 
 |-  ( A e. On -> -. E. y e. |^| { x e. On | A C_ ( aleph ` x ) } A e. ( aleph ` y ) )
71 70 adantr 
 |-  ( ( A e. On /\ Lim |^| { x e. On | A C_ ( aleph ` x ) } ) -> -. E. y e. |^| { x e. On | A C_ ( aleph ` x ) } A e. ( aleph ` y ) )
72 alephlim 
 |-  ( ( |^| { x e. On | A C_ ( aleph ` x ) } e. On /\ Lim |^| { x e. On | A C_ ( aleph ` x ) } ) -> ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) = U_ y e. |^| { x e. On | A C_ ( aleph ` x ) } ( aleph ` y ) )
73 63 72 sylan 
 |-  ( ( A e. On /\ Lim |^| { x e. On | A C_ ( aleph ` x ) } ) -> ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) = U_ y e. |^| { x e. On | A C_ ( aleph ` x ) } ( aleph ` y ) )
74 73 eleq2d 
 |-  ( ( A e. On /\ Lim |^| { x e. On | A C_ ( aleph ` x ) } ) -> ( A e. ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) <-> A e. U_ y e. |^| { x e. On | A C_ ( aleph ` x ) } ( aleph ` y ) ) )
75 eliun 
 |-  ( A e. U_ y e. |^| { x e. On | A C_ ( aleph ` x ) } ( aleph ` y ) <-> E. y e. |^| { x e. On | A C_ ( aleph ` x ) } A e. ( aleph ` y ) )
76 74 75 bitrdi 
 |-  ( ( A e. On /\ Lim |^| { x e. On | A C_ ( aleph ` x ) } ) -> ( A e. ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) <-> E. y e. |^| { x e. On | A C_ ( aleph ` x ) } A e. ( aleph ` y ) ) )
77 71 76 mtbird 
 |-  ( ( A e. On /\ Lim |^| { x e. On | A C_ ( aleph ` x ) } ) -> -. A e. ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) )
78 77 ex 
 |-  ( A e. On -> ( Lim |^| { x e. On | A C_ ( aleph ` x ) } -> -. A e. ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
79 3 78 syl 
 |-  ( ( card ` A ) = A -> ( Lim |^| { x e. On | A C_ ( aleph ` x ) } -> -. A e. ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
80 61 79 jaod 
 |-  ( ( card ` A ) = A -> ( ( E. y e. On |^| { x e. On | A C_ ( aleph ` x ) } = suc y \/ Lim |^| { x e. On | A C_ ( aleph ` x ) } ) -> -. A e. ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
81 8 17 syl 
 |-  ( A e. On -> A C_ ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) )
82 alephon 
 |-  ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) e. On
83 onsseleq 
 |-  ( ( A e. On /\ ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) e. On ) -> ( A C_ ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) <-> ( A e. ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) \/ A = ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) ) ) )
84 82 83 mpan2 
 |-  ( A e. On -> ( A C_ ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) <-> ( A e. ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) \/ A = ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) ) ) )
85 81 84 mpbid 
 |-  ( A e. On -> ( A e. ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) \/ A = ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
86 85 ord 
 |-  ( A e. On -> ( -. A e. ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) -> A = ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
87 3 80 86 sylsyld 
 |-  ( ( card ` A ) = A -> ( ( E. y e. On |^| { x e. On | A C_ ( aleph ` x ) } = suc y \/ Lim |^| { x e. On | A C_ ( aleph ` x ) } ) -> A = ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
88 87 adantl 
 |-  ( ( _om C_ A /\ ( card ` A ) = A ) -> ( ( E. y e. On |^| { x e. On | A C_ ( aleph ` x ) } = suc y \/ Lim |^| { x e. On | A C_ ( aleph ` x ) } ) -> A = ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
89 eloni 
 |-  ( |^| { x e. On | A C_ ( aleph ` x ) } e. On -> Ord |^| { x e. On | A C_ ( aleph ` x ) } )
90 ordzsl 
 |-  ( Ord |^| { x e. On | A C_ ( aleph ` x ) } <-> ( |^| { x e. On | A C_ ( aleph ` x ) } = (/) \/ E. y e. On |^| { x e. On | A C_ ( aleph ` x ) } = suc y \/ Lim |^| { x e. On | A C_ ( aleph ` x ) } ) )
91 3orass 
 |-  ( ( |^| { x e. On | A C_ ( aleph ` x ) } = (/) \/ E. y e. On |^| { x e. On | A C_ ( aleph ` x ) } = suc y \/ Lim |^| { x e. On | A C_ ( aleph ` x ) } ) <-> ( |^| { x e. On | A C_ ( aleph ` x ) } = (/) \/ ( E. y e. On |^| { x e. On | A C_ ( aleph ` x ) } = suc y \/ Lim |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
92 90 91 bitri 
 |-  ( Ord |^| { x e. On | A C_ ( aleph ` x ) } <-> ( |^| { x e. On | A C_ ( aleph ` x ) } = (/) \/ ( E. y e. On |^| { x e. On | A C_ ( aleph ` x ) } = suc y \/ Lim |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
93 89 92 sylib 
 |-  ( |^| { x e. On | A C_ ( aleph ` x ) } e. On -> ( |^| { x e. On | A C_ ( aleph ` x ) } = (/) \/ ( E. y e. On |^| { x e. On | A C_ ( aleph ` x ) } = suc y \/ Lim |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
94 3 63 93 3syl 
 |-  ( ( card ` A ) = A -> ( |^| { x e. On | A C_ ( aleph ` x ) } = (/) \/ ( E. y e. On |^| { x e. On | A C_ ( aleph ` x ) } = suc y \/ Lim |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
95 94 adantl 
 |-  ( ( _om C_ A /\ ( card ` A ) = A ) -> ( |^| { x e. On | A C_ ( aleph ` x ) } = (/) \/ ( E. y e. On |^| { x e. On | A C_ ( aleph ` x ) } = suc y \/ Lim |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
96 29 88 95 mpjaod 
 |-  ( ( _om C_ A /\ ( card ` A ) = A ) -> A = ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) )