Step |
Hyp |
Ref |
Expression |
1 |
|
ovex |
Could not format ( 2 -aryF X ) e. _V : No typesetting found for |- ( 2 -aryF X ) e. _V with typecode |- |
2 |
1
|
mptex |
Could not format ( f e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) ) e. _V : No typesetting found for |- ( f e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) ) e. _V with typecode |- |
3 |
2
|
a1i |
Could not format ( X e. _V -> ( f e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) ) e. _V ) : No typesetting found for |- ( X e. _V -> ( f e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) ) e. _V ) with typecode |- |
4 |
|
eqid |
Could not format ( f e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) ) = ( f e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) ) : No typesetting found for |- ( f e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) ) = ( f e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) ) with typecode |- |
5 |
4
|
2arymaptf1o |
Could not format ( X e. _V -> ( f e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) ) : ( 2 -aryF X ) -1-1-onto-> ( X ^m ( X X. X ) ) ) : No typesetting found for |- ( X e. _V -> ( f e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) ) : ( 2 -aryF X ) -1-1-onto-> ( X ^m ( X X. X ) ) ) with typecode |- |
6 |
|
f1oeq1 |
Could not format ( h = ( f e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) ) -> ( h : ( 2 -aryF X ) -1-1-onto-> ( X ^m ( X X. X ) ) <-> ( f e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) ) : ( 2 -aryF X ) -1-1-onto-> ( X ^m ( X X. X ) ) ) ) : No typesetting found for |- ( h = ( f e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) ) -> ( h : ( 2 -aryF X ) -1-1-onto-> ( X ^m ( X X. X ) ) <-> ( f e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) ) : ( 2 -aryF X ) -1-1-onto-> ( X ^m ( X X. X ) ) ) ) with typecode |- |
7 |
3 5 6
|
spcedv |
Could not format ( X e. _V -> E. h h : ( 2 -aryF X ) -1-1-onto-> ( X ^m ( X X. X ) ) ) : No typesetting found for |- ( X e. _V -> E. h h : ( 2 -aryF X ) -1-1-onto-> ( X ^m ( X X. X ) ) ) with typecode |- |
8 |
|
bren |
Could not format ( ( 2 -aryF X ) ~~ ( X ^m ( X X. X ) ) <-> E. h h : ( 2 -aryF X ) -1-1-onto-> ( X ^m ( X X. X ) ) ) : No typesetting found for |- ( ( 2 -aryF X ) ~~ ( X ^m ( X X. X ) ) <-> E. h h : ( 2 -aryF X ) -1-1-onto-> ( X ^m ( X X. X ) ) ) with typecode |- |
9 |
7 8
|
sylibr |
Could not format ( X e. _V -> ( 2 -aryF X ) ~~ ( X ^m ( X X. X ) ) ) : No typesetting found for |- ( X e. _V -> ( 2 -aryF X ) ~~ ( X ^m ( X X. X ) ) ) with typecode |- |
10 |
|
0ex |
|
11 |
10
|
enref |
|
12 |
11
|
a1i |
|
13 |
|
df-naryf |
Could not format -aryF = ( n e. NN0 , x e. _V |-> ( x ^m ( x ^m ( 0 ..^ n ) ) ) ) : No typesetting found for |- -aryF = ( n e. NN0 , x e. _V |-> ( x ^m ( x ^m ( 0 ..^ n ) ) ) ) with typecode |- |
14 |
13
|
reldmmpo |
Could not format Rel dom -aryF : No typesetting found for |- Rel dom -aryF with typecode |- |
15 |
14
|
ovprc2 |
Could not format ( -. X e. _V -> ( 2 -aryF X ) = (/) ) : No typesetting found for |- ( -. X e. _V -> ( 2 -aryF X ) = (/) ) with typecode |- |
16 |
|
reldmmap |
|
17 |
16
|
ovprc1 |
|
18 |
12 15 17
|
3brtr4d |
Could not format ( -. X e. _V -> ( 2 -aryF X ) ~~ ( X ^m ( X X. X ) ) ) : No typesetting found for |- ( -. X e. _V -> ( 2 -aryF X ) ~~ ( X ^m ( X X. X ) ) ) with typecode |- |
19 |
9 18
|
pm2.61i |
Could not format ( 2 -aryF X ) ~~ ( X ^m ( X X. X ) ) : No typesetting found for |- ( 2 -aryF X ) ~~ ( X ^m ( X X. X ) ) with typecode |- |