Step | Hyp | Ref
| Expression |
1 | | 0elon 6319 |
. . 3
⊢ ∅
∈ On |
2 | | madeval2 34037 |
. . 3
⊢ (∅
∈ On → ( M ‘∅) = {𝑥 ∈ No
∣ ∃𝑙 ∈
𝒫 ∪ ( M “ ∅)∃𝑟 ∈ 𝒫 ∪ ( M “ ∅)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)}) |
3 | 1, 2 | ax-mp 5 |
. 2
⊢ ( M
‘∅) = {𝑥 ∈
No ∣ ∃𝑙 ∈ 𝒫 ∪ ( M “ ∅)∃𝑟 ∈ 𝒫 ∪ ( M “ ∅)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)} |
4 | | rabeqsn 4602 |
. . 3
⊢ ({𝑥 ∈
No ∣ ∃𝑙
∈ 𝒫 ∪ ( M “ ∅)∃𝑟 ∈ 𝒫 ∪ ( M “ ∅)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)} = { 0s } ↔ ∀𝑥((𝑥 ∈ No
∧ ∃𝑙 ∈
𝒫 ∪ ( M “ ∅)∃𝑟 ∈ 𝒫 ∪ ( M “ ∅)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)) ↔ 𝑥 = 0s )) |
5 | | 0elpw 5278 |
. . . . . . . 8
⊢ ∅
∈ 𝒫 No |
6 | | nulssgt 33992 |
. . . . . . . 8
⊢ (∅
∈ 𝒫 No → ∅ <<s
∅) |
7 | 5, 6 | ax-mp 5 |
. . . . . . 7
⊢ ∅
<<s ∅ |
8 | | ima0 5985 |
. . . . . . . . . . . . 13
⊢ ( M
“ ∅) = ∅ |
9 | 8 | unieqi 4852 |
. . . . . . . . . . . 12
⊢ ∪ ( M “ ∅) = ∪
∅ |
10 | | uni0 4869 |
. . . . . . . . . . . 12
⊢ ∪ ∅ = ∅ |
11 | 9, 10 | eqtri 2766 |
. . . . . . . . . . 11
⊢ ∪ ( M “ ∅) = ∅ |
12 | 11 | pweqi 4551 |
. . . . . . . . . 10
⊢ 𝒫
∪ ( M “ ∅) = 𝒫
∅ |
13 | | pw0 4745 |
. . . . . . . . . 10
⊢ 𝒫
∅ = {∅} |
14 | 12, 13 | eqtri 2766 |
. . . . . . . . 9
⊢ 𝒫
∪ ( M “ ∅) = {∅} |
15 | 14 | rexeqi 3347 |
. . . . . . . 8
⊢
(∃𝑙 ∈
𝒫 ∪ ( M “ ∅)∃𝑟 ∈ 𝒫 ∪ ( M “ ∅)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) ↔ ∃𝑙 ∈ {∅}∃𝑟 ∈ 𝒫 ∪ ( M “ ∅)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)) |
16 | 14 | rexeqi 3347 |
. . . . . . . . 9
⊢
(∃𝑟 ∈
𝒫 ∪ ( M “ ∅)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) ↔ ∃𝑟 ∈ {∅} (𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)) |
17 | 16 | rexbii 3181 |
. . . . . . . 8
⊢
(∃𝑙 ∈
{∅}∃𝑟 ∈
𝒫 ∪ ( M “ ∅)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) ↔ ∃𝑙 ∈ {∅}∃𝑟 ∈ {∅} (𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)) |
18 | | 0ex 5231 |
. . . . . . . . . . 11
⊢ ∅
∈ V |
19 | | breq2 5078 |
. . . . . . . . . . . 12
⊢ (𝑟 = ∅ → (𝑙 <<s 𝑟 ↔ 𝑙 <<s ∅)) |
20 | | oveq2 7283 |
. . . . . . . . . . . . 13
⊢ (𝑟 = ∅ → (𝑙 |s 𝑟) = (𝑙 |s ∅)) |
21 | 20 | eqeq1d 2740 |
. . . . . . . . . . . 12
⊢ (𝑟 = ∅ → ((𝑙 |s 𝑟) = 𝑥 ↔ (𝑙 |s ∅) = 𝑥)) |
22 | 19, 21 | anbi12d 631 |
. . . . . . . . . . 11
⊢ (𝑟 = ∅ → ((𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) ↔ (𝑙 <<s ∅ ∧ (𝑙 |s ∅) = 𝑥))) |
23 | 18, 22 | rexsn 4618 |
. . . . . . . . . 10
⊢
(∃𝑟 ∈
{∅} (𝑙 <<s
𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) ↔ (𝑙 <<s ∅ ∧ (𝑙 |s ∅) = 𝑥)) |
24 | 23 | rexbii 3181 |
. . . . . . . . 9
⊢
(∃𝑙 ∈
{∅}∃𝑟 ∈
{∅} (𝑙 <<s
𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) ↔ ∃𝑙 ∈ {∅} (𝑙 <<s ∅ ∧ (𝑙 |s ∅) = 𝑥)) |
25 | | breq1 5077 |
. . . . . . . . . . 11
⊢ (𝑙 = ∅ → (𝑙 <<s ∅ ↔
∅ <<s ∅)) |
26 | | oveq1 7282 |
. . . . . . . . . . . 12
⊢ (𝑙 = ∅ → (𝑙 |s ∅) = (∅ |s
∅)) |
27 | 26 | eqeq1d 2740 |
. . . . . . . . . . 11
⊢ (𝑙 = ∅ → ((𝑙 |s ∅) = 𝑥 ↔ (∅ |s ∅) =
𝑥)) |
28 | 25, 27 | anbi12d 631 |
. . . . . . . . . 10
⊢ (𝑙 = ∅ → ((𝑙 <<s ∅ ∧ (𝑙 |s ∅) = 𝑥) ↔ (∅ <<s
∅ ∧ (∅ |s ∅) = 𝑥))) |
29 | 18, 28 | rexsn 4618 |
. . . . . . . . 9
⊢
(∃𝑙 ∈
{∅} (𝑙 <<s
∅ ∧ (𝑙 |s
∅) = 𝑥) ↔
(∅ <<s ∅ ∧ (∅ |s ∅) = 𝑥)) |
30 | 24, 29 | bitri 274 |
. . . . . . . 8
⊢
(∃𝑙 ∈
{∅}∃𝑟 ∈
{∅} (𝑙 <<s
𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) ↔ (∅ <<s ∅ ∧
(∅ |s ∅) = 𝑥)) |
31 | 15, 17, 30 | 3bitri 297 |
. . . . . . 7
⊢
(∃𝑙 ∈
𝒫 ∪ ( M “ ∅)∃𝑟 ∈ 𝒫 ∪ ( M “ ∅)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) ↔ (∅ <<s ∅ ∧
(∅ |s ∅) = 𝑥)) |
32 | 7, 31 | mpbiran 706 |
. . . . . 6
⊢
(∃𝑙 ∈
𝒫 ∪ ( M “ ∅)∃𝑟 ∈ 𝒫 ∪ ( M “ ∅)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) ↔ (∅ |s ∅) = 𝑥) |
33 | | df-0s 34018 |
. . . . . . 7
⊢ 0s =
(∅ |s ∅) |
34 | 33 | eqeq1i 2743 |
. . . . . 6
⊢ ( 0s =
𝑥 ↔ (∅ |s
∅) = 𝑥) |
35 | | eqcom 2745 |
. . . . . 6
⊢ ( 0s =
𝑥 ↔ 𝑥 = 0s ) |
36 | 32, 34, 35 | 3bitr2i 299 |
. . . . 5
⊢
(∃𝑙 ∈
𝒫 ∪ ( M “ ∅)∃𝑟 ∈ 𝒫 ∪ ( M “ ∅)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) ↔ 𝑥 = 0s ) |
37 | 36 | anbi2i 623 |
. . . 4
⊢ ((𝑥 ∈
No ∧ ∃𝑙
∈ 𝒫 ∪ ( M “ ∅)∃𝑟 ∈ 𝒫 ∪ ( M “ ∅)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)) ↔ (𝑥 ∈ No
∧ 𝑥 = 0s
)) |
38 | | 0sno 34020 |
. . . . . 6
⊢ 0s
∈ No |
39 | | eleq1 2826 |
. . . . . 6
⊢ (𝑥 = 0s → (𝑥 ∈ No
↔ 0s ∈ No )) |
40 | 38, 39 | mpbiri 257 |
. . . . 5
⊢ (𝑥 = 0s → 𝑥 ∈ No
) |
41 | 40 | pm4.71ri 561 |
. . . 4
⊢ (𝑥 = 0s ↔ (𝑥 ∈ No
∧ 𝑥 = 0s
)) |
42 | 37, 41 | bitr4i 277 |
. . 3
⊢ ((𝑥 ∈
No ∧ ∃𝑙
∈ 𝒫 ∪ ( M “ ∅)∃𝑟 ∈ 𝒫 ∪ ( M “ ∅)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)) ↔ 𝑥 = 0s ) |
43 | 4, 42 | mpgbir 1802 |
. 2
⊢ {𝑥 ∈
No ∣ ∃𝑙
∈ 𝒫 ∪ ( M “ ∅)∃𝑟 ∈ 𝒫 ∪ ( M “ ∅)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)} = { 0s } |
44 | 3, 43 | eqtri 2766 |
1
⊢ ( M
‘∅) = { 0s } |