| Step |
Hyp |
Ref |
Expression |
| 1 |
|
jf1o |
Could not format _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On : No typesetting found for |- _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On with typecode |- |
| 2 |
|
f1ocnvdm |
Could not format ( ( _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On /\ A e. On ) -> ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) ) : No typesetting found for |- ( ( _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On /\ A e. On ) -> ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) ) with typecode |- |
| 3 |
1 2
|
mpan |
Could not format ( A e. On -> ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) ) : No typesetting found for |- ( A e. On -> ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) ) with typecode |- |
| 4 |
|
2fveq3 |
Could not format ( x = A -> ( 1st ` ( `' _J ` x ) ) = ( 1st ` ( `' _J ` A ) ) ) : No typesetting found for |- ( x = A -> ( 1st ` ( `' _J ` x ) ) = ( 1st ` ( `' _J ` A ) ) ) with typecode |- |
| 5 |
4
|
fveq2d |
Could not format ( x = A -> ( 1st ` ( 1st ` ( `' _J ` x ) ) ) = ( 1st ` ( 1st ` ( `' _J ` A ) ) ) ) : No typesetting found for |- ( x = A -> ( 1st ` ( 1st ` ( `' _J ` x ) ) ) = ( 1st ` ( 1st ` ( `' _J ` A ) ) ) ) with typecode |- |
| 6 |
|
dfk12 |
Could not format _K1 = ( x e. On |-> ( 1st ` ( 1st ` ( `' _J ` x ) ) ) ) : No typesetting found for |- _K1 = ( x e. On |-> ( 1st ` ( 1st ` ( `' _J ` x ) ) ) ) with typecode |- |
| 7 |
|
fvex |
Could not format ( 1st ` ( 1st ` ( `' _J ` A ) ) ) e. _V : No typesetting found for |- ( 1st ` ( 1st ` ( `' _J ` A ) ) ) e. _V with typecode |- |
| 8 |
5 6 7
|
fvmpt |
Could not format ( A e. On -> ( _K1 ` A ) = ( 1st ` ( 1st ` ( `' _J ` A ) ) ) ) : No typesetting found for |- ( A e. On -> ( _K1 ` A ) = ( 1st ` ( 1st ` ( `' _J ` A ) ) ) ) with typecode |- |
| 9 |
8
|
eqcomd |
Could not format ( A e. On -> ( 1st ` ( 1st ` ( `' _J ` A ) ) ) = ( _K1 ` A ) ) : No typesetting found for |- ( A e. On -> ( 1st ` ( 1st ` ( `' _J ` A ) ) ) = ( _K1 ` A ) ) with typecode |- |
| 10 |
4
|
fveq2d |
Could not format ( x = A -> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) = ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) ) : No typesetting found for |- ( x = A -> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) = ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) ) with typecode |- |
| 11 |
|
dfk22 |
Could not format _K2 = ( x e. On |-> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) : No typesetting found for |- _K2 = ( x e. On |-> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) with typecode |- |
| 12 |
|
fvex |
Could not format ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) e. _V : No typesetting found for |- ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) e. _V with typecode |- |
| 13 |
10 11 12
|
fvmpt |
Could not format ( A e. On -> ( _K2 ` A ) = ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) ) : No typesetting found for |- ( A e. On -> ( _K2 ` A ) = ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) ) with typecode |- |
| 14 |
13
|
eqcomd |
Could not format ( A e. On -> ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) = ( _K2 ` A ) ) : No typesetting found for |- ( A e. On -> ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) = ( _K2 ` A ) ) with typecode |- |
| 15 |
|
2fveq3 |
Could not format ( x = A -> ( 2nd ` ( `' _J ` x ) ) = ( 2nd ` ( `' _J ` A ) ) ) : No typesetting found for |- ( x = A -> ( 2nd ` ( `' _J ` x ) ) = ( 2nd ` ( `' _J ` A ) ) ) with typecode |- |
| 16 |
|
dfk32 |
Could not format _K3 = ( x e. On |-> ( 2nd ` ( `' _J ` x ) ) ) : No typesetting found for |- _K3 = ( x e. On |-> ( 2nd ` ( `' _J ` x ) ) ) with typecode |- |
| 17 |
|
fvex |
Could not format ( 2nd ` ( `' _J ` A ) ) e. _V : No typesetting found for |- ( 2nd ` ( `' _J ` A ) ) e. _V with typecode |- |
| 18 |
15 16 17
|
fvmpt |
Could not format ( A e. On -> ( _K3 ` A ) = ( 2nd ` ( `' _J ` A ) ) ) : No typesetting found for |- ( A e. On -> ( _K3 ` A ) = ( 2nd ` ( `' _J ` A ) ) ) with typecode |- |
| 19 |
18
|
eqcomd |
Could not format ( A e. On -> ( 2nd ` ( `' _J ` A ) ) = ( _K3 ` A ) ) : No typesetting found for |- ( A e. On -> ( 2nd ` ( `' _J ` A ) ) = ( _K3 ` A ) ) with typecode |- |
| 20 |
9 14 19
|
3jca |
Could not format ( A e. On -> ( ( 1st ` ( 1st ` ( `' _J ` A ) ) ) = ( _K1 ` A ) /\ ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) = ( _K2 ` A ) /\ ( 2nd ` ( `' _J ` A ) ) = ( _K3 ` A ) ) ) : No typesetting found for |- ( A e. On -> ( ( 1st ` ( 1st ` ( `' _J ` A ) ) ) = ( _K1 ` A ) /\ ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) = ( _K2 ` A ) /\ ( 2nd ` ( `' _J ` A ) ) = ( _K3 ` A ) ) ) with typecode |- |
| 21 |
3 20
|
jca |
Could not format ( A e. On -> ( ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) /\ ( ( 1st ` ( 1st ` ( `' _J ` A ) ) ) = ( _K1 ` A ) /\ ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) = ( _K2 ` A ) /\ ( 2nd ` ( `' _J ` A ) ) = ( _K3 ` A ) ) ) ) : No typesetting found for |- ( A e. On -> ( ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) /\ ( ( 1st ` ( 1st ` ( `' _J ` A ) ) ) = ( _K1 ` A ) /\ ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) = ( _K2 ` A ) /\ ( 2nd ` ( `' _J ` A ) ) = ( _K3 ` A ) ) ) ) with typecode |- |
| 22 |
|
k1on |
Could not format ( _K1 ` A ) e. On : No typesetting found for |- ( _K1 ` A ) e. On with typecode |- |
| 23 |
|
k2on |
Could not format ( _K2 ` A ) e. On : No typesetting found for |- ( _K2 ` A ) e. On with typecode |- |
| 24 |
|
k39o |
Could not format ( _K3 ` A ) e. 9o : No typesetting found for |- ( _K3 ` A ) e. 9o with typecode |- |
| 25 |
|
el2xptp0 |
Could not format ( ( ( _K1 ` A ) e. On /\ ( _K2 ` A ) e. On /\ ( _K3 ` A ) e. 9o ) -> ( ( ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) /\ ( ( 1st ` ( 1st ` ( `' _J ` A ) ) ) = ( _K1 ` A ) /\ ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) = ( _K2 ` A ) /\ ( 2nd ` ( `' _J ` A ) ) = ( _K3 ` A ) ) ) <-> ( `' _J ` A ) = <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) ) : No typesetting found for |- ( ( ( _K1 ` A ) e. On /\ ( _K2 ` A ) e. On /\ ( _K3 ` A ) e. 9o ) -> ( ( ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) /\ ( ( 1st ` ( 1st ` ( `' _J ` A ) ) ) = ( _K1 ` A ) /\ ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) = ( _K2 ` A ) /\ ( 2nd ` ( `' _J ` A ) ) = ( _K3 ` A ) ) ) <-> ( `' _J ` A ) = <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) ) with typecode |- |
| 26 |
22 23 24 25
|
mp3an |
Could not format ( ( ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) /\ ( ( 1st ` ( 1st ` ( `' _J ` A ) ) ) = ( _K1 ` A ) /\ ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) = ( _K2 ` A ) /\ ( 2nd ` ( `' _J ` A ) ) = ( _K3 ` A ) ) ) <-> ( `' _J ` A ) = <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) : No typesetting found for |- ( ( ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) /\ ( ( 1st ` ( 1st ` ( `' _J ` A ) ) ) = ( _K1 ` A ) /\ ( 2nd ` ( 1st ` ( `' _J ` A ) ) ) = ( _K2 ` A ) /\ ( 2nd ` ( `' _J ` A ) ) = ( _K3 ` A ) ) ) <-> ( `' _J ` A ) = <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) with typecode |- |
| 27 |
21 26
|
sylib |
Could not format ( A e. On -> ( `' _J ` A ) = <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) : No typesetting found for |- ( A e. On -> ( `' _J ` A ) = <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) with typecode |- |
| 28 |
27 3
|
eqeltrrd |
Could not format ( A e. On -> <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. e. ( ( On X. On ) X. 9o ) ) : No typesetting found for |- ( A e. On -> <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. e. ( ( On X. On ) X. 9o ) ) with typecode |- |
| 29 |
|
f1ocnvfvb |
Could not format ( ( _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On /\ <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. e. ( ( On X. On ) X. 9o ) /\ A e. On ) -> ( ( _J ` <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) = A <-> ( `' _J ` A ) = <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) ) : No typesetting found for |- ( ( _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On /\ <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. e. ( ( On X. On ) X. 9o ) /\ A e. On ) -> ( ( _J ` <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) = A <-> ( `' _J ` A ) = <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) ) with typecode |- |
| 30 |
1 29
|
mp3an1 |
Could not format ( ( <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. e. ( ( On X. On ) X. 9o ) /\ A e. On ) -> ( ( _J ` <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) = A <-> ( `' _J ` A ) = <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) ) : No typesetting found for |- ( ( <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. e. ( ( On X. On ) X. 9o ) /\ A e. On ) -> ( ( _J ` <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) = A <-> ( `' _J ` A ) = <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) ) with typecode |- |
| 31 |
28 30
|
mpancom |
Could not format ( A e. On -> ( ( _J ` <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) = A <-> ( `' _J ` A ) = <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) ) : No typesetting found for |- ( A e. On -> ( ( _J ` <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) = A <-> ( `' _J ` A ) = <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) ) with typecode |- |
| 32 |
27 31
|
mpbird |
Could not format ( A e. On -> ( _J ` <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) = A ) : No typesetting found for |- ( A e. On -> ( _J ` <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) = A ) with typecode |- |
| 33 |
32
|
eqcomd |
Could not format ( A e. On -> A = ( _J ` <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) ) : No typesetting found for |- ( A e. On -> A = ( _J ` <. ( _K1 ` A ) , ( _K2 ` A ) , ( _K3 ` A ) >. ) ) with typecode |- |