Step |
Hyp |
Ref |
Expression |
0 |
|
csx |
⊢ ×s |
1 |
|
vs |
⊢ 𝑠 |
2 |
|
cvv |
⊢ V |
3 |
|
vt |
⊢ 𝑡 |
4 |
|
csigagen |
⊢ sigaGen |
5 |
|
vx |
⊢ 𝑥 |
6 |
1
|
cv |
⊢ 𝑠 |
7 |
|
vy |
⊢ 𝑦 |
8 |
3
|
cv |
⊢ 𝑡 |
9 |
5
|
cv |
⊢ 𝑥 |
10 |
7
|
cv |
⊢ 𝑦 |
11 |
9 10
|
cxp |
⊢ ( 𝑥 × 𝑦 ) |
12 |
5 7 6 8 11
|
cmpo |
⊢ ( 𝑥 ∈ 𝑠 , 𝑦 ∈ 𝑡 ↦ ( 𝑥 × 𝑦 ) ) |
13 |
12
|
crn |
⊢ ran ( 𝑥 ∈ 𝑠 , 𝑦 ∈ 𝑡 ↦ ( 𝑥 × 𝑦 ) ) |
14 |
13 4
|
cfv |
⊢ ( sigaGen ‘ ran ( 𝑥 ∈ 𝑠 , 𝑦 ∈ 𝑡 ↦ ( 𝑥 × 𝑦 ) ) ) |
15 |
1 3 2 2 14
|
cmpo |
⊢ ( 𝑠 ∈ V , 𝑡 ∈ V ↦ ( sigaGen ‘ ran ( 𝑥 ∈ 𝑠 , 𝑦 ∈ 𝑡 ↦ ( 𝑥 × 𝑦 ) ) ) ) |
16 |
0 15
|
wceq |
⊢ ×s = ( 𝑠 ∈ V , 𝑡 ∈ V ↦ ( sigaGen ‘ ran ( 𝑥 ∈ 𝑠 , 𝑦 ∈ 𝑡 ↦ ( 𝑥 × 𝑦 ) ) ) ) |