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∈ran⁡card∖ω→∃x∈Onx=⋂y∈On|∅∈y∧A≼ℵ⁡y∧cf⁡ℵ⁡y=ℵ⁡y

Proof

Step Hyp Ref Expression
1 minregex ⊢A∈ran⁡card∖ω→∃x∈Onx=⋂y∈On|∅∈y∧A⊆ℵ⁡y∧cf⁡ℵ⁡y=ℵ⁡y
2 eldifi ⊢A∈ran⁡card∖ω→A∈ran⁡card
3 iscard4 ⊢card⁡A=A↔A∈ran⁡card
4 2 3 sylibr ⊢A∈ran⁡card∖ω→card⁡A=A
5 4 adantr ⊢A∈ran⁡card∖ω∧y∈On→card⁡A=A
6 alephcard ⊢card⁡ℵ⁡y=ℵ⁡y
7 6 a1i ⊢A∈ran⁡card∖ω∧y∈On→card⁡ℵ⁡y=ℵ⁡y
8 5 7 sseq12d ⊢A∈ran⁡card∖ω∧y∈On→card⁡A⊆card⁡ℵ⁡y↔A⊆ℵ⁡y
9 numth3 ⊢A∈ran⁡card∖ω→A∈dom⁡card
10 alephon ⊢ℵ⁡y∈On
11 onenon ⊢ℵ⁡y∈On→ℵ⁡y∈dom⁡card
12 10 11 mp1i ⊢y∈On→ℵ⁡y∈dom⁡card
13 carddom2 ⊢A∈dom⁡card∧ℵ⁡y∈dom⁡card→card⁡A⊆card⁡ℵ⁡y↔A≼ℵ⁡y
14 9 12 13 syl2an ⊢A∈ran⁡card∖ω∧y∈On→card⁡A⊆card⁡ℵ⁡y↔A≼ℵ⁡y
15 8 14 bitr3d ⊢A∈ran⁡card∖ω∧y∈On→A⊆ℵ⁡y↔A≼ℵ⁡y
16 15 3anbi2d ⊢A∈ran⁡card∖ω∧y∈On→∅∈y∧A⊆ℵ⁡y∧cf⁡ℵ⁡y=ℵ⁡y↔∅∈y∧A≼ℵ⁡y∧cf⁡ℵ⁡y=ℵ⁡y
17 16 rabbidva ⊢A∈ran⁡card∖ω→y∈On|∅∈y∧A⊆ℵ⁡y∧cf⁡ℵ⁡y=ℵ⁡y=y∈On|∅∈y∧A≼ℵ⁡y∧cf⁡ℵ⁡y=ℵ⁡y
18 17 inteqd ⊢A∈ran⁡card∖ω→⋂y∈On|∅∈y∧A⊆ℵ⁡y∧cf⁡ℵ⁡y=ℵ⁡y=⋂y∈On|∅∈y∧A≼ℵ⁡y∧cf⁡ℵ⁡y=ℵ⁡y
19 18 eqeq2d ⊢A∈ran⁡card∖ω→x=⋂y∈On|∅∈y∧A⊆ℵ⁡y∧cf⁡ℵ⁡y=ℵ⁡y↔x=⋂y∈On|∅∈y∧A≼ℵ⁡y∧cf⁡ℵ⁡y=ℵ⁡y
20 19 rexbidv ⊢A∈ran⁡card∖ω→∃x∈Onx=⋂y∈On|∅∈y∧A⊆ℵ⁡y∧cf⁡ℵ⁡y=ℵ⁡y↔∃x∈Onx=⋂y∈On|∅∈y∧A≼ℵ⁡y∧cf⁡ℵ⁡y=ℵ⁡y
21 1 20 mpbid ⊢A∈ran⁡card∖ω→∃x∈Onx=⋂y∈On|∅∈y∧A≼ℵ⁡y∧cf⁡ℵ⁡y=ℵ⁡y