Step | Hyp | Ref
| Expression |
1 | | df-om 7808 |
. 2
⊢ ω =
{𝑥 ∈ On ∣
∀𝑧(Lim 𝑧 → 𝑥 ∈ 𝑧)} |
2 | | vex 3452 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ V |
3 | | limelon 6386 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ V ∧ Lim 𝑧) → 𝑧 ∈ On) |
4 | 2, 3 | mpan 689 |
. . . . . . . . . 10
⊢ (Lim
𝑧 → 𝑧 ∈ On) |
5 | 4 | pm4.71ri 562 |
. . . . . . . . 9
⊢ (Lim
𝑧 ↔ (𝑧 ∈ On ∧ Lim 𝑧)) |
6 | 5 | imbi1i 350 |
. . . . . . . 8
⊢ ((Lim
𝑧 → 𝑥 ∈ 𝑧) ↔ ((𝑧 ∈ On ∧ Lim 𝑧) → 𝑥 ∈ 𝑧)) |
7 | | impexp 452 |
. . . . . . . 8
⊢ (((𝑧 ∈ On ∧ Lim 𝑧) → 𝑥 ∈ 𝑧) ↔ (𝑧 ∈ On → (Lim 𝑧 → 𝑥 ∈ 𝑧))) |
8 | | con34b 316 |
. . . . . . . . . 10
⊢ ((Lim
𝑧 → 𝑥 ∈ 𝑧) ↔ (¬ 𝑥 ∈ 𝑧 → ¬ Lim 𝑧)) |
9 | | ibar 530 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ On → (¬ Lim
𝑧 ↔ (𝑧 ∈ On ∧ ¬ Lim 𝑧))) |
10 | 9 | imbi2d 341 |
. . . . . . . . . 10
⊢ (𝑧 ∈ On → ((¬ 𝑥 ∈ 𝑧 → ¬ Lim 𝑧) ↔ (¬ 𝑥 ∈ 𝑧 → (𝑧 ∈ On ∧ ¬ Lim 𝑧)))) |
11 | 8, 10 | bitrid 283 |
. . . . . . . . 9
⊢ (𝑧 ∈ On → ((Lim 𝑧 → 𝑥 ∈ 𝑧) ↔ (¬ 𝑥 ∈ 𝑧 → (𝑧 ∈ On ∧ ¬ Lim 𝑧)))) |
12 | 11 | pm5.74i 271 |
. . . . . . . 8
⊢ ((𝑧 ∈ On → (Lim 𝑧 → 𝑥 ∈ 𝑧)) ↔ (𝑧 ∈ On → (¬ 𝑥 ∈ 𝑧 → (𝑧 ∈ On ∧ ¬ Lim 𝑧)))) |
13 | 6, 7, 12 | 3bitri 297 |
. . . . . . 7
⊢ ((Lim
𝑧 → 𝑥 ∈ 𝑧) ↔ (𝑧 ∈ On → (¬ 𝑥 ∈ 𝑧 → (𝑧 ∈ On ∧ ¬ Lim 𝑧)))) |
14 | | onsssuc 6412 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ On ∧ 𝑥 ∈ On) → (𝑧 ⊆ 𝑥 ↔ 𝑧 ∈ suc 𝑥)) |
15 | | ontri1 6356 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ On ∧ 𝑥 ∈ On) → (𝑧 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝑧)) |
16 | 14, 15 | bitr3d 281 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ On ∧ 𝑥 ∈ On) → (𝑧 ∈ suc 𝑥 ↔ ¬ 𝑥 ∈ 𝑧)) |
17 | 16 | ancoms 460 |
. . . . . . . . 9
⊢ ((𝑥 ∈ On ∧ 𝑧 ∈ On) → (𝑧 ∈ suc 𝑥 ↔ ¬ 𝑥 ∈ 𝑧)) |
18 | | limeq 6334 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → (Lim 𝑦 ↔ Lim 𝑧)) |
19 | 18 | notbid 318 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (¬ Lim 𝑦 ↔ ¬ Lim 𝑧)) |
20 | 19 | elrab 3650 |
. . . . . . . . . 10
⊢ (𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦} ↔ (𝑧 ∈ On ∧ ¬ Lim 𝑧)) |
21 | 20 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑥 ∈ On ∧ 𝑧 ∈ On) → (𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦} ↔ (𝑧 ∈ On ∧ ¬ Lim 𝑧))) |
22 | 17, 21 | imbi12d 345 |
. . . . . . . 8
⊢ ((𝑥 ∈ On ∧ 𝑧 ∈ On) → ((𝑧 ∈ suc 𝑥 → 𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦}) ↔ (¬ 𝑥 ∈ 𝑧 → (𝑧 ∈ On ∧ ¬ Lim 𝑧)))) |
23 | 22 | pm5.74da 803 |
. . . . . . 7
⊢ (𝑥 ∈ On → ((𝑧 ∈ On → (𝑧 ∈ suc 𝑥 → 𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦})) ↔ (𝑧 ∈ On → (¬ 𝑥 ∈ 𝑧 → (𝑧 ∈ On ∧ ¬ Lim 𝑧))))) |
24 | 13, 23 | bitr4id 290 |
. . . . . 6
⊢ (𝑥 ∈ On → ((Lim 𝑧 → 𝑥 ∈ 𝑧) ↔ (𝑧 ∈ On → (𝑧 ∈ suc 𝑥 → 𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦})))) |
25 | | impexp 452 |
. . . . . . 7
⊢ (((𝑧 ∈ On ∧ 𝑧 ∈ suc 𝑥) → 𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦}) ↔ (𝑧 ∈ On → (𝑧 ∈ suc 𝑥 → 𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦}))) |
26 | | simpr 486 |
. . . . . . . . 9
⊢ ((𝑧 ∈ On ∧ 𝑧 ∈ suc 𝑥) → 𝑧 ∈ suc 𝑥) |
27 | | onsuc 7751 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ On → suc 𝑥 ∈ On) |
28 | | onelon 6347 |
. . . . . . . . . . . 12
⊢ ((suc
𝑥 ∈ On ∧ 𝑧 ∈ suc 𝑥) → 𝑧 ∈ On) |
29 | 28 | ex 414 |
. . . . . . . . . . 11
⊢ (suc
𝑥 ∈ On → (𝑧 ∈ suc 𝑥 → 𝑧 ∈ On)) |
30 | 27, 29 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ On → (𝑧 ∈ suc 𝑥 → 𝑧 ∈ On)) |
31 | 30 | ancrd 553 |
. . . . . . . . 9
⊢ (𝑥 ∈ On → (𝑧 ∈ suc 𝑥 → (𝑧 ∈ On ∧ 𝑧 ∈ suc 𝑥))) |
32 | 26, 31 | impbid2 225 |
. . . . . . . 8
⊢ (𝑥 ∈ On → ((𝑧 ∈ On ∧ 𝑧 ∈ suc 𝑥) ↔ 𝑧 ∈ suc 𝑥)) |
33 | 32 | imbi1d 342 |
. . . . . . 7
⊢ (𝑥 ∈ On → (((𝑧 ∈ On ∧ 𝑧 ∈ suc 𝑥) → 𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦}) ↔ (𝑧 ∈ suc 𝑥 → 𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦}))) |
34 | 25, 33 | bitr3id 285 |
. . . . . 6
⊢ (𝑥 ∈ On → ((𝑧 ∈ On → (𝑧 ∈ suc 𝑥 → 𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦})) ↔ (𝑧 ∈ suc 𝑥 → 𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦}))) |
35 | 24, 34 | bitrd 279 |
. . . . 5
⊢ (𝑥 ∈ On → ((Lim 𝑧 → 𝑥 ∈ 𝑧) ↔ (𝑧 ∈ suc 𝑥 → 𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦}))) |
36 | 35 | albidv 1924 |
. . . 4
⊢ (𝑥 ∈ On → (∀𝑧(Lim 𝑧 → 𝑥 ∈ 𝑧) ↔ ∀𝑧(𝑧 ∈ suc 𝑥 → 𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦}))) |
37 | | dfss2 3935 |
. . . 4
⊢ (suc
𝑥 ⊆ {𝑦 ∈ On ∣ ¬ Lim
𝑦} ↔ ∀𝑧(𝑧 ∈ suc 𝑥 → 𝑧 ∈ {𝑦 ∈ On ∣ ¬ Lim 𝑦})) |
38 | 36, 37 | bitr4di 289 |
. . 3
⊢ (𝑥 ∈ On → (∀𝑧(Lim 𝑧 → 𝑥 ∈ 𝑧) ↔ suc 𝑥 ⊆ {𝑦 ∈ On ∣ ¬ Lim 𝑦})) |
39 | 38 | rabbiia 3414 |
. 2
⊢ {𝑥 ∈ On ∣ ∀𝑧(Lim 𝑧 → 𝑥 ∈ 𝑧)} = {𝑥 ∈ On ∣ suc 𝑥 ⊆ {𝑦 ∈ On ∣ ¬ Lim 𝑦}} |
40 | 1, 39 | eqtri 2765 |
1
⊢ ω =
{𝑥 ∈ On ∣ suc
𝑥 ⊆ {𝑦 ∈ On ∣ ¬ Lim
𝑦}} |