Step |
Hyp |
Ref |
Expression |
0 |
|
cdsr |
|- ||r |
1 |
|
vw |
|- w |
2 |
|
cvv |
|- _V |
3 |
|
vx |
|- x |
4 |
|
vy |
|- y |
5 |
3
|
cv |
|- x |
6 |
|
cbs |
|- Base |
7 |
1
|
cv |
|- w |
8 |
7 6
|
cfv |
|- ( Base ` w ) |
9 |
5 8
|
wcel |
|- x e. ( Base ` w ) |
10 |
|
vz |
|- z |
11 |
10
|
cv |
|- z |
12 |
|
cmulr |
|- .r |
13 |
7 12
|
cfv |
|- ( .r ` w ) |
14 |
11 5 13
|
co |
|- ( z ( .r ` w ) x ) |
15 |
4
|
cv |
|- y |
16 |
14 15
|
wceq |
|- ( z ( .r ` w ) x ) = y |
17 |
16 10 8
|
wrex |
|- E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y |
18 |
9 17
|
wa |
|- ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) |
19 |
18 3 4
|
copab |
|- { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } |
20 |
1 2 19
|
cmpt |
|- ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } ) |
21 |
0 20
|
wceq |
|- ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } ) |