Metamath Proof Explorer


Theorem cardaleph

Description: Given any transfinite cardinal number A , there is exactly one aleph that is equal to it. Here we compute that alephexplicitly. (Contributed by NM, 9-Nov-2003) (Revised by Mario Carneiro, 2-Feb-2013)

Ref Expression
Assertion cardaleph ( ( ω ⊆ 𝐴 ∧ ( card ‘ 𝐴 ) = 𝐴 ) → 𝐴 = ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) )

Proof

Step Hyp Ref Expression
1 cardon ( card ‘ 𝐴 ) ∈ On
2 eleq1 ( ( card ‘ 𝐴 ) = 𝐴 → ( ( card ‘ 𝐴 ) ∈ On ↔ 𝐴 ∈ On ) )
3 1 2 mpbii ( ( card ‘ 𝐴 ) = 𝐴𝐴 ∈ On )
4 alephle ( 𝐴 ∈ On → 𝐴 ⊆ ( ℵ ‘ 𝐴 ) )
5 fveq2 ( 𝑥 = 𝐴 → ( ℵ ‘ 𝑥 ) = ( ℵ ‘ 𝐴 ) )
6 5 sseq2d ( 𝑥 = 𝐴 → ( 𝐴 ⊆ ( ℵ ‘ 𝑥 ) ↔ 𝐴 ⊆ ( ℵ ‘ 𝐴 ) ) )
7 6 rspcev ( ( 𝐴 ∈ On ∧ 𝐴 ⊆ ( ℵ ‘ 𝐴 ) ) → ∃ 𝑥 ∈ On 𝐴 ⊆ ( ℵ ‘ 𝑥 ) )
8 4 7 mpdan ( 𝐴 ∈ On → ∃ 𝑥 ∈ On 𝐴 ⊆ ( ℵ ‘ 𝑥 ) )
9 nfcv 𝑥 𝐴
10 nfcv 𝑥
11 nfrab1 𝑥 { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) }
12 11 nfint 𝑥 { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) }
13 10 12 nffv 𝑥 ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } )
14 9 13 nfss 𝑥 𝐴 ⊆ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } )
15 fveq2 ( 𝑥 = { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } → ( ℵ ‘ 𝑥 ) = ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) )
16 15 sseq2d ( 𝑥 = { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } → ( 𝐴 ⊆ ( ℵ ‘ 𝑥 ) ↔ 𝐴 ⊆ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ) )
17 14 16 onminsb ( ∃ 𝑥 ∈ On 𝐴 ⊆ ( ℵ ‘ 𝑥 ) → 𝐴 ⊆ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) )
18 3 8 17 3syl ( ( card ‘ 𝐴 ) = 𝐴𝐴 ⊆ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) )
19 18 a1i ( { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = ∅ → ( ( card ‘ 𝐴 ) = 𝐴𝐴 ⊆ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ) )
20 fveq2 ( { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = ∅ → ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) = ( ℵ ‘ ∅ ) )
21 aleph0 ( ℵ ‘ ∅ ) = ω
22 20 21 eqtrdi ( { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = ∅ → ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) = ω )
23 22 sseq1d ( { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = ∅ → ( ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ⊆ 𝐴 ↔ ω ⊆ 𝐴 ) )
24 23 biimprd ( { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = ∅ → ( ω ⊆ 𝐴 → ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ⊆ 𝐴 ) )
25 19 24 anim12d ( { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = ∅ → ( ( ( card ‘ 𝐴 ) = 𝐴 ∧ ω ⊆ 𝐴 ) → ( 𝐴 ⊆ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ∧ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ⊆ 𝐴 ) ) )
26 eqss ( 𝐴 = ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ↔ ( 𝐴 ⊆ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ∧ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ⊆ 𝐴 ) )
27 25 26 syl6ibr ( { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = ∅ → ( ( ( card ‘ 𝐴 ) = 𝐴 ∧ ω ⊆ 𝐴 ) → 𝐴 = ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ) )
28 27 com12 ( ( ( card ‘ 𝐴 ) = 𝐴 ∧ ω ⊆ 𝐴 ) → ( { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = ∅ → 𝐴 = ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ) )
29 28 ancoms ( ( ω ⊆ 𝐴 ∧ ( card ‘ 𝐴 ) = 𝐴 ) → ( { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = ∅ → 𝐴 = ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ) )
30 fveq2 ( 𝑥 = 𝑦 → ( ℵ ‘ 𝑥 ) = ( ℵ ‘ 𝑦 ) )
31 30 sseq2d ( 𝑥 = 𝑦 → ( 𝐴 ⊆ ( ℵ ‘ 𝑥 ) ↔ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) ) )
32 31 onnminsb ( 𝑦 ∈ On → ( 𝑦 { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } → ¬ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) ) )
33 vex 𝑦 ∈ V
34 33 sucid 𝑦 ∈ suc 𝑦
35 eleq2 ( { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = suc 𝑦 → ( 𝑦 { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ↔ 𝑦 ∈ suc 𝑦 ) )
36 34 35 mpbiri ( { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = suc 𝑦𝑦 { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } )
37 32 36 impel ( ( 𝑦 ∈ On ∧ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = suc 𝑦 ) → ¬ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) )
38 37 adantl ( ( ( card ‘ 𝐴 ) = 𝐴 ∧ ( 𝑦 ∈ On ∧ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = suc 𝑦 ) ) → ¬ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) )
39 fveq2 ( { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = suc 𝑦 → ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) = ( ℵ ‘ suc 𝑦 ) )
40 alephsuc ( 𝑦 ∈ On → ( ℵ ‘ suc 𝑦 ) = ( har ‘ ( ℵ ‘ 𝑦 ) ) )
41 39 40 sylan9eqr ( ( 𝑦 ∈ On ∧ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = suc 𝑦 ) → ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) = ( har ‘ ( ℵ ‘ 𝑦 ) ) )
42 41 eleq2d ( ( 𝑦 ∈ On ∧ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = suc 𝑦 ) → ( 𝐴 ∈ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ↔ 𝐴 ∈ ( har ‘ ( ℵ ‘ 𝑦 ) ) ) )
43 42 biimpd ( ( 𝑦 ∈ On ∧ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = suc 𝑦 ) → ( 𝐴 ∈ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) → 𝐴 ∈ ( har ‘ ( ℵ ‘ 𝑦 ) ) ) )
44 elharval ( 𝐴 ∈ ( har ‘ ( ℵ ‘ 𝑦 ) ) ↔ ( 𝐴 ∈ On ∧ 𝐴 ≼ ( ℵ ‘ 𝑦 ) ) )
45 44 simprbi ( 𝐴 ∈ ( har ‘ ( ℵ ‘ 𝑦 ) ) → 𝐴 ≼ ( ℵ ‘ 𝑦 ) )
46 onenon ( 𝐴 ∈ On → 𝐴 ∈ dom card )
47 3 46 syl ( ( card ‘ 𝐴 ) = 𝐴𝐴 ∈ dom card )
48 alephon ( ℵ ‘ 𝑦 ) ∈ On
49 onenon ( ( ℵ ‘ 𝑦 ) ∈ On → ( ℵ ‘ 𝑦 ) ∈ dom card )
50 48 49 ax-mp ( ℵ ‘ 𝑦 ) ∈ dom card
51 carddom2 ( ( 𝐴 ∈ dom card ∧ ( ℵ ‘ 𝑦 ) ∈ dom card ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ ( ℵ ‘ 𝑦 ) ) ↔ 𝐴 ≼ ( ℵ ‘ 𝑦 ) ) )
52 47 50 51 sylancl ( ( card ‘ 𝐴 ) = 𝐴 → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ ( ℵ ‘ 𝑦 ) ) ↔ 𝐴 ≼ ( ℵ ‘ 𝑦 ) ) )
53 sseq1 ( ( card ‘ 𝐴 ) = 𝐴 → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ ( ℵ ‘ 𝑦 ) ) ↔ 𝐴 ⊆ ( card ‘ ( ℵ ‘ 𝑦 ) ) ) )
54 alephcard ( card ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 )
55 54 sseq2i ( 𝐴 ⊆ ( card ‘ ( ℵ ‘ 𝑦 ) ) ↔ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) )
56 53 55 bitrdi ( ( card ‘ 𝐴 ) = 𝐴 → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ ( ℵ ‘ 𝑦 ) ) ↔ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) ) )
57 52 56 bitr3d ( ( card ‘ 𝐴 ) = 𝐴 → ( 𝐴 ≼ ( ℵ ‘ 𝑦 ) ↔ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) ) )
58 45 57 syl5ib ( ( card ‘ 𝐴 ) = 𝐴 → ( 𝐴 ∈ ( har ‘ ( ℵ ‘ 𝑦 ) ) → 𝐴 ⊆ ( ℵ ‘ 𝑦 ) ) )
59 43 58 sylan9r ( ( ( card ‘ 𝐴 ) = 𝐴 ∧ ( 𝑦 ∈ On ∧ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = suc 𝑦 ) ) → ( 𝐴 ∈ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) → 𝐴 ⊆ ( ℵ ‘ 𝑦 ) ) )
60 38 59 mtod ( ( ( card ‘ 𝐴 ) = 𝐴 ∧ ( 𝑦 ∈ On ∧ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = suc 𝑦 ) ) → ¬ 𝐴 ∈ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) )
61 60 rexlimdvaa ( ( card ‘ 𝐴 ) = 𝐴 → ( ∃ 𝑦 ∈ On { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = suc 𝑦 → ¬ 𝐴 ∈ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ) )
62 onintrab2 ( ∃ 𝑥 ∈ On 𝐴 ⊆ ( ℵ ‘ 𝑥 ) ↔ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ∈ On )
63 8 62 sylib ( 𝐴 ∈ On → { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ∈ On )
64 onelon ( ( { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ∈ On ∧ 𝑦 { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) → 𝑦 ∈ On )
65 63 64 sylan ( ( 𝐴 ∈ On ∧ 𝑦 { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) → 𝑦 ∈ On )
66 32 adantld ( 𝑦 ∈ On → ( ( 𝐴 ∈ On ∧ 𝑦 { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) → ¬ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) ) )
67 65 66 mpcom ( ( 𝐴 ∈ On ∧ 𝑦 { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) → ¬ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) )
68 48 onelssi ( 𝐴 ∈ ( ℵ ‘ 𝑦 ) → 𝐴 ⊆ ( ℵ ‘ 𝑦 ) )
69 67 68 nsyl ( ( 𝐴 ∈ On ∧ 𝑦 { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) → ¬ 𝐴 ∈ ( ℵ ‘ 𝑦 ) )
70 69 nrexdv ( 𝐴 ∈ On → ¬ ∃ 𝑦 { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } 𝐴 ∈ ( ℵ ‘ 𝑦 ) )
71 70 adantr ( ( 𝐴 ∈ On ∧ Lim { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) → ¬ ∃ 𝑦 { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } 𝐴 ∈ ( ℵ ‘ 𝑦 ) )
72 alephlim ( ( { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ∈ On ∧ Lim { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) → ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) = 𝑦 { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ( ℵ ‘ 𝑦 ) )
73 63 72 sylan ( ( 𝐴 ∈ On ∧ Lim { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) → ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) = 𝑦 { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ( ℵ ‘ 𝑦 ) )
74 73 eleq2d ( ( 𝐴 ∈ On ∧ Lim { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) → ( 𝐴 ∈ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ↔ 𝐴 𝑦 { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ( ℵ ‘ 𝑦 ) ) )
75 eliun ( 𝐴 𝑦 { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ( ℵ ‘ 𝑦 ) ↔ ∃ 𝑦 { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } 𝐴 ∈ ( ℵ ‘ 𝑦 ) )
76 74 75 bitrdi ( ( 𝐴 ∈ On ∧ Lim { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) → ( 𝐴 ∈ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ↔ ∃ 𝑦 { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } 𝐴 ∈ ( ℵ ‘ 𝑦 ) ) )
77 71 76 mtbird ( ( 𝐴 ∈ On ∧ Lim { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) → ¬ 𝐴 ∈ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) )
78 77 ex ( 𝐴 ∈ On → ( Lim { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } → ¬ 𝐴 ∈ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ) )
79 3 78 syl ( ( card ‘ 𝐴 ) = 𝐴 → ( Lim { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } → ¬ 𝐴 ∈ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ) )
80 61 79 jaod ( ( card ‘ 𝐴 ) = 𝐴 → ( ( ∃ 𝑦 ∈ On { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = suc 𝑦 ∨ Lim { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) → ¬ 𝐴 ∈ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ) )
81 8 17 syl ( 𝐴 ∈ On → 𝐴 ⊆ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) )
82 alephon ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ∈ On
83 onsseleq ( ( 𝐴 ∈ On ∧ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ∈ On ) → ( 𝐴 ⊆ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ↔ ( 𝐴 ∈ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ∨ 𝐴 = ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ) ) )
84 82 83 mpan2 ( 𝐴 ∈ On → ( 𝐴 ⊆ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ↔ ( 𝐴 ∈ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ∨ 𝐴 = ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ) ) )
85 81 84 mpbid ( 𝐴 ∈ On → ( 𝐴 ∈ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ∨ 𝐴 = ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ) )
86 85 ord ( 𝐴 ∈ On → ( ¬ 𝐴 ∈ ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) → 𝐴 = ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ) )
87 3 80 86 sylsyld ( ( card ‘ 𝐴 ) = 𝐴 → ( ( ∃ 𝑦 ∈ On { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = suc 𝑦 ∨ Lim { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) → 𝐴 = ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ) )
88 87 adantl ( ( ω ⊆ 𝐴 ∧ ( card ‘ 𝐴 ) = 𝐴 ) → ( ( ∃ 𝑦 ∈ On { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = suc 𝑦 ∨ Lim { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) → 𝐴 = ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ) )
89 eloni ( { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ∈ On → Ord { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } )
90 ordzsl ( Ord { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ↔ ( { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = ∅ ∨ ∃ 𝑦 ∈ On { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = suc 𝑦 ∨ Lim { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) )
91 3orass ( ( { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = ∅ ∨ ∃ 𝑦 ∈ On { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = suc 𝑦 ∨ Lim { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ↔ ( { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = ∅ ∨ ( ∃ 𝑦 ∈ On { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = suc 𝑦 ∨ Lim { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ) )
92 90 91 bitri ( Ord { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ↔ ( { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = ∅ ∨ ( ∃ 𝑦 ∈ On { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = suc 𝑦 ∨ Lim { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ) )
93 89 92 sylib ( { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ∈ On → ( { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = ∅ ∨ ( ∃ 𝑦 ∈ On { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = suc 𝑦 ∨ Lim { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ) )
94 3 63 93 3syl ( ( card ‘ 𝐴 ) = 𝐴 → ( { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = ∅ ∨ ( ∃ 𝑦 ∈ On { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = suc 𝑦 ∨ Lim { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ) )
95 94 adantl ( ( ω ⊆ 𝐴 ∧ ( card ‘ 𝐴 ) = 𝐴 ) → ( { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = ∅ ∨ ( ∃ 𝑦 ∈ On { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } = suc 𝑦 ∨ Lim { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) ) )
96 29 88 95 mpjaod ( ( ω ⊆ 𝐴 ∧ ( card ‘ 𝐴 ) = 𝐴 ) → 𝐴 = ( ℵ ‘ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) )