Detailed syntax breakdown of Definition df-tx
Step | Hyp | Ref
| Expression |
1 | | ctx 22311 |
. 2
class
×t |
2 | | vr |
. . 3
setvar 𝑟 |
3 | | vs |
. . 3
setvar 𝑠 |
4 | | cvv 3398 |
. . 3
class
V |
5 | | vx |
. . . . . 6
setvar 𝑥 |
6 | | vy |
. . . . . 6
setvar 𝑦 |
7 | 2 | cv 1541 |
. . . . . 6
class 𝑟 |
8 | 3 | cv 1541 |
. . . . . 6
class 𝑠 |
9 | 5 | cv 1541 |
. . . . . . 7
class 𝑥 |
10 | 6 | cv 1541 |
. . . . . . 7
class 𝑦 |
11 | 9, 10 | cxp 5523 |
. . . . . 6
class (𝑥 × 𝑦) |
12 | 5, 6, 7, 8, 11 | cmpo 7172 |
. . . . 5
class (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)) |
13 | 12 | crn 5526 |
. . . 4
class ran
(𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)) |
14 | | ctg 16814 |
. . . 4
class
topGen |
15 | 13, 14 | cfv 6339 |
. . 3
class
(topGen‘ran (𝑥
∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦))) |
16 | 2, 3, 4, 4, 15 | cmpo 7172 |
. 2
class (𝑟 ∈ V, 𝑠 ∈ V ↦ (topGen‘ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)))) |
17 | 1, 16 | wceq 1542 |
1
wff
×t = (𝑟
∈ V, 𝑠 ∈ V
↦ (topGen‘ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)))) |