| Step | Hyp | Ref
| Expression |
| 1 | | 0elon 6438 |
. . 3
⊢ ∅
∈ On |
| 2 | | madeval2 27892 |
. . 3
⊢ (∅
∈ On → ( M ‘∅) = {𝑥 ∈ No
∣ ∃𝑙 ∈
𝒫 ∪ ( M “ ∅)∃𝑟 ∈ 𝒫 ∪ ( M “ ∅)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)}) |
| 3 | 1, 2 | ax-mp 5 |
. 2
⊢ ( M
‘∅) = {𝑥 ∈
No ∣ ∃𝑙 ∈ 𝒫 ∪ ( M “ ∅)∃𝑟 ∈ 𝒫 ∪ ( M “ ∅)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)} |
| 4 | | rabeqsn 4667 |
. . 3
⊢ ({𝑥 ∈
No ∣ ∃𝑙
∈ 𝒫 ∪ ( M “ ∅)∃𝑟 ∈ 𝒫 ∪ ( M “ ∅)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)} = { 0s } ↔ ∀𝑥((𝑥 ∈ No
∧ ∃𝑙 ∈
𝒫 ∪ ( M “ ∅)∃𝑟 ∈ 𝒫 ∪ ( M “ ∅)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)) ↔ 𝑥 = 0s )) |
| 5 | | 0elpw 5356 |
. . . . . . . 8
⊢ ∅
∈ 𝒫 No |
| 6 | | nulssgt 27843 |
. . . . . . . 8
⊢ (∅
∈ 𝒫 No → ∅ <<s
∅) |
| 7 | 5, 6 | ax-mp 5 |
. . . . . . 7
⊢ ∅
<<s ∅ |
| 8 | | ima0 6095 |
. . . . . . . . . . . . 13
⊢ ( M
“ ∅) = ∅ |
| 9 | 8 | unieqi 4919 |
. . . . . . . . . . . 12
⊢ ∪ ( M “ ∅) = ∪
∅ |
| 10 | | uni0 4935 |
. . . . . . . . . . . 12
⊢ ∪ ∅ = ∅ |
| 11 | 9, 10 | eqtri 2765 |
. . . . . . . . . . 11
⊢ ∪ ( M “ ∅) = ∅ |
| 12 | 11 | pweqi 4616 |
. . . . . . . . . 10
⊢ 𝒫
∪ ( M “ ∅) = 𝒫
∅ |
| 13 | | pw0 4812 |
. . . . . . . . . 10
⊢ 𝒫
∅ = {∅} |
| 14 | 12, 13 | eqtri 2765 |
. . . . . . . . 9
⊢ 𝒫
∪ ( M “ ∅) = {∅} |
| 15 | 14 | rexeqi 3325 |
. . . . . . . 8
⊢
(∃𝑙 ∈
𝒫 ∪ ( M “ ∅)∃𝑟 ∈ 𝒫 ∪ ( M “ ∅)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) ↔ ∃𝑙 ∈ {∅}∃𝑟 ∈ 𝒫 ∪ ( M “ ∅)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)) |
| 16 | 14 | rexeqi 3325 |
. . . . . . . . 9
⊢
(∃𝑟 ∈
𝒫 ∪ ( M “ ∅)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) ↔ ∃𝑟 ∈ {∅} (𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)) |
| 17 | 16 | rexbii 3094 |
. . . . . . . 8
⊢
(∃𝑙 ∈
{∅}∃𝑟 ∈
𝒫 ∪ ( M “ ∅)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) ↔ ∃𝑙 ∈ {∅}∃𝑟 ∈ {∅} (𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)) |
| 18 | | 0ex 5307 |
. . . . . . . . . . 11
⊢ ∅
∈ V |
| 19 | | breq2 5147 |
. . . . . . . . . . . 12
⊢ (𝑟 = ∅ → (𝑙 <<s 𝑟 ↔ 𝑙 <<s ∅)) |
| 20 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑟 = ∅ → (𝑙 |s 𝑟) = (𝑙 |s ∅)) |
| 21 | 20 | eqeq1d 2739 |
. . . . . . . . . . . 12
⊢ (𝑟 = ∅ → ((𝑙 |s 𝑟) = 𝑥 ↔ (𝑙 |s ∅) = 𝑥)) |
| 22 | 19, 21 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝑟 = ∅ → ((𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) ↔ (𝑙 <<s ∅ ∧ (𝑙 |s ∅) = 𝑥))) |
| 23 | 18, 22 | rexsn 4682 |
. . . . . . . . . 10
⊢
(∃𝑟 ∈
{∅} (𝑙 <<s
𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) ↔ (𝑙 <<s ∅ ∧ (𝑙 |s ∅) = 𝑥)) |
| 24 | 23 | rexbii 3094 |
. . . . . . . . 9
⊢
(∃𝑙 ∈
{∅}∃𝑟 ∈
{∅} (𝑙 <<s
𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) ↔ ∃𝑙 ∈ {∅} (𝑙 <<s ∅ ∧ (𝑙 |s ∅) = 𝑥)) |
| 25 | | breq1 5146 |
. . . . . . . . . . 11
⊢ (𝑙 = ∅ → (𝑙 <<s ∅ ↔
∅ <<s ∅)) |
| 26 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑙 = ∅ → (𝑙 |s ∅) = (∅ |s
∅)) |
| 27 | 26 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ (𝑙 = ∅ → ((𝑙 |s ∅) = 𝑥 ↔ (∅ |s ∅) =
𝑥)) |
| 28 | 25, 27 | anbi12d 632 |
. . . . . . . . . 10
⊢ (𝑙 = ∅ → ((𝑙 <<s ∅ ∧ (𝑙 |s ∅) = 𝑥) ↔ (∅ <<s
∅ ∧ (∅ |s ∅) = 𝑥))) |
| 29 | 18, 28 | rexsn 4682 |
. . . . . . . . 9
⊢
(∃𝑙 ∈
{∅} (𝑙 <<s
∅ ∧ (𝑙 |s
∅) = 𝑥) ↔
(∅ <<s ∅ ∧ (∅ |s ∅) = 𝑥)) |
| 30 | 24, 29 | bitri 275 |
. . . . . . . 8
⊢
(∃𝑙 ∈
{∅}∃𝑟 ∈
{∅} (𝑙 <<s
𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) ↔ (∅ <<s ∅ ∧
(∅ |s ∅) = 𝑥)) |
| 31 | 15, 17, 30 | 3bitri 297 |
. . . . . . 7
⊢
(∃𝑙 ∈
𝒫 ∪ ( M “ ∅)∃𝑟 ∈ 𝒫 ∪ ( M “ ∅)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) ↔ (∅ <<s ∅ ∧
(∅ |s ∅) = 𝑥)) |
| 32 | 7, 31 | mpbiran 709 |
. . . . . 6
⊢
(∃𝑙 ∈
𝒫 ∪ ( M “ ∅)∃𝑟 ∈ 𝒫 ∪ ( M “ ∅)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥) ↔ (∅ |s ∅) = 𝑥) |
| 33 | | df-0s 27869 |
. . . . . . 7
⊢
0s = (∅ |s ∅) |
| 34 | 33 | eqeq1i 2742 |
. . . . . 6
⊢ (
0s = 𝑥 ↔
(∅ |s ∅) = 𝑥) |
| 35 | | eqcom 2744 |
. . . . . 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 27871 |
. . . . . 6
⊢
0s ∈ No |
| 39 | | eleq1 2829 |
. . . . . 6
⊢ (𝑥 = 0s → (𝑥 ∈
No ↔ 0s ∈ No
)) |
| 40 | 38, 39 | mpbiri 258 |
. . . . 5
⊢ (𝑥 = 0s → 𝑥 ∈
No ) |
| 41 | 40 | pm4.71ri 560 |
. . . 4
⊢ (𝑥 = 0s ↔ (𝑥 ∈
No ∧ 𝑥 =
0s )) |
| 42 | 37, 41 | bitr4i 278 |
. . 3
⊢ ((𝑥 ∈
No ∧ ∃𝑙
∈ 𝒫 ∪ ( M “ ∅)∃𝑟 ∈ 𝒫 ∪ ( M “ ∅)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)) ↔ 𝑥 = 0s ) |
| 43 | 4, 42 | mpgbir 1799 |
. 2
⊢ {𝑥 ∈
No ∣ ∃𝑙
∈ 𝒫 ∪ ( M “ ∅)∃𝑟 ∈ 𝒫 ∪ ( M “ ∅)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑥)} = { 0s } |
| 44 | 3, 43 | eqtri 2765 |
1
⊢ ( M
‘∅) = { 0s } |