Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1371.1 |
|
2 |
|
bnj1371.2 |
|
3 |
|
bnj1371.3 |
|
4 |
|
bnj1371.4 |
|
5 |
|
bnj1371.5 |
|
6 |
|
bnj1371.6 |
|
7 |
|
bnj1371.7 |
|
8 |
|
bnj1371.8 |
Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |- |
9 |
|
bnj1371.9 |
Could not format H = { f | E. y e. _pred ( x , A , R ) ta' } : No typesetting found for |- H = { f | E. y e. _pred ( x , A , R ) ta' } with typecode |- |
10 |
|
bnj1371.10 |
|
11 |
|
bnj1371.11 |
Could not format ( ta' <-> ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) : No typesetting found for |- ( ta' <-> ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) with typecode |- |
12 |
9
|
bnj1436 |
Could not format ( f e. H -> E. y e. _pred ( x , A , R ) ta' ) : No typesetting found for |- ( f e. H -> E. y e. _pred ( x , A , R ) ta' ) with typecode |- |
13 |
|
rexex |
Could not format ( E. y e. _pred ( x , A , R ) ta' -> E. y ta' ) : No typesetting found for |- ( E. y e. _pred ( x , A , R ) ta' -> E. y ta' ) with typecode |- |
14 |
12 13
|
syl |
Could not format ( f e. H -> E. y ta' ) : No typesetting found for |- ( f e. H -> E. y ta' ) with typecode |- |
15 |
11
|
exbii |
Could not format ( E. y ta' <-> E. y ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) : No typesetting found for |- ( E. y ta' <-> E. y ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) with typecode |- |
16 |
14 15
|
sylib |
|
17 |
|
exsimpl |
|
18 |
16 17
|
syl |
|
19 |
3
|
abeq2i |
|
20 |
19
|
bnj1238 |
|
21 |
|
fnfun |
|
22 |
20 21
|
bnj31 |
|
23 |
22
|
bnj1265 |
|
24 |
18 23
|
bnj593 |
|
25 |
24
|
bnj937 |
|