Detailed syntax breakdown of Definition df-finxp
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cU | . . 3
class 𝑈 | 
| 2 |  | cN | . . 3
class 𝑁 | 
| 3 | 1, 2 | cfinxp 37384 | . 2
class (𝑈↑↑𝑁) | 
| 4 |  | com 7887 | . . . . 5
class
ω | 
| 5 | 2, 4 | wcel 2108 | . . . 4
wff 𝑁 ∈ ω | 
| 6 |  | c0 4333 | . . . . 5
class
∅ | 
| 7 |  | vn | . . . . . . . 8
setvar 𝑛 | 
| 8 |  | vx | . . . . . . . 8
setvar 𝑥 | 
| 9 |  | cvv 3480 | . . . . . . . 8
class
V | 
| 10 | 7 | cv 1539 | . . . . . . . . . . 11
class 𝑛 | 
| 11 |  | c1o 8499 | . . . . . . . . . . 11
class
1o | 
| 12 | 10, 11 | wceq 1540 | . . . . . . . . . 10
wff 𝑛 =
1o | 
| 13 | 8 | cv 1539 | . . . . . . . . . . 11
class 𝑥 | 
| 14 | 13, 1 | wcel 2108 | . . . . . . . . . 10
wff 𝑥 ∈ 𝑈 | 
| 15 | 12, 14 | wa 395 | . . . . . . . . 9
wff (𝑛 = 1o ∧ 𝑥 ∈ 𝑈) | 
| 16 | 9, 1 | cxp 5683 | . . . . . . . . . . 11
class (V
× 𝑈) | 
| 17 | 13, 16 | wcel 2108 | . . . . . . . . . 10
wff 𝑥 ∈ (V × 𝑈) | 
| 18 | 10 | cuni 4907 | . . . . . . . . . . 11
class ∪ 𝑛 | 
| 19 |  | c1st 8012 | . . . . . . . . . . . 12
class
1st | 
| 20 | 13, 19 | cfv 6561 | . . . . . . . . . . 11
class
(1st ‘𝑥) | 
| 21 | 18, 20 | cop 4632 | . . . . . . . . . 10
class
〈∪ 𝑛, (1st ‘𝑥)〉 | 
| 22 | 10, 13 | cop 4632 | . . . . . . . . . 10
class
〈𝑛, 𝑥〉 | 
| 23 | 17, 21, 22 | cif 4525 | . . . . . . . . 9
class if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) | 
| 24 | 15, 6, 23 | cif 4525 | . . . . . . . 8
class if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) | 
| 25 | 7, 8, 4, 9, 24 | cmpo 7433 | . . . . . . 7
class (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) | 
| 26 |  | vy | . . . . . . . . 9
setvar 𝑦 | 
| 27 | 26 | cv 1539 | . . . . . . . 8
class 𝑦 | 
| 28 | 2, 27 | cop 4632 | . . . . . . 7
class
〈𝑁, 𝑦〉 | 
| 29 | 25, 28 | crdg 8449 | . . . . . 6
class
rec((𝑛 ∈
ω, 𝑥 ∈ V ↦
if((𝑛 = 1o ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈𝑁, 𝑦〉) | 
| 30 | 2, 29 | cfv 6561 | . . . . 5
class
(rec((𝑛 ∈
ω, 𝑥 ∈ V ↦
if((𝑛 = 1o ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈𝑁, 𝑦〉)‘𝑁) | 
| 31 | 6, 30 | wceq 1540 | . . . 4
wff ∅ =
(rec((𝑛 ∈ ω,
𝑥 ∈ V ↦
if((𝑛 = 1o ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈𝑁, 𝑦〉)‘𝑁) | 
| 32 | 5, 31 | wa 395 | . . 3
wff (𝑁 ∈ ω ∧ ∅ =
(rec((𝑛 ∈ ω,
𝑥 ∈ V ↦
if((𝑛 = 1o ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈𝑁, 𝑦〉)‘𝑁)) | 
| 33 | 32, 26 | cab 2714 | . 2
class {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈𝑁, 𝑦〉)‘𝑁))} | 
| 34 | 3, 33 | wceq 1540 | 1
wff (𝑈↑↑𝑁) = {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈𝑁, 𝑦〉)‘𝑁))} |