Step |
Hyp |
Ref |
Expression |
0 |
|
cspc |
|- Lambda |
1 |
|
vt |
|- t |
2 |
|
chba |
|- ~H |
3 |
|
cmap |
|- ^m |
4 |
2 2 3
|
co |
|- ( ~H ^m ~H ) |
5 |
|
vx |
|- x |
6 |
|
cc |
|- CC |
7 |
1
|
cv |
|- t |
8 |
|
chod |
|- -op |
9 |
5
|
cv |
|- x |
10 |
|
chot |
|- .op |
11 |
|
cid |
|- _I |
12 |
11 2
|
cres |
|- ( _I |` ~H ) |
13 |
9 12 10
|
co |
|- ( x .op ( _I |` ~H ) ) |
14 |
7 13 8
|
co |
|- ( t -op ( x .op ( _I |` ~H ) ) ) |
15 |
2 2 14
|
wf1 |
|- ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H |
16 |
15
|
wn |
|- -. ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H |
17 |
16 5 6
|
crab |
|- { x e. CC | -. ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H } |
18 |
1 4 17
|
cmpt |
|- ( t e. ( ~H ^m ~H ) |-> { x e. CC | -. ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H } ) |
19 |
0 18
|
wceq |
|- Lambda = ( t e. ( ~H ^m ~H ) |-> { x e. CC | -. ( t -op ( x .op ( _I |` ~H ) ) ) : ~H -1-1-> ~H } ) |