| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eleq2 2830 | . . 3
⊢ (𝑥 = ∅ → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ ∅)) | 
| 2 |  | fveq2 6906 | . . . 4
⊢ (𝑥 = ∅ →
(ℵ‘𝑥) =
(ℵ‘∅)) | 
| 3 | 2 | breq2d 5155 | . . 3
⊢ (𝑥 = ∅ →
((ℵ‘𝐴) ≺
(ℵ‘𝑥) ↔
(ℵ‘𝐴) ≺
(ℵ‘∅))) | 
| 4 | 1, 3 | imbi12d 344 | . 2
⊢ (𝑥 = ∅ → ((𝐴 ∈ 𝑥 → (ℵ‘𝐴) ≺ (ℵ‘𝑥)) ↔ (𝐴 ∈ ∅ → (ℵ‘𝐴) ≺
(ℵ‘∅)))) | 
| 5 |  | eleq2 2830 | . . 3
⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦)) | 
| 6 |  | fveq2 6906 | . . . 4
⊢ (𝑥 = 𝑦 → (ℵ‘𝑥) = (ℵ‘𝑦)) | 
| 7 | 6 | breq2d 5155 | . . 3
⊢ (𝑥 = 𝑦 → ((ℵ‘𝐴) ≺ (ℵ‘𝑥) ↔ (ℵ‘𝐴) ≺ (ℵ‘𝑦))) | 
| 8 | 5, 7 | imbi12d 344 | . 2
⊢ (𝑥 = 𝑦 → ((𝐴 ∈ 𝑥 → (ℵ‘𝐴) ≺ (ℵ‘𝑥)) ↔ (𝐴 ∈ 𝑦 → (ℵ‘𝐴) ≺ (ℵ‘𝑦)))) | 
| 9 |  | eleq2 2830 | . . 3
⊢ (𝑥 = suc 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ suc 𝑦)) | 
| 10 |  | fveq2 6906 | . . . 4
⊢ (𝑥 = suc 𝑦 → (ℵ‘𝑥) = (ℵ‘suc 𝑦)) | 
| 11 | 10 | breq2d 5155 | . . 3
⊢ (𝑥 = suc 𝑦 → ((ℵ‘𝐴) ≺ (ℵ‘𝑥) ↔ (ℵ‘𝐴) ≺ (ℵ‘suc 𝑦))) | 
| 12 | 9, 11 | imbi12d 344 | . 2
⊢ (𝑥 = suc 𝑦 → ((𝐴 ∈ 𝑥 → (ℵ‘𝐴) ≺ (ℵ‘𝑥)) ↔ (𝐴 ∈ suc 𝑦 → (ℵ‘𝐴) ≺ (ℵ‘suc 𝑦)))) | 
| 13 |  | eleq2 2830 | . . 3
⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵)) | 
| 14 |  | fveq2 6906 | . . . 4
⊢ (𝑥 = 𝐵 → (ℵ‘𝑥) = (ℵ‘𝐵)) | 
| 15 | 14 | breq2d 5155 | . . 3
⊢ (𝑥 = 𝐵 → ((ℵ‘𝐴) ≺ (ℵ‘𝑥) ↔ (ℵ‘𝐴) ≺ (ℵ‘𝐵))) | 
| 16 | 13, 15 | imbi12d 344 | . 2
⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 → (ℵ‘𝐴) ≺ (ℵ‘𝑥)) ↔ (𝐴 ∈ 𝐵 → (ℵ‘𝐴) ≺ (ℵ‘𝐵)))) | 
| 17 |  | noel 4338 | . . 3
⊢  ¬
𝐴 ∈
∅ | 
| 18 | 17 | pm2.21i 119 | . 2
⊢ (𝐴 ∈ ∅ →
(ℵ‘𝐴) ≺
(ℵ‘∅)) | 
| 19 |  | vex 3484 | . . . . 5
⊢ 𝑦 ∈ V | 
| 20 | 19 | elsuc2 6455 | . . . 4
⊢ (𝐴 ∈ suc 𝑦 ↔ (𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦)) | 
| 21 |  | alephordilem1 10113 | . . . . . . . . 9
⊢ (𝑦 ∈ On →
(ℵ‘𝑦) ≺
(ℵ‘suc 𝑦)) | 
| 22 |  | sdomtr 9155 | . . . . . . . . 9
⊢
(((ℵ‘𝐴)
≺ (ℵ‘𝑦)
∧ (ℵ‘𝑦)
≺ (ℵ‘suc 𝑦)) → (ℵ‘𝐴) ≺ (ℵ‘suc 𝑦)) | 
| 23 | 21, 22 | sylan2 593 | . . . . . . . 8
⊢
(((ℵ‘𝐴)
≺ (ℵ‘𝑦)
∧ 𝑦 ∈ On) →
(ℵ‘𝐴) ≺
(ℵ‘suc 𝑦)) | 
| 24 | 23 | expcom 413 | . . . . . . 7
⊢ (𝑦 ∈ On →
((ℵ‘𝐴) ≺
(ℵ‘𝑦) →
(ℵ‘𝐴) ≺
(ℵ‘suc 𝑦))) | 
| 25 | 24 | imim2d 57 | . . . . . 6
⊢ (𝑦 ∈ On → ((𝐴 ∈ 𝑦 → (ℵ‘𝐴) ≺ (ℵ‘𝑦)) → (𝐴 ∈ 𝑦 → (ℵ‘𝐴) ≺ (ℵ‘suc 𝑦)))) | 
| 26 | 25 | com23 86 | . . . . 5
⊢ (𝑦 ∈ On → (𝐴 ∈ 𝑦 → ((𝐴 ∈ 𝑦 → (ℵ‘𝐴) ≺ (ℵ‘𝑦)) → (ℵ‘𝐴) ≺ (ℵ‘suc 𝑦)))) | 
| 27 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝐴 = 𝑦 → (ℵ‘𝐴) = (ℵ‘𝑦)) | 
| 28 | 27 | breq1d 5153 | . . . . . . . 8
⊢ (𝐴 = 𝑦 → ((ℵ‘𝐴) ≺ (ℵ‘suc 𝑦) ↔ (ℵ‘𝑦) ≺ (ℵ‘suc
𝑦))) | 
| 29 | 21, 28 | imbitrrid 246 | . . . . . . 7
⊢ (𝐴 = 𝑦 → (𝑦 ∈ On → (ℵ‘𝐴) ≺ (ℵ‘suc
𝑦))) | 
| 30 | 29 | a1d 25 | . . . . . 6
⊢ (𝐴 = 𝑦 → ((𝐴 ∈ 𝑦 → (ℵ‘𝐴) ≺ (ℵ‘𝑦)) → (𝑦 ∈ On → (ℵ‘𝐴) ≺ (ℵ‘suc
𝑦)))) | 
| 31 | 30 | com3r 87 | . . . . 5
⊢ (𝑦 ∈ On → (𝐴 = 𝑦 → ((𝐴 ∈ 𝑦 → (ℵ‘𝐴) ≺ (ℵ‘𝑦)) → (ℵ‘𝐴) ≺ (ℵ‘suc 𝑦)))) | 
| 32 | 26, 31 | jaod 860 | . . . 4
⊢ (𝑦 ∈ On → ((𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦) → ((𝐴 ∈ 𝑦 → (ℵ‘𝐴) ≺ (ℵ‘𝑦)) → (ℵ‘𝐴) ≺ (ℵ‘suc 𝑦)))) | 
| 33 | 20, 32 | biimtrid 242 | . . 3
⊢ (𝑦 ∈ On → (𝐴 ∈ suc 𝑦 → ((𝐴 ∈ 𝑦 → (ℵ‘𝐴) ≺ (ℵ‘𝑦)) → (ℵ‘𝐴) ≺ (ℵ‘suc 𝑦)))) | 
| 34 | 33 | com23 86 | . 2
⊢ (𝑦 ∈ On → ((𝐴 ∈ 𝑦 → (ℵ‘𝐴) ≺ (ℵ‘𝑦)) → (𝐴 ∈ suc 𝑦 → (ℵ‘𝐴) ≺ (ℵ‘suc 𝑦)))) | 
| 35 |  | fvexd 6921 | . . . . . 6
⊢ (Lim
𝑥 →
(ℵ‘𝑥) ∈
V) | 
| 36 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑤 = 𝐴 → (ℵ‘𝑤) = (ℵ‘𝐴)) | 
| 37 | 36 | ssiun2s 5048 | . . . . . . 7
⊢ (𝐴 ∈ 𝑥 → (ℵ‘𝐴) ⊆ ∪ 𝑤 ∈ 𝑥 (ℵ‘𝑤)) | 
| 38 |  | vex 3484 | . . . . . . . . 9
⊢ 𝑥 ∈ V | 
| 39 |  | alephlim 10107 | . . . . . . . . 9
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → (ℵ‘𝑥) = ∪ 𝑤 ∈ 𝑥 (ℵ‘𝑤)) | 
| 40 | 38, 39 | mpan 690 | . . . . . . . 8
⊢ (Lim
𝑥 →
(ℵ‘𝑥) =
∪ 𝑤 ∈ 𝑥 (ℵ‘𝑤)) | 
| 41 | 40 | sseq2d 4016 | . . . . . . 7
⊢ (Lim
𝑥 →
((ℵ‘𝐴) ⊆
(ℵ‘𝑥) ↔
(ℵ‘𝐴) ⊆
∪ 𝑤 ∈ 𝑥 (ℵ‘𝑤))) | 
| 42 | 37, 41 | imbitrrid 246 | . . . . . 6
⊢ (Lim
𝑥 → (𝐴 ∈ 𝑥 → (ℵ‘𝐴) ⊆ (ℵ‘𝑥))) | 
| 43 |  | ssdomg 9040 | . . . . . 6
⊢
((ℵ‘𝑥)
∈ V → ((ℵ‘𝐴) ⊆ (ℵ‘𝑥) → (ℵ‘𝐴) ≼ (ℵ‘𝑥))) | 
| 44 | 35, 42, 43 | sylsyld 61 | . . . . 5
⊢ (Lim
𝑥 → (𝐴 ∈ 𝑥 → (ℵ‘𝐴) ≼ (ℵ‘𝑥))) | 
| 45 |  | limsuc 7870 | . . . . . . . . . 10
⊢ (Lim
𝑥 → (𝐴 ∈ 𝑥 ↔ suc 𝐴 ∈ 𝑥)) | 
| 46 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ (𝑤 = suc 𝐴 → (ℵ‘𝑤) = (ℵ‘suc 𝐴)) | 
| 47 | 46 | ssiun2s 5048 | . . . . . . . . . . . 12
⊢ (suc
𝐴 ∈ 𝑥 → (ℵ‘suc 𝐴) ⊆ ∪ 𝑤 ∈ 𝑥 (ℵ‘𝑤)) | 
| 48 | 40 | sseq2d 4016 | . . . . . . . . . . . 12
⊢ (Lim
𝑥 →
((ℵ‘suc 𝐴)
⊆ (ℵ‘𝑥)
↔ (ℵ‘suc 𝐴) ⊆ ∪ 𝑤 ∈ 𝑥 (ℵ‘𝑤))) | 
| 49 | 47, 48 | imbitrrid 246 | . . . . . . . . . . 11
⊢ (Lim
𝑥 → (suc 𝐴 ∈ 𝑥 → (ℵ‘suc 𝐴) ⊆ (ℵ‘𝑥))) | 
| 50 |  | ssdomg 9040 | . . . . . . . . . . 11
⊢
((ℵ‘𝑥)
∈ V → ((ℵ‘suc 𝐴) ⊆ (ℵ‘𝑥) → (ℵ‘suc 𝐴) ≼ (ℵ‘𝑥))) | 
| 51 | 35, 49, 50 | sylsyld 61 | . . . . . . . . . 10
⊢ (Lim
𝑥 → (suc 𝐴 ∈ 𝑥 → (ℵ‘suc 𝐴) ≼ (ℵ‘𝑥))) | 
| 52 | 45, 51 | sylbid 240 | . . . . . . . . 9
⊢ (Lim
𝑥 → (𝐴 ∈ 𝑥 → (ℵ‘suc 𝐴) ≼ (ℵ‘𝑥))) | 
| 53 | 52 | imp 406 | . . . . . . . 8
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ 𝑥) → (ℵ‘suc 𝐴) ≼ (ℵ‘𝑥)) | 
| 54 |  | domnsym 9139 | . . . . . . . 8
⊢
((ℵ‘suc 𝐴) ≼ (ℵ‘𝑥) → ¬ (ℵ‘𝑥) ≺ (ℵ‘suc
𝐴)) | 
| 55 | 53, 54 | syl 17 | . . . . . . 7
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ 𝑥) → ¬ (ℵ‘𝑥) ≺ (ℵ‘suc
𝐴)) | 
| 56 |  | limelon 6448 | . . . . . . . . . 10
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On) | 
| 57 | 38, 56 | mpan 690 | . . . . . . . . 9
⊢ (Lim
𝑥 → 𝑥 ∈ On) | 
| 58 |  | onelon 6409 | . . . . . . . . 9
⊢ ((𝑥 ∈ On ∧ 𝐴 ∈ 𝑥) → 𝐴 ∈ On) | 
| 59 | 57, 58 | sylan 580 | . . . . . . . 8
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ 𝑥) → 𝐴 ∈ On) | 
| 60 |  | ensym 9043 | . . . . . . . . 9
⊢
((ℵ‘𝐴)
≈ (ℵ‘𝑥)
→ (ℵ‘𝑥)
≈ (ℵ‘𝐴)) | 
| 61 |  | alephordilem1 10113 | . . . . . . . . 9
⊢ (𝐴 ∈ On →
(ℵ‘𝐴) ≺
(ℵ‘suc 𝐴)) | 
| 62 |  | ensdomtr 9153 | . . . . . . . . . 10
⊢
(((ℵ‘𝑥)
≈ (ℵ‘𝐴)
∧ (ℵ‘𝐴)
≺ (ℵ‘suc 𝐴)) → (ℵ‘𝑥) ≺ (ℵ‘suc 𝐴)) | 
| 63 | 62 | ex 412 | . . . . . . . . 9
⊢
((ℵ‘𝑥)
≈ (ℵ‘𝐴)
→ ((ℵ‘𝐴)
≺ (ℵ‘suc 𝐴) → (ℵ‘𝑥) ≺ (ℵ‘suc 𝐴))) | 
| 64 | 60, 61, 63 | syl2im 40 | . . . . . . . 8
⊢
((ℵ‘𝐴)
≈ (ℵ‘𝑥)
→ (𝐴 ∈ On →
(ℵ‘𝑥) ≺
(ℵ‘suc 𝐴))) | 
| 65 | 59, 64 | syl5com 31 | . . . . . . 7
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ 𝑥) → ((ℵ‘𝐴) ≈ (ℵ‘𝑥) → (ℵ‘𝑥) ≺ (ℵ‘suc 𝐴))) | 
| 66 | 55, 65 | mtod 198 | . . . . . 6
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ 𝑥) → ¬ (ℵ‘𝐴) ≈ (ℵ‘𝑥)) | 
| 67 | 66 | ex 412 | . . . . 5
⊢ (Lim
𝑥 → (𝐴 ∈ 𝑥 → ¬ (ℵ‘𝐴) ≈ (ℵ‘𝑥))) | 
| 68 | 44, 67 | jcad 512 | . . . 4
⊢ (Lim
𝑥 → (𝐴 ∈ 𝑥 → ((ℵ‘𝐴) ≼ (ℵ‘𝑥) ∧ ¬ (ℵ‘𝐴) ≈ (ℵ‘𝑥)))) | 
| 69 |  | brsdom 9015 | . . . 4
⊢
((ℵ‘𝐴)
≺ (ℵ‘𝑥)
↔ ((ℵ‘𝐴)
≼ (ℵ‘𝑥)
∧ ¬ (ℵ‘𝐴) ≈ (ℵ‘𝑥))) | 
| 70 | 68, 69 | imbitrrdi 252 | . . 3
⊢ (Lim
𝑥 → (𝐴 ∈ 𝑥 → (ℵ‘𝐴) ≺ (ℵ‘𝑥))) | 
| 71 | 70 | a1d 25 | . 2
⊢ (Lim
𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ∈ 𝑦 → (ℵ‘𝐴) ≺ (ℵ‘𝑦)) → (𝐴 ∈ 𝑥 → (ℵ‘𝐴) ≺ (ℵ‘𝑥)))) | 
| 72 | 4, 8, 12, 16, 18, 34, 71 | tfinds 7881 | 1
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → (ℵ‘𝐴) ≺ (ℵ‘𝐵))) |