Metamath Proof Explorer

Theorem minregex2

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

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

Proof

Step Hyp Ref Expression
1 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 ) ) } )
2 eldifi 
 |-  ( A e. ( ran card \ _om ) -> A e. ran card )
3 iscard4 
 |-  ( ( card ` A ) = A <-> A e. ran card )
4 2 3 sylibr 
 |-  ( A e. ( ran card \ _om ) -> ( card ` A ) = A )
5 4 adantr 
 |-  ( ( A e. ( ran card \ _om ) /\ y e. On ) -> ( card ` A ) = A )
6 alephcard 
 |-  ( card ` ( aleph ` y ) ) = ( aleph ` y )
7 6 a1i 
 |-  ( ( A e. ( ran card \ _om ) /\ y e. On ) -> ( card ` ( aleph ` y ) ) = ( aleph ` y ) )
8 5 7 sseq12d 
 |-  ( ( A e. ( ran card \ _om ) /\ y e. On ) -> ( ( card ` A ) C_ ( card ` ( aleph ` y ) ) <-> A C_ ( aleph ` y ) ) )
9 numth3 
 |-  ( A e. ( ran card \ _om ) -> A e. dom card )
10 alephon 
 |-  ( aleph ` y ) e. On
11 onenon 
 |-  ( ( aleph ` y ) e. On -> ( aleph ` y ) e. dom card )
12 10 11 mp1i 
 |-  ( y e. On -> ( aleph ` y ) e. dom card )
13 carddom2 
 |-  ( ( A e. dom card /\ ( aleph ` y ) e. dom card ) -> ( ( card ` A ) C_ ( card ` ( aleph ` y ) ) <-> A ~<_ ( aleph ` y ) ) )
14 9 12 13 syl2an 
 |-  ( ( A e. ( ran card \ _om ) /\ y e. On ) -> ( ( card ` A ) C_ ( card ` ( aleph ` y ) ) <-> A ~<_ ( aleph ` y ) ) )
15 8 14 bitr3d 
 |-  ( ( A e. ( ran card \ _om ) /\ y e. On ) -> ( A C_ ( aleph ` y ) <-> A ~<_ ( aleph ` y ) ) )
16 15 3anbi2d 
 |-  ( ( A e. ( ran card \ _om ) /\ y e. On ) -> ( ( (/) e. y /\ A C_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) <-> ( (/) e. y /\ A ~<_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) ) )
17 16 rabbidva 
 |-  ( A e. ( ran card \ _om ) -> { y e. On | ( (/) e. y /\ A C_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) } = { y e. On | ( (/) e. y /\ A ~<_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) } )
18 17 inteqd 
 |-  ( A e. ( ran card \ _om ) -> |^| { y e. On | ( (/) e. y /\ A C_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) } = |^| { y e. On | ( (/) e. y /\ A ~<_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) } )
19 18 eqeq2d 
 |-  ( A e. ( ran card \ _om ) -> ( x = |^| { y e. On | ( (/) e. y /\ A C_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) } <-> x = |^| { y e. On | ( (/) e. y /\ A ~<_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) } ) )
20 19 rexbidv 
 |-  ( A e. ( ran card \ _om ) -> ( E. x e. On x = |^| { 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 ~<_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) } ) )
21 1 20 mpbid 
 |-  ( A e. ( ran card \ _om ) -> E. x e. On x = |^| { y e. On | ( (/) e. y /\ A ~<_ ( aleph ` y ) /\ ( cf ` ( aleph ` y ) ) = ( aleph ` y ) ) } )