Metamath Proof Explorer

Theorem minregex

Description: Given any cardinal number A , there exists an argument x , which yields the least regular uncountable value of aleph which is greater to or equal to A . This proof uses AC. (Contributed by RP, 23-Nov-2023)

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

Proof

Step Hyp Ref Expression
1 eldif 
 |-  ( A e. ( ran card \ _om ) <-> ( A e. ran card /\ -. A e. _om ) )
2 omelon 
 |-  _om e. On
3 cardon 
 |-  ( card ` A ) e. On
4 eleq1 
 |-  ( ( card ` A ) = A -> ( ( card ` A ) e. On <-> A e. On ) )
5 3 4 mpbii 
 |-  ( ( card ` A ) = A -> A e. On )
6 ontri1 
 |-  ( ( _om e. On /\ A e. On ) -> ( _om C_ A <-> -. A e. _om ) )
7 2 5 6 sylancr 
 |-  ( ( card ` A ) = A -> ( _om C_ A <-> -. A e. _om ) )
8 7 pm5.32i 
 |-  ( ( ( card ` A ) = A /\ _om C_ A ) <-> ( ( card ` A ) = A /\ -. A e. _om ) )
9 iscard4 
 |-  ( ( card ` A ) = A <-> A e. ran card )
10 9 anbi1i 
 |-  ( ( ( card ` A ) = A /\ -. A e. _om ) <-> ( A e. ran card /\ -. A e. _om ) )
11 8 10 bitr2i 
 |-  ( ( A e. ran card /\ -. A e. _om ) <-> ( ( card ` A ) = A /\ _om C_ A ) )
12 ancom 
 |-  ( ( ( card ` A ) = A /\ _om C_ A ) <-> ( _om C_ A /\ ( card ` A ) = A ) )
13 1 11 12 3bitri 
 |-  ( A e. ( ran card \ _om ) <-> ( _om C_ A /\ ( card ` A ) = A ) )
14 13 biimpi 
 |-  ( A e. ( ran card \ _om ) -> ( _om C_ A /\ ( card ` A ) = A ) )
15 cardalephex 
 |-  ( _om C_ A -> ( ( card ` A ) = A <-> E. x e. On A = ( aleph ` x ) ) )
16 15 biimpa 
 |-  ( ( _om C_ A /\ ( card ` A ) = A ) -> E. x e. On A = ( aleph ` x ) )
17 eqimss 
 |-  ( A = ( aleph ` x ) -> A C_ ( aleph ` x ) )
18 17 a1i 
 |-  ( ( _om C_ A /\ ( card ` A ) = A ) -> ( A = ( aleph ` x ) -> A C_ ( aleph ` x ) ) )
19 18 reximdv 
 |-  ( ( _om C_ A /\ ( card ` A ) = A ) -> ( E. x e. On A = ( aleph ` x ) -> E. x e. On A C_ ( aleph ` x ) ) )
20 16 19 mpd 
 |-  ( ( _om C_ A /\ ( card ` A ) = A ) -> E. x e. On A C_ ( aleph ` x ) )
21 onintrab2 
 |-  ( E. x e. On A C_ ( aleph ` x ) <-> |^| { x e. On | A C_ ( aleph ` x ) } e. On )
22 20 21 sylib 
 |-  ( ( _om C_ A /\ ( card ` A ) = A ) -> |^| { x e. On | A C_ ( aleph ` x ) } e. On )
23 simpr 
 |-  ( ( ( _om C_ A /\ ( card ` A ) = A ) /\ |^| { x e. On | A C_ ( aleph ` x ) } e. On ) -> |^| { x e. On | A C_ ( aleph ` x ) } e. On )
24 onsuc 
 |-  ( |^| { x e. On | A C_ ( aleph ` x ) } e. On -> suc |^| { x e. On | A C_ ( aleph ` x ) } e. On )
25 23 24 syl 
 |-  ( ( ( _om C_ A /\ ( card ` A ) = A ) /\ |^| { x e. On | A C_ ( aleph ` x ) } e. On ) -> suc |^| { x e. On | A C_ ( aleph ` x ) } e. On )
26 eloni 
 |-  ( |^| { x e. On | A C_ ( aleph ` x ) } e. On -> Ord |^| { x e. On | A C_ ( aleph ` x ) } )
27 23 26 syl 
 |-  ( ( ( _om C_ A /\ ( card ` A ) = A ) /\ |^| { x e. On | A C_ ( aleph ` x ) } e. On ) -> Ord |^| { x e. On | A C_ ( aleph ` x ) } )
28 0elsuc 
 |-  ( Ord |^| { x e. On | A C_ ( aleph ` x ) } -> (/) e. suc |^| { x e. On | A C_ ( aleph ` x ) } )
29 27 28 syl 
 |-  ( ( ( _om C_ A /\ ( card ` A ) = A ) /\ |^| { x e. On | A C_ ( aleph ` x ) } e. On ) -> (/) e. suc |^| { x e. On | A C_ ( aleph ` x ) } )
30 cardaleph 
 |-  ( ( _om C_ A /\ ( card ` A ) = A ) -> A = ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) )
31 30 adantr 
 |-  ( ( ( _om C_ A /\ ( card ` A ) = A ) /\ |^| { x e. On | A C_ ( aleph ` x ) } e. On ) -> A = ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) )
32 sssucid 
 |-  |^| { x e. On | A C_ ( aleph ` x ) } C_ suc |^| { x e. On | A C_ ( aleph ` x ) }
33 alephord3 
 |-  ( ( |^| { x e. On | A C_ ( aleph ` x ) } e. On /\ suc |^| { x e. On | A C_ ( aleph ` x ) } e. On ) -> ( |^| { x e. On | A C_ ( aleph ` x ) } C_ suc |^| { x e. On | A C_ ( aleph ` x ) } <-> ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) C_ ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
34 23 24 33 syl2anc2 
 |-  ( ( ( _om C_ A /\ ( card ` A ) = A ) /\ |^| { x e. On | A C_ ( aleph ` x ) } e. On ) -> ( |^| { x e. On | A C_ ( aleph ` x ) } C_ suc |^| { x e. On | A C_ ( aleph ` x ) } <-> ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) C_ ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
35 32 34 mpbii 
 |-  ( ( ( _om C_ A /\ ( card ` A ) = A ) /\ |^| { x e. On | A C_ ( aleph ` x ) } e. On ) -> ( aleph ` |^| { x e. On | A C_ ( aleph ` x ) } ) C_ ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) )
36 31 35 eqsstrd 
 |-  ( ( ( _om C_ A /\ ( card ` A ) = A ) /\ |^| { x e. On | A C_ ( aleph ` x ) } e. On ) -> A C_ ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) )
37 alephreg 
 |-  ( cf ` ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) = ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } )
38 37 a1i 
 |-  ( ( ( _om C_ A /\ ( card ` A ) = A ) /\ |^| { x e. On | A C_ ( aleph ` x ) } e. On ) -> ( cf ` ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) = ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) )
39 29 36 38 3jca 
 |-  ( ( ( _om C_ A /\ ( card ` A ) = A ) /\ |^| { x e. On | A C_ ( aleph ` x ) } e. On ) -> ( (/) e. suc |^| { x e. On | A C_ ( aleph ` x ) } /\ A C_ ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) /\ ( cf ` ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) = ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
40 25 39 jca 
 |-  ( ( ( _om C_ A /\ ( card ` A ) = A ) /\ |^| { x e. On | A C_ ( aleph ` x ) } e. On ) -> ( suc |^| { x e. On | A C_ ( aleph ` x ) } e. On /\ ( (/) e. suc |^| { x e. On | A C_ ( aleph ` x ) } /\ A C_ ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) /\ ( cf ` ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) = ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) ) )
41 14 22 40 syl2anc2 
 |-  ( A e. ( ran card \ _om ) -> ( suc |^| { x e. On | A C_ ( aleph ` x ) } e. On /\ ( (/) e. suc |^| { x e. On | A C_ ( aleph ` x ) } /\ A C_ ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) /\ ( cf ` ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) = ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) ) )
42 14 16 syl 
 |-  ( A e. ( ran card \ _om ) -> E. x e. On A = ( aleph ` x ) )
43 17 a1i 
 |-  ( A e. ( ran card \ _om ) -> ( A = ( aleph ` x ) -> A C_ ( aleph ` x ) ) )
44 43 reximdv 
 |-  ( A e. ( ran card \ _om ) -> ( E. x e. On A = ( aleph ` x ) -> E. x e. On A C_ ( aleph ` x ) ) )
45 42 44 mpd 
 |-  ( A e. ( ran card \ _om ) -> E. x e. On A C_ ( aleph ` x ) )
46 45 21 sylib 
 |-  ( A e. ( ran card \ _om ) -> |^| { x e. On | A C_ ( aleph ` x ) } e. On )
47 46 24 syl 
 |-  ( A e. ( ran card \ _om ) -> suc |^| { x e. On | A C_ ( aleph ` x ) } e. On )
48 sbcan 
 |-  ( [. suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]. ( y e. On /\ ( (/) e. y /\ A C_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) ) <-> ( [. suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]. y e. On /\ [. suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]. ( (/) e. y /\ A C_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) ) )
49 sbcel1v 
 |-  ( [. suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]. y e. On <-> suc |^| { x e. On | A C_ ( aleph ` x ) } e. On )
50 49 a1i 
 |-  ( suc |^| { x e. On | A C_ ( aleph ` x ) } e. On -> ( [. suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]. y e. On <-> suc |^| { x e. On | A C_ ( aleph ` x ) } e. On ) )
51 sbc3an 
 |-  ( [. suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]. ( (/) e. y /\ A C_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) <-> ( [. suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]. (/) e. y /\ [. suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]. A C_ ( aleph ` y ) /\ [. suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]. ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) )
52 sbcel2gv 
 |-  ( suc |^| { x e. On | A C_ ( aleph ` x ) } e. On -> ( [. suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]. (/) e. y <-> (/) e. suc |^| { x e. On | A C_ ( aleph ` x ) } ) )
53 sbcssg 
 |-  ( suc |^| { x e. On | A C_ ( aleph ` x ) } e. On -> ( [. suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]. A C_ ( aleph ` y ) <-> [_ suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]_ A C_ [_ suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]_ ( aleph ` y ) ) )
54 csbconstg 
 |-  ( suc |^| { x e. On | A C_ ( aleph ` x ) } e. On -> [_ suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]_ A = A )
55 csbfv2g 
 |-  ( suc |^| { x e. On | A C_ ( aleph ` x ) } e. On -> [_ suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]_ ( aleph ` y ) = ( aleph ` [_ suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]_ y ) )
56 csbvarg 
 |-  ( suc |^| { x e. On | A C_ ( aleph ` x ) } e. On -> [_ suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]_ y = suc |^| { x e. On | A C_ ( aleph ` x ) } )
57 56 fveq2d 
 |-  ( suc |^| { x e. On | A C_ ( aleph ` x ) } e. On -> ( aleph ` [_ suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]_ y ) = ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) )
58 55 57 eqtrd 
 |-  ( suc |^| { x e. On | A C_ ( aleph ` x ) } e. On -> [_ suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]_ ( aleph ` y ) = ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) )
59 54 58 sseq12d 
 |-  ( suc |^| { x e. On | A C_ ( aleph ` x ) } e. On -> ( [_ suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]_ A C_ [_ suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]_ ( aleph ` y ) <-> A C_ ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
60 53 59 bitrd 
 |-  ( suc |^| { x e. On | A C_ ( aleph ` x ) } e. On -> ( [. suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]. A C_ ( aleph ` y ) <-> A C_ ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
61 sbceqg 
 |-  ( suc |^| { x e. On | A C_ ( aleph ` x ) } e. On -> ( [. suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]. ( cf ` ( aleph ` y ) ) = ( aleph ` y ) <-> [_ suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]_ ( cf ` ( aleph ` y ) ) = [_ suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]_ ( aleph ` y ) ) )
62 csbfv2g 
 |-  ( suc |^| { x e. On | A C_ ( aleph ` x ) } e. On -> [_ suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]_ ( cf ` ( aleph ` y ) ) = ( cf ` [_ suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]_ ( aleph ` y ) ) )
63 58 fveq2d 
 |-  ( suc |^| { x e. On | A C_ ( aleph ` x ) } e. On -> ( cf ` [_ suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]_ ( aleph ` y ) ) = ( cf ` ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
64 62 63 eqtrd 
 |-  ( suc |^| { x e. On | A C_ ( aleph ` x ) } e. On -> [_ suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]_ ( cf ` ( aleph ` y ) ) = ( cf ` ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
65 64 58 eqeq12d 
 |-  ( suc |^| { x e. On | A C_ ( aleph ` x ) } e. On -> ( [_ suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]_ ( cf ` ( aleph ` y ) ) = [_ suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]_ ( aleph ` y ) <-> ( cf ` ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) = ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
66 61 65 bitrd 
 |-  ( suc |^| { x e. On | A C_ ( aleph ` x ) } e. On -> ( [. suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]. ( cf ` ( aleph ` y ) ) = ( aleph ` y ) <-> ( cf ` ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) = ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) )
67 52 60 66 3anbi123d 
 |-  ( suc |^| { x e. On | A C_ ( aleph ` x ) } e. On -> ( ( [. suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]. (/) e. y /\ [. suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]. A C_ ( aleph ` y ) /\ [. suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]. ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) <-> ( (/) e. suc |^| { x e. On | A C_ ( aleph ` x ) } /\ A C_ ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) /\ ( cf ` ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) = ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) ) )
68 51 67 bitrid 
 |-  ( suc |^| { x e. On | A C_ ( aleph ` x ) } e. On -> ( [. suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]. ( (/) e. y /\ A C_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) <-> ( (/) e. suc |^| { x e. On | A C_ ( aleph ` x ) } /\ A C_ ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) /\ ( cf ` ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) = ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) ) )
69 50 68 anbi12d 
 |-  ( suc |^| { x e. On | A C_ ( aleph ` x ) } e. On -> ( ( [. suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]. y e. On /\ [. suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]. ( (/) e. y /\ A C_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) ) <-> ( suc |^| { x e. On | A C_ ( aleph ` x ) } e. On /\ ( (/) e. suc |^| { x e. On | A C_ ( aleph ` x ) } /\ A C_ ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) /\ ( cf ` ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) = ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) ) ) )
70 48 69 bitrid 
 |-  ( suc |^| { x e. On | A C_ ( aleph ` x ) } e. On -> ( [. suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]. ( y e. On /\ ( (/) e. y /\ A C_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) ) <-> ( suc |^| { x e. On | A C_ ( aleph ` x ) } e. On /\ ( (/) e. suc |^| { x e. On | A C_ ( aleph ` x ) } /\ A C_ ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) /\ ( cf ` ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) = ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) ) ) )
71 47 70 syl 
 |-  ( A e. ( ran card \ _om ) -> ( [. suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]. ( y e. On /\ ( (/) e. y /\ A C_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) ) <-> ( suc |^| { x e. On | A C_ ( aleph ` x ) } e. On /\ ( (/) e. suc |^| { x e. On | A C_ ( aleph ` x ) } /\ A C_ ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) /\ ( cf ` ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) = ( aleph ` suc |^| { x e. On | A C_ ( aleph ` x ) } ) ) ) ) )
72 41 71 mpbird 
 |-  ( A e. ( ran card \ _om ) -> [. suc |^| { x e. On | A C_ ( aleph ` x ) } / y ]. ( y e. On /\ ( (/) e. y /\ A C_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) ) )
73 72 spesbcd 
 |-  ( A e. ( ran card \ _om ) -> E. y ( y e. On /\ ( (/) e. y /\ A C_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) ) )
74 onintrab2 
 |-  ( E. y e. On ( (/) e. y /\ A C_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) <-> |^| { y e. On | ( (/) e. y /\ A C_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) } e. On )
75 df-rex 
 |-  ( E. y e. On ( (/) e. y /\ A C_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) <-> E. y ( y e. On /\ ( (/) e. y /\ A C_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) ) )
76 risset 
 |-  ( |^| { y e. On | ( (/) e. y /\ A C_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) } e. On <-> E. x e. On x = |^| { y e. On | ( (/) e. y /\ A C_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) } )
77 74 75 76 3bitr3i 
 |-  ( E. y ( y e. On /\ ( (/) e. y /\ A C_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) ) <-> E. x e. On x = |^| { y e. On | ( (/) e. y /\ A C_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) } )
78 73 77 sylib 
 |-  ( A e. ( ran card \ _om ) -> E. x e. On x = |^| { y e. On | ( (/) e. y /\ A C_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) } )