| Step |
Hyp |
Ref |
Expression |
| 1 |
|
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 |- |
| 2 |
|
dfk32 |
Could not format _K3 = ( x e. On |-> ( 2nd ` ( `' _J ` x ) ) ) : No typesetting found for |- _K3 = ( x e. On |-> ( 2nd ` ( `' _J ` x ) ) ) with typecode |- |
| 3 |
|
fvex |
Could not format ( 2nd ` ( `' _J ` A ) ) e. _V : No typesetting found for |- ( 2nd ` ( `' _J ` A ) ) e. _V with typecode |- |
| 4 |
1 2 3
|
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 |- |
| 5 |
|
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 |- |
| 6 |
|
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 |- |
| 7 |
5 6
|
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 |- |
| 8 |
|
xp2nd |
Could not format ( ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) -> ( 2nd ` ( `' _J ` A ) ) e. 9o ) : No typesetting found for |- ( ( `' _J ` A ) e. ( ( On X. On ) X. 9o ) -> ( 2nd ` ( `' _J ` A ) ) e. 9o ) with typecode |- |
| 9 |
7 8
|
syl |
Could not format ( A e. On -> ( 2nd ` ( `' _J ` A ) ) e. 9o ) : No typesetting found for |- ( A e. On -> ( 2nd ` ( `' _J ` A ) ) e. 9o ) with typecode |- |
| 10 |
4 9
|
eqeltrd |
Could not format ( A e. On -> ( _K3 ` A ) e. 9o ) : No typesetting found for |- ( A e. On -> ( _K3 ` A ) e. 9o ) with typecode |- |
| 11 |
2
|
fvmptndm |
Could not format ( -. A e. On -> ( _K3 ` A ) = (/) ) : No typesetting found for |- ( -. A e. On -> ( _K3 ` A ) = (/) ) with typecode |- |
| 12 |
|
df-9o |
Could not format 9o = suc 8o : No typesetting found for |- 9o = suc 8o with typecode |- |
| 13 |
|
nsuceq0 |
Could not format suc 8o =/= (/) : No typesetting found for |- suc 8o =/= (/) with typecode |- |
| 14 |
12 13
|
eqnetri |
Could not format 9o =/= (/) : No typesetting found for |- 9o =/= (/) with typecode |- |
| 15 |
|
9on |
Could not format 9o e. On : No typesetting found for |- 9o e. On with typecode |- |
| 16 |
|
on0eln0 |
Could not format ( 9o e. On -> ( (/) e. 9o <-> 9o =/= (/) ) ) : No typesetting found for |- ( 9o e. On -> ( (/) e. 9o <-> 9o =/= (/) ) ) with typecode |- |
| 17 |
15 16
|
ax-mp |
Could not format ( (/) e. 9o <-> 9o =/= (/) ) : No typesetting found for |- ( (/) e. 9o <-> 9o =/= (/) ) with typecode |- |
| 18 |
14 17
|
mpbir |
Could not format (/) e. 9o : No typesetting found for |- (/) e. 9o with typecode |- |
| 19 |
11 18
|
eqeltrdi |
Could not format ( -. A e. On -> ( _K3 ` A ) e. 9o ) : No typesetting found for |- ( -. A e. On -> ( _K3 ` A ) e. 9o ) with typecode |- |
| 20 |
10 19
|
pm2.61i |
Could not format ( _K3 ` A ) e. 9o : No typesetting found for |- ( _K3 ` A ) e. 9o with typecode |- |