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 ( 𝐴 ∈ ( ran card ∖ ω ) → ∃ 𝑥 ∈ On 𝑥 = ∩ { 𝑦 ∈ On ∣ ( ∅ ∈ 𝑦 ∧ 𝐴 ≼ ( ℵ ‘ 𝑦 ) ∧ ( cf ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) ) } )

Proof

Step Hyp Ref Expression
1 minregex ⊢ ( 𝐴 ∈ ( ran card ∖ ω ) → ∃ 𝑥 ∈ On 𝑥 = ∩ { 𝑦 ∈ On ∣ ( ∅ ∈ 𝑦 ∧ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) ∧ ( cf ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) ) } )
2 eldifi ⊢ ( 𝐴 ∈ ( ran card ∖ ω ) → 𝐴 ∈ ran card )
3 iscard4 ⊢ ( ( card ‘ 𝐴 ) = 𝐴 ↔ 𝐴 ∈ ran card )
4 2 3 sylibr ⊢ ( 𝐴 ∈ ( ran card ∖ ω ) → ( card ‘ 𝐴 ) = 𝐴 )
5 4 adantr ⊢ ( ( 𝐴 ∈ ( ran card ∖ ω ) ∧ 𝑦 ∈ On ) → ( card ‘ 𝐴 ) = 𝐴 )
6 alephcard ⊢ ( card ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 )
7 6 a1i ⊢ ( ( 𝐴 ∈ ( ran card ∖ ω ) ∧ 𝑦 ∈ On ) → ( card ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) )
8 5 7 sseq12d ⊢ ( ( 𝐴 ∈ ( ran card ∖ ω ) ∧ 𝑦 ∈ On ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ ( ℵ ‘ 𝑦 ) ) ↔ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) ) )
9 numth3 ⊢ ( 𝐴 ∈ ( ran card ∖ ω ) → 𝐴 ∈ dom card )
10 alephon ⊢ ( ℵ ‘ 𝑦 ) ∈ On
11 onenon ⊢ ( ( ℵ ‘ 𝑦 ) ∈ On → ( ℵ ‘ 𝑦 ) ∈ dom card )
12 10 11 mp1i ⊢ ( 𝑦 ∈ On → ( ℵ ‘ 𝑦 ) ∈ dom card )
13 carddom2 ⊢ ( ( 𝐴 ∈ dom card ∧ ( ℵ ‘ 𝑦 ) ∈ dom card ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ ( ℵ ‘ 𝑦 ) ) ↔ 𝐴 ≼ ( ℵ ‘ 𝑦 ) ) )
14 9 12 13 syl2an ⊢ ( ( 𝐴 ∈ ( ran card ∖ ω ) ∧ 𝑦 ∈ On ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ ( ℵ ‘ 𝑦 ) ) ↔ 𝐴 ≼ ( ℵ ‘ 𝑦 ) ) )
15 8 14 bitr3d ⊢ ( ( 𝐴 ∈ ( ran card ∖ ω ) ∧ 𝑦 ∈ On ) → ( 𝐴 ⊆ ( ℵ ‘ 𝑦 ) ↔ 𝐴 ≼ ( ℵ ‘ 𝑦 ) ) )
16 15 3anbi2d ⊢ ( ( 𝐴 ∈ ( ran card ∖ ω ) ∧ 𝑦 ∈ On ) → ( ( ∅ ∈ 𝑦 ∧ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) ∧ ( cf ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) ) ↔ ( ∅ ∈ 𝑦 ∧ 𝐴 ≼ ( ℵ ‘ 𝑦 ) ∧ ( cf ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) ) ) )
17 16 rabbidva ⊢ ( 𝐴 ∈ ( ran card ∖ ω ) → { 𝑦 ∈ On ∣ ( ∅ ∈ 𝑦 ∧ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) ∧ ( cf ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) ) } = { 𝑦 ∈ On ∣ ( ∅ ∈ 𝑦 ∧ 𝐴 ≼ ( ℵ ‘ 𝑦 ) ∧ ( cf ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) ) } )
18 17 inteqd ⊢ ( 𝐴 ∈ ( ran card ∖ ω ) → ∩ { 𝑦 ∈ On ∣ ( ∅ ∈ 𝑦 ∧ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) ∧ ( cf ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) ) } = ∩ { 𝑦 ∈ On ∣ ( ∅ ∈ 𝑦 ∧ 𝐴 ≼ ( ℵ ‘ 𝑦 ) ∧ ( cf ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) ) } )
19 18 eqeq2d ⊢ ( 𝐴 ∈ ( ran card ∖ ω ) → ( 𝑥 = ∩ { 𝑦 ∈ On ∣ ( ∅ ∈ 𝑦 ∧ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) ∧ ( cf ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) ) } ↔ 𝑥 = ∩ { 𝑦 ∈ On ∣ ( ∅ ∈ 𝑦 ∧ 𝐴 ≼ ( ℵ ‘ 𝑦 ) ∧ ( cf ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) ) } ) )
20 19 rexbidv ⊢ ( 𝐴 ∈ ( ran card ∖ ω ) → ( ∃ 𝑥 ∈ On 𝑥 = ∩ { 𝑦 ∈ On ∣ ( ∅ ∈ 𝑦 ∧ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) ∧ ( cf ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) ) } ↔ ∃ 𝑥 ∈ On 𝑥 = ∩ { 𝑦 ∈ On ∣ ( ∅ ∈ 𝑦 ∧ 𝐴 ≼ ( ℵ ‘ 𝑦 ) ∧ ( cf ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) ) } ) )
21 1 20 mpbid ⊢ ( 𝐴 ∈ ( ran card ∖ ω ) → ∃ 𝑥 ∈ On 𝑥 = ∩ { 𝑦 ∈ On ∣ ( ∅ ∈ 𝑦 ∧ 𝐴 ≼ ( ℵ ‘ 𝑦 ) ∧ ( cf ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) ) } )