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

Proof

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