Step |
Hyp |
Ref |
Expression |
0 |
|
csx |
|- sX |
1 |
|
vs |
|- s |
2 |
|
cvv |
|- _V |
3 |
|
vt |
|- t |
4 |
|
csigagen |
|- sigaGen |
5 |
|
vx |
|- x |
6 |
1
|
cv |
|- s |
7 |
|
vy |
|- y |
8 |
3
|
cv |
|- t |
9 |
5
|
cv |
|- x |
10 |
7
|
cv |
|- y |
11 |
9 10
|
cxp |
|- ( x X. y ) |
12 |
5 7 6 8 11
|
cmpo |
|- ( x e. s , y e. t |-> ( x X. y ) ) |
13 |
12
|
crn |
|- ran ( x e. s , y e. t |-> ( x X. y ) ) |
14 |
13 4
|
cfv |
|- ( sigaGen ` ran ( x e. s , y e. t |-> ( x X. y ) ) ) |
15 |
1 3 2 2 14
|
cmpo |
|- ( s e. _V , t e. _V |-> ( sigaGen ` ran ( x e. s , y e. t |-> ( x X. y ) ) ) ) |
16 |
0 15
|
wceq |
|- sX = ( s e. _V , t e. _V |-> ( sigaGen ` ran ( x e. s , y e. t |-> ( x X. y ) ) ) ) |