Step | Hyp | Ref
| Expression |
1 | | alephiso 9601 |
. 2
⊢ ℵ
Isom E , E (On, {𝑥 ∣
(ω ⊆ 𝑥 ∧
(card‘𝑥) = 𝑥)}) |
2 | | iscard4 40717 |
. . . . . . . 8
⊢
((card‘𝑥) =
𝑥 ↔ 𝑥 ∈ ran card) |
3 | 2 | anbi1ci 629 |
. . . . . . 7
⊢ ((ω
⊆ 𝑥 ∧
(card‘𝑥) = 𝑥) ↔ (𝑥 ∈ ran card ∧ ω ⊆ 𝑥)) |
4 | 3 | abbii 2804 |
. . . . . 6
⊢ {𝑥 ∣ (ω ⊆ 𝑥 ∧ (card‘𝑥) = 𝑥)} = {𝑥 ∣ (𝑥 ∈ ran card ∧ ω ⊆ 𝑥)} |
5 | | df-rab 3063 |
. . . . . 6
⊢ {𝑥 ∈ ran card ∣ ω
⊆ 𝑥} = {𝑥 ∣ (𝑥 ∈ ran card ∧ ω ⊆ 𝑥)} |
6 | 4, 5 | eqtr4i 2765 |
. . . . 5
⊢ {𝑥 ∣ (ω ⊆ 𝑥 ∧ (card‘𝑥) = 𝑥)} = {𝑥 ∈ ran card ∣ ω ⊆
𝑥} |
7 | | f1oeq3 6611 |
. . . . 5
⊢ ({𝑥 ∣ (ω ⊆ 𝑥 ∧ (card‘𝑥) = 𝑥)} = {𝑥 ∈ ran card ∣ ω ⊆
𝑥} →
(ℵ:On–1-1-onto→{𝑥 ∣ (ω ⊆ 𝑥 ∧ (card‘𝑥) = 𝑥)} ↔ ℵ:On–1-1-onto→{𝑥 ∈ ran card ∣ ω ⊆
𝑥})) |
8 | 6, 7 | ax-mp 5 |
. . . 4
⊢
(ℵ:On–1-1-onto→{𝑥 ∣ (ω ⊆ 𝑥 ∧ (card‘𝑥) = 𝑥)} ↔ ℵ:On–1-1-onto→{𝑥 ∈ ran card ∣ ω ⊆
𝑥}) |
9 | | alephon 9572 |
. . . . . . . . 9
⊢
(ℵ‘𝑧)
∈ On |
10 | | epelg 5436 |
. . . . . . . . 9
⊢
((ℵ‘𝑧)
∈ On → ((ℵ‘𝑦) E (ℵ‘𝑧) ↔ (ℵ‘𝑦) ∈ (ℵ‘𝑧))) |
11 | 9, 10 | mp1i 13 |
. . . . . . . 8
⊢ ((𝑦 ∈ On ∧ 𝑧 ∈ On) →
((ℵ‘𝑦) E
(ℵ‘𝑧) ↔
(ℵ‘𝑦) ∈
(ℵ‘𝑧))) |
12 | | alephord2 9579 |
. . . . . . . 8
⊢ ((𝑦 ∈ On ∧ 𝑧 ∈ On) → (𝑦 ∈ 𝑧 ↔ (ℵ‘𝑦) ∈ (ℵ‘𝑧))) |
13 | | alephord 9578 |
. . . . . . . 8
⊢ ((𝑦 ∈ On ∧ 𝑧 ∈ On) → (𝑦 ∈ 𝑧 ↔ (ℵ‘𝑦) ≺ (ℵ‘𝑧))) |
14 | 11, 12, 13 | 3bitr2d 310 |
. . . . . . 7
⊢ ((𝑦 ∈ On ∧ 𝑧 ∈ On) →
((ℵ‘𝑦) E
(ℵ‘𝑧) ↔
(ℵ‘𝑦) ≺
(ℵ‘𝑧))) |
15 | 14 | bibi2d 346 |
. . . . . 6
⊢ ((𝑦 ∈ On ∧ 𝑧 ∈ On) → ((𝑦 E 𝑧 ↔ (ℵ‘𝑦) E (ℵ‘𝑧)) ↔ (𝑦 E 𝑧 ↔ (ℵ‘𝑦) ≺ (ℵ‘𝑧)))) |
16 | 15 | ralbidva 3109 |
. . . . 5
⊢ (𝑦 ∈ On → (∀𝑧 ∈ On (𝑦 E 𝑧 ↔ (ℵ‘𝑦) E (ℵ‘𝑧)) ↔ ∀𝑧 ∈ On (𝑦 E 𝑧 ↔ (ℵ‘𝑦) ≺ (ℵ‘𝑧)))) |
17 | 16 | ralbiia 3080 |
. . . 4
⊢
(∀𝑦 ∈ On
∀𝑧 ∈ On (𝑦 E 𝑧 ↔ (ℵ‘𝑦) E (ℵ‘𝑧)) ↔ ∀𝑦 ∈ On ∀𝑧 ∈ On (𝑦 E 𝑧 ↔ (ℵ‘𝑦) ≺ (ℵ‘𝑧))) |
18 | 8, 17 | anbi12i 630 |
. . 3
⊢
((ℵ:On–1-1-onto→{𝑥 ∣ (ω ⊆ 𝑥 ∧ (card‘𝑥) = 𝑥)} ∧ ∀𝑦 ∈ On ∀𝑧 ∈ On (𝑦 E 𝑧 ↔ (ℵ‘𝑦) E (ℵ‘𝑧))) ↔ (ℵ:On–1-1-onto→{𝑥 ∈ ran card ∣ ω ⊆
𝑥} ∧ ∀𝑦 ∈ On ∀𝑧 ∈ On (𝑦 E 𝑧 ↔ (ℵ‘𝑦) ≺ (ℵ‘𝑧)))) |
19 | | df-isom 6349 |
. . 3
⊢ (ℵ
Isom E , E (On, {𝑥 ∣
(ω ⊆ 𝑥 ∧
(card‘𝑥) = 𝑥)}) ↔
(ℵ:On–1-1-onto→{𝑥 ∣ (ω ⊆ 𝑥 ∧ (card‘𝑥) = 𝑥)} ∧ ∀𝑦 ∈ On ∀𝑧 ∈ On (𝑦 E 𝑧 ↔ (ℵ‘𝑦) E (ℵ‘𝑧)))) |
20 | | df-isom 6349 |
. . 3
⊢ (ℵ
Isom E , ≺ (On, {𝑥
∈ ran card ∣ ω ⊆ 𝑥}) ↔ (ℵ:On–1-1-onto→{𝑥 ∈ ran card ∣ ω ⊆
𝑥} ∧ ∀𝑦 ∈ On ∀𝑧 ∈ On (𝑦 E 𝑧 ↔ (ℵ‘𝑦) ≺ (ℵ‘𝑧)))) |
21 | 18, 19, 20 | 3bitr4i 306 |
. 2
⊢ (ℵ
Isom E , E (On, {𝑥 ∣
(ω ⊆ 𝑥 ∧
(card‘𝑥) = 𝑥)}) ↔ ℵ Isom E ,
≺ (On, {𝑥 ∈ ran
card ∣ ω ⊆ 𝑥})) |
22 | 1, 21 | mpbi 233 |
1
⊢ ℵ
Isom E , ≺ (On, {𝑥
∈ ran card ∣ ω ⊆ 𝑥}) |