Step |
Hyp |
Ref |
Expression |
0 |
|
cdjaN |
|- vA |
1 |
|
vk |
|- k |
2 |
|
cvv |
|- _V |
3 |
|
vw |
|- w |
4 |
|
clh |
|- LHyp |
5 |
1
|
cv |
|- k |
6 |
5 4
|
cfv |
|- ( LHyp ` k ) |
7 |
|
vx |
|- x |
8 |
|
cltrn |
|- LTrn |
9 |
5 8
|
cfv |
|- ( LTrn ` k ) |
10 |
3
|
cv |
|- w |
11 |
10 9
|
cfv |
|- ( ( LTrn ` k ) ` w ) |
12 |
11
|
cpw |
|- ~P ( ( LTrn ` k ) ` w ) |
13 |
|
vy |
|- y |
14 |
|
cocaN |
|- ocA |
15 |
5 14
|
cfv |
|- ( ocA ` k ) |
16 |
10 15
|
cfv |
|- ( ( ocA ` k ) ` w ) |
17 |
7
|
cv |
|- x |
18 |
17 16
|
cfv |
|- ( ( ( ocA ` k ) ` w ) ` x ) |
19 |
13
|
cv |
|- y |
20 |
19 16
|
cfv |
|- ( ( ( ocA ` k ) ` w ) ` y ) |
21 |
18 20
|
cin |
|- ( ( ( ( ocA ` k ) ` w ) ` x ) i^i ( ( ( ocA ` k ) ` w ) ` y ) ) |
22 |
21 16
|
cfv |
|- ( ( ( ocA ` k ) ` w ) ` ( ( ( ( ocA ` k ) ` w ) ` x ) i^i ( ( ( ocA ` k ) ` w ) ` y ) ) ) |
23 |
7 13 12 12 22
|
cmpo |
|- ( x e. ~P ( ( LTrn ` k ) ` w ) , y e. ~P ( ( LTrn ` k ) ` w ) |-> ( ( ( ocA ` k ) ` w ) ` ( ( ( ( ocA ` k ) ` w ) ` x ) i^i ( ( ( ocA ` k ) ` w ) ` y ) ) ) ) |
24 |
3 6 23
|
cmpt |
|- ( w e. ( LHyp ` k ) |-> ( x e. ~P ( ( LTrn ` k ) ` w ) , y e. ~P ( ( LTrn ` k ) ` w ) |-> ( ( ( ocA ` k ) ` w ) ` ( ( ( ( ocA ` k ) ` w ) ` x ) i^i ( ( ( ocA ` k ) ` w ) ` y ) ) ) ) ) |
25 |
1 2 24
|
cmpt |
|- ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ~P ( ( LTrn ` k ) ` w ) , y e. ~P ( ( LTrn ` k ) ` w ) |-> ( ( ( ocA ` k ) ` w ) ` ( ( ( ( ocA ` k ) ` w ) ` x ) i^i ( ( ( ocA ` k ) ` w ) ` y ) ) ) ) ) ) |
26 |
0 25
|
wceq |
|- vA = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ~P ( ( LTrn ` k ) ` w ) , y e. ~P ( ( LTrn ` k ) ` w ) |-> ( ( ( ocA ` k ) ` w ) ` ( ( ( ( ocA ` k ) ` w ) ` x ) i^i ( ( ( ocA ` k ) ` w ) ` y ) ) ) ) ) ) |