This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrrdi ⊢ ( ∩ { 𝑥 ∈ 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 imbitrid ⊢ ( ( 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 ∣ 𝐴 ⊆ ( ℵ ‘ 𝑥 ) } ) )