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

Proof

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