Detailed syntax breakdown of Definition df-tx
Step | Hyp | Ref
| Expression |
1 | | ctx 22720 |
. 2
class
×t |
2 | | vr |
. . 3
setvar 𝑟 |
3 | | vs |
. . 3
setvar 𝑠 |
4 | | cvv 3433 |
. . 3
class
V |
5 | | vx |
. . . . . 6
setvar 𝑥 |
6 | | vy |
. . . . . 6
setvar 𝑦 |
7 | 2 | cv 1538 |
. . . . . 6
class 𝑟 |
8 | 3 | cv 1538 |
. . . . . 6
class 𝑠 |
9 | 5 | cv 1538 |
. . . . . . 7
class 𝑥 |
10 | 6 | cv 1538 |
. . . . . . 7
class 𝑦 |
11 | 9, 10 | cxp 5588 |
. . . . . 6
class (𝑥 × 𝑦) |
12 | 5, 6, 7, 8, 11 | cmpo 7286 |
. . . . 5
class (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)) |
13 | 12 | crn 5591 |
. . . 4
class ran
(𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)) |
14 | | ctg 17157 |
. . . 4
class
topGen |
15 | 13, 14 | cfv 6437 |
. . 3
class
(topGen‘ran (𝑥
∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦))) |
16 | 2, 3, 4, 4, 15 | cmpo 7286 |
. 2
class (𝑟 ∈ V, 𝑠 ∈ V ↦ (topGen‘ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)))) |
17 | 1, 16 | wceq 1539 |
1
wff
×t = (𝑟
∈ V, 𝑠 ∈ V
↦ (topGen‘ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)))) |