Step | Hyp | Ref
| Expression |
1 | | cU |
. . 3
class 𝑈 |
2 | | cN |
. . 3
class 𝑁 |
3 | 1, 2 | cfinxp 36259 |
. 2
class (𝑈↑↑𝑁) |
4 | | com 7854 |
. . . . 5
class
ω |
5 | 2, 4 | wcel 2106 |
. . . 4
wff 𝑁 ∈ ω |
6 | | c0 4322 |
. . . . 5
class
∅ |
7 | | vn |
. . . . . . . 8
setvar 𝑛 |
8 | | vx |
. . . . . . . 8
setvar 𝑥 |
9 | | cvv 3474 |
. . . . . . . 8
class
V |
10 | 7 | cv 1540 |
. . . . . . . . . . 11
class 𝑛 |
11 | | c1o 8458 |
. . . . . . . . . . 11
class
1o |
12 | 10, 11 | wceq 1541 |
. . . . . . . . . 10
wff 𝑛 =
1o |
13 | 8 | cv 1540 |
. . . . . . . . . . 11
class 𝑥 |
14 | 13, 1 | wcel 2106 |
. . . . . . . . . 10
wff 𝑥 ∈ 𝑈 |
15 | 12, 14 | wa 396 |
. . . . . . . . 9
wff (𝑛 = 1o ∧ 𝑥 ∈ 𝑈) |
16 | 9, 1 | cxp 5674 |
. . . . . . . . . . 11
class (V
× 𝑈) |
17 | 13, 16 | wcel 2106 |
. . . . . . . . . 10
wff 𝑥 ∈ (V × 𝑈) |
18 | 10 | cuni 4908 |
. . . . . . . . . . 11
class ∪ 𝑛 |
19 | | c1st 7972 |
. . . . . . . . . . . 12
class
1st |
20 | 13, 19 | cfv 6543 |
. . . . . . . . . . 11
class
(1st ‘𝑥) |
21 | 18, 20 | cop 4634 |
. . . . . . . . . 10
class
⟨∪ 𝑛, (1st ‘𝑥)⟩ |
22 | 10, 13 | cop 4634 |
. . . . . . . . . 10
class
⟨𝑛, 𝑥⟩ |
23 | 17, 21, 22 | cif 4528 |
. . . . . . . . 9
class if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛,
(1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩) |
24 | 15, 6, 23 | cif 4528 |
. . . . . . . 8
class if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)) |
25 | 7, 8, 4, 9, 24 | cmpo 7410 |
. . . . . . 7
class (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))) |
26 | | vy |
. . . . . . . . 9
setvar 𝑦 |
27 | 26 | cv 1540 |
. . . . . . . 8
class 𝑦 |
28 | 2, 27 | cop 4634 |
. . . . . . 7
class
⟨𝑁, 𝑦⟩ |
29 | 25, 28 | crdg 8408 |
. . . . . 6
class
rec((𝑛 ∈
ω, 𝑥 ∈ V ↦
if((𝑛 = 1o ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩) |
30 | 2, 29 | cfv 6543 |
. . . . 5
class
(rec((𝑛 ∈
ω, 𝑥 ∈ V ↦
if((𝑛 = 1o ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁) |
31 | 6, 30 | wceq 1541 |
. . . 4
wff ∅ =
(rec((𝑛 ∈ ω,
𝑥 ∈ V ↦
if((𝑛 = 1o ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁) |
32 | 5, 31 | wa 396 |
. . 3
wff (𝑁 ∈ ω ∧ ∅ =
(rec((𝑛 ∈ ω,
𝑥 ∈ V ↦
if((𝑛 = 1o ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁)) |
33 | 32, 26 | cab 2709 |
. 2
class {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))} |
34 | 3, 33 | wceq 1541 |
1
wff (𝑈↑↑𝑁) = {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))} |