| Step | Hyp | Ref
| Expression |
| 1 | | alephordi 10114 |
. . . . 5
⊢ (𝐴 ∈ On → (𝑦 ∈ 𝐴 → (ℵ‘𝑦) ≺ (ℵ‘𝐴))) |
| 2 | 1 | ralrimiv 3145 |
. . . 4
⊢ (𝐴 ∈ On → ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ (ℵ‘𝐴)) |
| 3 | | alephon 10109 |
. . . 4
⊢
(ℵ‘𝐴)
∈ On |
| 4 | 2, 3 | jctil 519 |
. . 3
⊢ (𝐴 ∈ On →
((ℵ‘𝐴) ∈
On ∧ ∀𝑦 ∈
𝐴 (ℵ‘𝑦) ≺ (ℵ‘𝐴))) |
| 5 | | breq2 5147 |
. . . . 5
⊢ (𝑥 = (ℵ‘𝐴) → ((ℵ‘𝑦) ≺ 𝑥 ↔ (ℵ‘𝑦) ≺ (ℵ‘𝐴))) |
| 6 | 5 | ralbidv 3178 |
. . . 4
⊢ (𝑥 = (ℵ‘𝐴) → (∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥 ↔ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ (ℵ‘𝐴))) |
| 7 | 6 | elrab 3692 |
. . 3
⊢
((ℵ‘𝐴)
∈ {𝑥 ∈ On ∣
∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥} ↔ ((ℵ‘𝐴) ∈ On ∧ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ (ℵ‘𝐴))) |
| 8 | 4, 7 | sylibr 234 |
. 2
⊢ (𝐴 ∈ On →
(ℵ‘𝐴) ∈
{𝑥 ∈ On ∣
∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥}) |
| 9 | | cardsdomelir 10013 |
. . . . 5
⊢ (𝑧 ∈
(card‘(ℵ‘𝐴)) → 𝑧 ≺ (ℵ‘𝐴)) |
| 10 | | alephcard 10110 |
. . . . . 6
⊢
(card‘(ℵ‘𝐴)) = (ℵ‘𝐴) |
| 11 | 10 | eqcomi 2746 |
. . . . 5
⊢
(ℵ‘𝐴) =
(card‘(ℵ‘𝐴)) |
| 12 | 9, 11 | eleq2s 2859 |
. . . 4
⊢ (𝑧 ∈ (ℵ‘𝐴) → 𝑧 ≺ (ℵ‘𝐴)) |
| 13 | | omex 9683 |
. . . . . 6
⊢ ω
∈ V |
| 14 | | vex 3484 |
. . . . . 6
⊢ 𝑧 ∈ V |
| 15 | | entri3 10599 |
. . . . . 6
⊢ ((ω
∈ V ∧ 𝑧 ∈ V)
→ (ω ≼ 𝑧
∨ 𝑧 ≼
ω)) |
| 16 | 13, 14, 15 | mp2an 692 |
. . . . 5
⊢ (ω
≼ 𝑧 ∨ 𝑧 ≼
ω) |
| 17 | | carddom 10594 |
. . . . . . . . . 10
⊢ ((ω
∈ V ∧ 𝑧 ∈ V)
→ ((card‘ω) ⊆ (card‘𝑧) ↔ ω ≼ 𝑧)) |
| 18 | 13, 14, 17 | mp2an 692 |
. . . . . . . . 9
⊢
((card‘ω) ⊆ (card‘𝑧) ↔ ω ≼ 𝑧) |
| 19 | | cardom 10026 |
. . . . . . . . . 10
⊢
(card‘ω) = ω |
| 20 | 19 | sseq1i 4012 |
. . . . . . . . 9
⊢
((card‘ω) ⊆ (card‘𝑧) ↔ ω ⊆ (card‘𝑧)) |
| 21 | 18, 20 | bitr3i 277 |
. . . . . . . 8
⊢ (ω
≼ 𝑧 ↔ ω
⊆ (card‘𝑧)) |
| 22 | | cardidm 9999 |
. . . . . . . . . 10
⊢
(card‘(card‘𝑧)) = (card‘𝑧) |
| 23 | | cardalephex 10130 |
. . . . . . . . . 10
⊢ (ω
⊆ (card‘𝑧)
→ ((card‘(card‘𝑧)) = (card‘𝑧) ↔ ∃𝑥 ∈ On (card‘𝑧) = (ℵ‘𝑥))) |
| 24 | 22, 23 | mpbii 233 |
. . . . . . . . 9
⊢ (ω
⊆ (card‘𝑧)
→ ∃𝑥 ∈ On
(card‘𝑧) =
(ℵ‘𝑥)) |
| 25 | | alephord 10115 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ On ∧ 𝐴 ∈ On) → (𝑥 ∈ 𝐴 ↔ (ℵ‘𝑥) ≺ (ℵ‘𝐴))) |
| 26 | 25 | ancoms 458 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝑥 ∈ 𝐴 ↔ (ℵ‘𝑥) ≺ (ℵ‘𝐴))) |
| 27 | | breq1 5146 |
. . . . . . . . . . . . 13
⊢
((card‘𝑧) =
(ℵ‘𝑥) →
((card‘𝑧) ≺
(ℵ‘𝐴) ↔
(ℵ‘𝑥) ≺
(ℵ‘𝐴))) |
| 28 | 14 | cardid 10587 |
. . . . . . . . . . . . . 14
⊢
(card‘𝑧)
≈ 𝑧 |
| 29 | | sdomen1 9161 |
. . . . . . . . . . . . . 14
⊢
((card‘𝑧)
≈ 𝑧 →
((card‘𝑧) ≺
(ℵ‘𝐴) ↔
𝑧 ≺
(ℵ‘𝐴))) |
| 30 | 28, 29 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
((card‘𝑧)
≺ (ℵ‘𝐴)
↔ 𝑧 ≺
(ℵ‘𝐴)) |
| 31 | 27, 30 | bitr3di 286 |
. . . . . . . . . . . 12
⊢
((card‘𝑧) =
(ℵ‘𝑥) →
((ℵ‘𝑥) ≺
(ℵ‘𝐴) ↔
𝑧 ≺
(ℵ‘𝐴))) |
| 32 | 26, 31 | sylan9bb 509 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧
(card‘𝑧) =
(ℵ‘𝑥)) →
(𝑥 ∈ 𝐴 ↔ 𝑧 ≺ (ℵ‘𝐴))) |
| 33 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑥 → (ℵ‘𝑦) = (ℵ‘𝑥)) |
| 34 | 33 | breq1d 5153 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑥 → ((ℵ‘𝑦) ≺ 𝑧 ↔ (ℵ‘𝑥) ≺ 𝑧)) |
| 35 | 34 | rspcv 3618 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧 → (ℵ‘𝑥) ≺ 𝑧)) |
| 36 | | sdomirr 9154 |
. . . . . . . . . . . . . . 15
⊢ ¬
(ℵ‘𝑥) ≺
(ℵ‘𝑥) |
| 37 | | sdomen2 9162 |
. . . . . . . . . . . . . . . . 17
⊢
((card‘𝑧)
≈ 𝑧 →
((ℵ‘𝑥) ≺
(card‘𝑧) ↔
(ℵ‘𝑥) ≺
𝑧)) |
| 38 | 28, 37 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
((ℵ‘𝑥)
≺ (card‘𝑧)
↔ (ℵ‘𝑥)
≺ 𝑧) |
| 39 | | breq2 5147 |
. . . . . . . . . . . . . . . 16
⊢
((card‘𝑧) =
(ℵ‘𝑥) →
((ℵ‘𝑥) ≺
(card‘𝑧) ↔
(ℵ‘𝑥) ≺
(ℵ‘𝑥))) |
| 40 | 38, 39 | bitr3id 285 |
. . . . . . . . . . . . . . 15
⊢
((card‘𝑧) =
(ℵ‘𝑥) →
((ℵ‘𝑥) ≺
𝑧 ↔
(ℵ‘𝑥) ≺
(ℵ‘𝑥))) |
| 41 | 36, 40 | mtbiri 327 |
. . . . . . . . . . . . . 14
⊢
((card‘𝑧) =
(ℵ‘𝑥) →
¬ (ℵ‘𝑥)
≺ 𝑧) |
| 42 | 35, 41 | nsyli 157 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 → ((card‘𝑧) = (ℵ‘𝑥) → ¬ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧)) |
| 43 | 42 | com12 32 |
. . . . . . . . . . . 12
⊢
((card‘𝑧) =
(ℵ‘𝑥) →
(𝑥 ∈ 𝐴 → ¬ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧)) |
| 44 | 43 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧
(card‘𝑧) =
(ℵ‘𝑥)) →
(𝑥 ∈ 𝐴 → ¬ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧)) |
| 45 | 32, 44 | sylbird 260 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧
(card‘𝑧) =
(ℵ‘𝑥)) →
(𝑧 ≺
(ℵ‘𝐴) →
¬ ∀𝑦 ∈
𝐴 (ℵ‘𝑦) ≺ 𝑧)) |
| 46 | 45 | rexlimdva2 3157 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → (∃𝑥 ∈ On (card‘𝑧) = (ℵ‘𝑥) → (𝑧 ≺ (ℵ‘𝐴) → ¬ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧))) |
| 47 | 24, 46 | syl5 34 |
. . . . . . . 8
⊢ (𝐴 ∈ On → (ω
⊆ (card‘𝑧)
→ (𝑧 ≺
(ℵ‘𝐴) →
¬ ∀𝑦 ∈
𝐴 (ℵ‘𝑦) ≺ 𝑧))) |
| 48 | 21, 47 | biimtrid 242 |
. . . . . . 7
⊢ (𝐴 ∈ On → (ω
≼ 𝑧 → (𝑧 ≺ (ℵ‘𝐴) → ¬ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧))) |
| 49 | 48 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → (ω ≼
𝑧 → (𝑧 ≺ (ℵ‘𝐴) → ¬ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧))) |
| 50 | | ne0i 4341 |
. . . . . . . . . . . 12
⊢ (∅
∈ 𝐴 → 𝐴 ≠ ∅) |
| 51 | | onelon 6409 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ On) |
| 52 | | alephgeom 10122 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ On ↔ ω
⊆ (ℵ‘𝑦)) |
| 53 | | alephon 10109 |
. . . . . . . . . . . . . . . . . . 19
⊢
(ℵ‘𝑦)
∈ On |
| 54 | | ssdomg 9040 |
. . . . . . . . . . . . . . . . . . 19
⊢
((ℵ‘𝑦)
∈ On → (ω ⊆ (ℵ‘𝑦) → ω ≼ (ℵ‘𝑦))) |
| 55 | 53, 54 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ (ω
⊆ (ℵ‘𝑦)
→ ω ≼ (ℵ‘𝑦)) |
| 56 | 52, 55 | sylbi 217 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ On → ω
≼ (ℵ‘𝑦)) |
| 57 | | domtr 9047 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ≼ ω ∧ ω
≼ (ℵ‘𝑦))
→ 𝑧 ≼
(ℵ‘𝑦)) |
| 58 | 56, 57 | sylan2 593 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ≼ ω ∧ 𝑦 ∈ On) → 𝑧 ≼ (ℵ‘𝑦)) |
| 59 | | domnsym 9139 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ≼ (ℵ‘𝑦) → ¬
(ℵ‘𝑦) ≺
𝑧) |
| 60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ≼ ω ∧ 𝑦 ∈ On) → ¬
(ℵ‘𝑦) ≺
𝑧) |
| 61 | 51, 60 | sylan2 593 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ≼ ω ∧ (𝐴 ∈ On ∧ 𝑦 ∈ 𝐴)) → ¬ (ℵ‘𝑦) ≺ 𝑧) |
| 62 | 61 | expr 456 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ≼ ω ∧ 𝐴 ∈ On) → (𝑦 ∈ 𝐴 → ¬ (ℵ‘𝑦) ≺ 𝑧)) |
| 63 | 62 | ralrimiv 3145 |
. . . . . . . . . . . 12
⊢ ((𝑧 ≼ ω ∧ 𝐴 ∈ On) → ∀𝑦 ∈ 𝐴 ¬ (ℵ‘𝑦) ≺ 𝑧) |
| 64 | | r19.2z 4495 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 ¬ (ℵ‘𝑦) ≺ 𝑧) → ∃𝑦 ∈ 𝐴 ¬ (ℵ‘𝑦) ≺ 𝑧) |
| 65 | 64 | ex 412 |
. . . . . . . . . . . 12
⊢ (𝐴 ≠ ∅ →
(∀𝑦 ∈ 𝐴 ¬ (ℵ‘𝑦) ≺ 𝑧 → ∃𝑦 ∈ 𝐴 ¬ (ℵ‘𝑦) ≺ 𝑧)) |
| 66 | 50, 63, 65 | syl2im 40 |
. . . . . . . . . . 11
⊢ (∅
∈ 𝐴 → ((𝑧 ≼ ω ∧ 𝐴 ∈ On) → ∃𝑦 ∈ 𝐴 ¬ (ℵ‘𝑦) ≺ 𝑧)) |
| 67 | | rexnal 3100 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
𝐴 ¬
(ℵ‘𝑦) ≺
𝑧 ↔ ¬
∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧) |
| 68 | 66, 67 | imbitrdi 251 |
. . . . . . . . . 10
⊢ (∅
∈ 𝐴 → ((𝑧 ≼ ω ∧ 𝐴 ∈ On) → ¬
∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧)) |
| 69 | 68 | com12 32 |
. . . . . . . . 9
⊢ ((𝑧 ≼ ω ∧ 𝐴 ∈ On) → (∅
∈ 𝐴 → ¬
∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧)) |
| 70 | 69 | expimpd 453 |
. . . . . . . 8
⊢ (𝑧 ≼ ω → ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → ¬
∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧)) |
| 71 | 70 | a1d 25 |
. . . . . . 7
⊢ (𝑧 ≼ ω → (𝑧 ≺ (ℵ‘𝐴) → ((𝐴 ∈ On ∧ ∅ ∈ 𝐴) → ¬ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧))) |
| 72 | 71 | com3r 87 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → (𝑧 ≼ ω → (𝑧 ≺ (ℵ‘𝐴) → ¬ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧))) |
| 73 | 49, 72 | jaod 860 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → ((ω ≼
𝑧 ∨ 𝑧 ≼ ω) → (𝑧 ≺ (ℵ‘𝐴) → ¬ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧))) |
| 74 | 16, 73 | mpi 20 |
. . . 4
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → (𝑧 ≺ (ℵ‘𝐴) → ¬ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧)) |
| 75 | | breq2 5147 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → ((ℵ‘𝑦) ≺ 𝑥 ↔ (ℵ‘𝑦) ≺ 𝑧)) |
| 76 | 75 | ralbidv 3178 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥 ↔ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧)) |
| 77 | 76 | elrab 3692 |
. . . . . 6
⊢ (𝑧 ∈ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥} ↔ (𝑧 ∈ On ∧ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧)) |
| 78 | 77 | simprbi 496 |
. . . . 5
⊢ (𝑧 ∈ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥} → ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧) |
| 79 | 78 | con3i 154 |
. . . 4
⊢ (¬
∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑧 → ¬ 𝑧 ∈ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥}) |
| 80 | 12, 74, 79 | syl56 36 |
. . 3
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → (𝑧 ∈ (ℵ‘𝐴) → ¬ 𝑧 ∈ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥})) |
| 81 | 80 | ralrimiv 3145 |
. 2
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → ∀𝑧 ∈ (ℵ‘𝐴) ¬ 𝑧 ∈ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥}) |
| 82 | | ssrab2 4080 |
. . 3
⊢ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥} ⊆ On |
| 83 | | oneqmini 6436 |
. . 3
⊢ ({𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥} ⊆ On → (((ℵ‘𝐴) ∈ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥} ∧ ∀𝑧 ∈ (ℵ‘𝐴) ¬ 𝑧 ∈ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥}) → (ℵ‘𝐴) = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥})) |
| 84 | 82, 83 | ax-mp 5 |
. 2
⊢
(((ℵ‘𝐴)
∈ {𝑥 ∈ On ∣
∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥} ∧ ∀𝑧 ∈ (ℵ‘𝐴) ¬ 𝑧 ∈ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥}) → (ℵ‘𝐴) = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥}) |
| 85 | 8, 81, 84 | syl2an2r 685 |
1
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) →
(ℵ‘𝐴) = ∩ {𝑥
∈ On ∣ ∀𝑦
∈ 𝐴
(ℵ‘𝑦) ≺
𝑥}) |