Step |
Hyp |
Ref |
Expression |
0 |
|
ctx |
|- tX |
1 |
|
vr |
|- r |
2 |
|
cvv |
|- _V |
3 |
|
vs |
|- s |
4 |
|
ctg |
|- topGen |
5 |
|
vx |
|- x |
6 |
1
|
cv |
|- r |
7 |
|
vy |
|- y |
8 |
3
|
cv |
|- s |
9 |
5
|
cv |
|- x |
10 |
7
|
cv |
|- y |
11 |
9 10
|
cxp |
|- ( x X. y ) |
12 |
5 7 6 8 11
|
cmpo |
|- ( x e. r , y e. s |-> ( x X. y ) ) |
13 |
12
|
crn |
|- ran ( x e. r , y e. s |-> ( x X. y ) ) |
14 |
13 4
|
cfv |
|- ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) |
15 |
1 3 2 2 14
|
cmpo |
|- ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) ) |
16 |
0 15
|
wceq |
|- tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) ) |