Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cardaleph Structured version   Visualization version   GIF version

Theorem cardaleph 9112
 Description: Given any transfinite cardinal number 𝐴, there is exactly one aleph that is equal to it. Here we compute that aleph explicitly. (Contributed by NM, 9-Nov-2003.) (Revised by Mario Carneiro, 2-Feb-2013.)
Assertion
Ref Expression
cardaleph ((ω ⊆ 𝐴 ∧ (card‘𝐴) = 𝐴) → 𝐴 = (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}))
Distinct variable group:   𝑥,𝐴

Proof of Theorem cardaleph
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 cardon 8970 . . . . . . . . 9 (card‘𝐴) ∈ On
2 eleq1 2838 . . . . . . . . 9 ((card‘𝐴) = 𝐴 → ((card‘𝐴) ∈ On ↔ 𝐴 ∈ On))
31, 2mpbii 223 . . . . . . . 8 ((card‘𝐴) = 𝐴𝐴 ∈ On)
4 alephle 9111 . . . . . . . . 9 (𝐴 ∈ On → 𝐴 ⊆ (ℵ‘𝐴))
5 fveq2 6332 . . . . . . . . . . 11 (𝑥 = 𝐴 → (ℵ‘𝑥) = (ℵ‘𝐴))
65sseq2d 3782 . . . . . . . . . 10 (𝑥 = 𝐴 → (𝐴 ⊆ (ℵ‘𝑥) ↔ 𝐴 ⊆ (ℵ‘𝐴)))
76rspcev 3460 . . . . . . . . 9 ((𝐴 ∈ On ∧ 𝐴 ⊆ (ℵ‘𝐴)) → ∃𝑥 ∈ On 𝐴 ⊆ (ℵ‘𝑥))
84, 7mpdan 667 . . . . . . . 8 (𝐴 ∈ On → ∃𝑥 ∈ On 𝐴 ⊆ (ℵ‘𝑥))
9 nfcv 2913 . . . . . . . . . 10 𝑥𝐴
10 nfcv 2913 . . . . . . . . . . 11 𝑥
11 nfrab1 3271 . . . . . . . . . . . 12 𝑥{𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}
1211nfint 4621 . . . . . . . . . . 11 𝑥 {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}
1310, 12nffv 6339 . . . . . . . . . 10 𝑥(ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)})
149, 13nfss 3745 . . . . . . . . 9 𝑥 𝐴 ⊆ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)})
15 fveq2 6332 . . . . . . . . . 10 (𝑥 = {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} → (ℵ‘𝑥) = (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}))
1615sseq2d 3782 . . . . . . . . 9 (𝑥 = {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} → (𝐴 ⊆ (ℵ‘𝑥) ↔ 𝐴 ⊆ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)})))
1714, 16onminsb 7146 . . . . . . . 8 (∃𝑥 ∈ On 𝐴 ⊆ (ℵ‘𝑥) → 𝐴 ⊆ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}))
183, 8, 173syl 18 . . . . . . 7 ((card‘𝐴) = 𝐴𝐴 ⊆ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}))
1918a1i 11 . . . . . 6 ( {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = ∅ → ((card‘𝐴) = 𝐴𝐴 ⊆ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)})))
20 fveq2 6332 . . . . . . . . 9 ( {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = ∅ → (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) = (ℵ‘∅))
21 aleph0 9089 . . . . . . . . 9 (ℵ‘∅) = ω
2220, 21syl6eq 2821 . . . . . . . 8 ( {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = ∅ → (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) = ω)
2322sseq1d 3781 . . . . . . 7 ( {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = ∅ → ((ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ⊆ 𝐴 ↔ ω ⊆ 𝐴))
2423biimprd 238 . . . . . 6 ( {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = ∅ → (ω ⊆ 𝐴 → (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ⊆ 𝐴))
2519, 24anim12d 596 . . . . 5 ( {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = ∅ → (((card‘𝐴) = 𝐴 ∧ ω ⊆ 𝐴) → (𝐴 ⊆ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ∧ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ⊆ 𝐴)))
26 eqss 3767 . . . . 5 (𝐴 = (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ↔ (𝐴 ⊆ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ∧ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ⊆ 𝐴))
2725, 26syl6ibr 242 . . . 4 ( {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = ∅ → (((card‘𝐴) = 𝐴 ∧ ω ⊆ 𝐴) → 𝐴 = (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)})))
2827com12 32 . . 3 (((card‘𝐴) = 𝐴 ∧ ω ⊆ 𝐴) → ( {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = ∅ → 𝐴 = (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)})))
2928ancoms 455 . 2 ((ω ⊆ 𝐴 ∧ (card‘𝐴) = 𝐴) → ( {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = ∅ → 𝐴 = (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)})))
30 vex 3354 . . . . . . . . . . . 12 𝑦 ∈ V
3130sucid 5947 . . . . . . . . . . 11 𝑦 ∈ suc 𝑦
32 eleq2 2839 . . . . . . . . . . 11 ( {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦 → (𝑦 {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} ↔ 𝑦 ∈ suc 𝑦))
3331, 32mpbiri 248 . . . . . . . . . 10 ( {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦𝑦 {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)})
34 fveq2 6332 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (ℵ‘𝑥) = (ℵ‘𝑦))
3534sseq2d 3782 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝐴 ⊆ (ℵ‘𝑥) ↔ 𝐴 ⊆ (ℵ‘𝑦)))
3635onnminsb 7151 . . . . . . . . . 10 (𝑦 ∈ On → (𝑦 {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} → ¬ 𝐴 ⊆ (ℵ‘𝑦)))
3733, 36syl5 34 . . . . . . . . 9 (𝑦 ∈ On → ( {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦 → ¬ 𝐴 ⊆ (ℵ‘𝑦)))
3837imp 393 . . . . . . . 8 ((𝑦 ∈ On ∧ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦) → ¬ 𝐴 ⊆ (ℵ‘𝑦))
3938adantl 467 . . . . . . 7 (((card‘𝐴) = 𝐴 ∧ (𝑦 ∈ On ∧ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦)) → ¬ 𝐴 ⊆ (ℵ‘𝑦))
40 fveq2 6332 . . . . . . . . . . 11 ( {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦 → (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) = (ℵ‘suc 𝑦))
41 alephsuc 9091 . . . . . . . . . . 11 (𝑦 ∈ On → (ℵ‘suc 𝑦) = (har‘(ℵ‘𝑦)))
4240, 41sylan9eqr 2827 . . . . . . . . . 10 ((𝑦 ∈ On ∧ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦) → (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) = (har‘(ℵ‘𝑦)))
4342eleq2d 2836 . . . . . . . . 9 ((𝑦 ∈ On ∧ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦) → (𝐴 ∈ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ↔ 𝐴 ∈ (har‘(ℵ‘𝑦))))
4443biimpd 219 . . . . . . . 8 ((𝑦 ∈ On ∧ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦) → (𝐴 ∈ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) → 𝐴 ∈ (har‘(ℵ‘𝑦))))
45 elharval 8624 . . . . . . . . . 10 (𝐴 ∈ (har‘(ℵ‘𝑦)) ↔ (𝐴 ∈ On ∧ 𝐴 ≼ (ℵ‘𝑦)))
4645simprbi 484 . . . . . . . . 9 (𝐴 ∈ (har‘(ℵ‘𝑦)) → 𝐴 ≼ (ℵ‘𝑦))
47 onenon 8975 . . . . . . . . . . . 12 (𝐴 ∈ On → 𝐴 ∈ dom card)
483, 47syl 17 . . . . . . . . . . 11 ((card‘𝐴) = 𝐴𝐴 ∈ dom card)
49 alephon 9092 . . . . . . . . . . . 12 (ℵ‘𝑦) ∈ On
50 onenon 8975 . . . . . . . . . . . 12 ((ℵ‘𝑦) ∈ On → (ℵ‘𝑦) ∈ dom card)
5149, 50ax-mp 5 . . . . . . . . . . 11 (ℵ‘𝑦) ∈ dom card
52 carddom2 9003 . . . . . . . . . . 11 ((𝐴 ∈ dom card ∧ (ℵ‘𝑦) ∈ dom card) → ((card‘𝐴) ⊆ (card‘(ℵ‘𝑦)) ↔ 𝐴 ≼ (ℵ‘𝑦)))
5348, 51, 52sylancl 574 . . . . . . . . . 10 ((card‘𝐴) = 𝐴 → ((card‘𝐴) ⊆ (card‘(ℵ‘𝑦)) ↔ 𝐴 ≼ (ℵ‘𝑦)))
54 sseq1 3775 . . . . . . . . . . 11 ((card‘𝐴) = 𝐴 → ((card‘𝐴) ⊆ (card‘(ℵ‘𝑦)) ↔ 𝐴 ⊆ (card‘(ℵ‘𝑦))))
55 alephcard 9093 . . . . . . . . . . . 12 (card‘(ℵ‘𝑦)) = (ℵ‘𝑦)
5655sseq2i 3779 . . . . . . . . . . 11 (𝐴 ⊆ (card‘(ℵ‘𝑦)) ↔ 𝐴 ⊆ (ℵ‘𝑦))
5754, 56syl6bb 276 . . . . . . . . . 10 ((card‘𝐴) = 𝐴 → ((card‘𝐴) ⊆ (card‘(ℵ‘𝑦)) ↔ 𝐴 ⊆ (ℵ‘𝑦)))
5853, 57bitr3d 270 . . . . . . . . 9 ((card‘𝐴) = 𝐴 → (𝐴 ≼ (ℵ‘𝑦) ↔ 𝐴 ⊆ (ℵ‘𝑦)))
5946, 58syl5ib 234 . . . . . . . 8 ((card‘𝐴) = 𝐴 → (𝐴 ∈ (har‘(ℵ‘𝑦)) → 𝐴 ⊆ (ℵ‘𝑦)))
6044, 59sylan9r 498 . . . . . . 7 (((card‘𝐴) = 𝐴 ∧ (𝑦 ∈ On ∧ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦)) → (𝐴 ∈ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) → 𝐴 ⊆ (ℵ‘𝑦)))
6139, 60mtod 189 . . . . . 6 (((card‘𝐴) = 𝐴 ∧ (𝑦 ∈ On ∧ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦)) → ¬ 𝐴 ∈ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}))
6261rexlimdvaa 3180 . . . . 5 ((card‘𝐴) = 𝐴 → (∃𝑦 ∈ On {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦 → ¬ 𝐴 ∈ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)})))
63 onintrab2 7149 . . . . . . . . . . . . . 14 (∃𝑥 ∈ On 𝐴 ⊆ (ℵ‘𝑥) ↔ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} ∈ On)
648, 63sylib 208 . . . . . . . . . . . . 13 (𝐴 ∈ On → {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} ∈ On)
65 onelon 5891 . . . . . . . . . . . . 13 (( {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} ∈ On ∧ 𝑦 {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) → 𝑦 ∈ On)
6664, 65sylan 569 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ 𝑦 {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) → 𝑦 ∈ On)
6736adantld 478 . . . . . . . . . . . 12 (𝑦 ∈ On → ((𝐴 ∈ On ∧ 𝑦 {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) → ¬ 𝐴 ⊆ (ℵ‘𝑦)))
6866, 67mpcom 38 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ 𝑦 {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) → ¬ 𝐴 ⊆ (ℵ‘𝑦))
6949onelssi 5979 . . . . . . . . . . 11 (𝐴 ∈ (ℵ‘𝑦) → 𝐴 ⊆ (ℵ‘𝑦))
7068, 69nsyl 137 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝑦 {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) → ¬ 𝐴 ∈ (ℵ‘𝑦))
7170nrexdv 3149 . . . . . . . . 9 (𝐴 ∈ On → ¬ ∃𝑦 {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}𝐴 ∈ (ℵ‘𝑦))
7271adantr 466 . . . . . . . 8 ((𝐴 ∈ On ∧ Lim {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) → ¬ ∃𝑦 {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}𝐴 ∈ (ℵ‘𝑦))
73 alephlim 9090 . . . . . . . . . . 11 (( {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} ∈ On ∧ Lim {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) → (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) = 𝑦 {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} (ℵ‘𝑦))
7464, 73sylan 569 . . . . . . . . . 10 ((𝐴 ∈ On ∧ Lim {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) → (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) = 𝑦 {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} (ℵ‘𝑦))
7574eleq2d 2836 . . . . . . . . 9 ((𝐴 ∈ On ∧ Lim {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) → (𝐴 ∈ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ↔ 𝐴 𝑦 {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} (ℵ‘𝑦)))
76 eliun 4658 . . . . . . . . 9 (𝐴 𝑦 {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} (ℵ‘𝑦) ↔ ∃𝑦 {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}𝐴 ∈ (ℵ‘𝑦))
7775, 76syl6bb 276 . . . . . . . 8 ((𝐴 ∈ On ∧ Lim {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) → (𝐴 ∈ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ↔ ∃𝑦 {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}𝐴 ∈ (ℵ‘𝑦)))
7872, 77mtbird 314 . . . . . . 7 ((𝐴 ∈ On ∧ Lim {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) → ¬ 𝐴 ∈ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}))
7978ex 397 . . . . . 6 (𝐴 ∈ On → (Lim {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} → ¬ 𝐴 ∈ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)})))
803, 79syl 17 . . . . 5 ((card‘𝐴) = 𝐴 → (Lim {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} → ¬ 𝐴 ∈ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)})))
8162, 80jaod 848 . . . 4 ((card‘𝐴) = 𝐴 → ((∃𝑦 ∈ On {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦 ∨ Lim {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) → ¬ 𝐴 ∈ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)})))
828, 17syl 17 . . . . . 6 (𝐴 ∈ On → 𝐴 ⊆ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}))
83 alephon 9092 . . . . . . 7 (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ∈ On
84 onsseleq 5908 . . . . . . 7 ((𝐴 ∈ On ∧ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ∈ On) → (𝐴 ⊆ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ↔ (𝐴 ∈ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ∨ 𝐴 = (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}))))
8583, 84mpan2 671 . . . . . 6 (𝐴 ∈ On → (𝐴 ⊆ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ↔ (𝐴 ∈ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ∨ 𝐴 = (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}))))
8682, 85mpbid 222 . . . . 5 (𝐴 ∈ On → (𝐴 ∈ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ∨ 𝐴 = (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)})))
8786ord 853 . . . 4 (𝐴 ∈ On → (¬ 𝐴 ∈ (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) → 𝐴 = (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)})))
883, 81, 87sylsyld 61 . . 3 ((card‘𝐴) = 𝐴 → ((∃𝑦 ∈ On {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦 ∨ Lim {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) → 𝐴 = (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)})))
8988adantl 467 . 2 ((ω ⊆ 𝐴 ∧ (card‘𝐴) = 𝐴) → ((∃𝑦 ∈ On {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦 ∨ Lim {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) → 𝐴 = (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)})))
90 eloni 5876 . . . . 5 ( {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} ∈ On → Ord {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)})
91 ordzsl 7192 . . . . . 6 (Ord {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} ↔ ( {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = ∅ ∨ ∃𝑦 ∈ On {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦 ∨ Lim {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}))
92 3orass 1074 . . . . . 6 (( {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = ∅ ∨ ∃𝑦 ∈ On {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦 ∨ Lim {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ↔ ( {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = ∅ ∨ (∃𝑦 ∈ On {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦 ∨ Lim {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)})))
9391, 92bitri 264 . . . . 5 (Ord {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} ↔ ( {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = ∅ ∨ (∃𝑦 ∈ On {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦 ∨ Lim {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)})))
9490, 93sylib 208 . . . 4 ( {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} ∈ On → ( {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = ∅ ∨ (∃𝑦 ∈ On {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦 ∨ Lim {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)})))
953, 64, 943syl 18 . . 3 ((card‘𝐴) = 𝐴 → ( {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = ∅ ∨ (∃𝑦 ∈ On {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦 ∨ Lim {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)})))
9695adantl 467 . 2 ((ω ⊆ 𝐴 ∧ (card‘𝐴) = 𝐴) → ( {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = ∅ ∨ (∃𝑦 ∈ On {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦 ∨ Lim {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)})))
9729, 89, 96mpjaod 849 1 ((ω ⊆ 𝐴 ∧ (card‘𝐴) = 𝐴) → 𝐴 = (ℵ‘ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 382   ∨ wo 836   ∨ w3o 1070   = wceq 1631   ∈ wcel 2145  ∃wrex 3062  {crab 3065   ⊆ wss 3723  ∅c0 4063  ∩ cint 4611  ∪ ciun 4654   class class class wbr 4786  dom cdm 5249  Ord word 5865  Oncon0 5866  Lim wlim 5867  suc csuc 5868  ‘cfv 6031  ωcom 7212   ≼ cdom 8107  harchar 8617  cardccrd 8961  ℵcale 8962 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-inf2 8702 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-om 7213  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-er 7896  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-oi 8571  df-har 8619  df-card 8965  df-aleph 8966 This theorem is referenced by:  cardalephex  9113  tskcard  9805
 Copyright terms: Public domain W3C validator