Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1090.9 |
|
2 |
|
bnj1090.10 |
|
3 |
|
bnj1090.17 |
Could not format ( et' <-> [. j / i ]. et ) : No typesetting found for |- ( et' <-> [. j / i ]. et ) with typecode |- |
4 |
|
bnj1090.18 |
Could not format ( si <-> ( ( j e. n /\ j _E i ) -> et' ) ) : No typesetting found for |- ( si <-> ( ( j e. n /\ j _E i ) -> et' ) ) with typecode |- |
5 |
|
bnj1090.19 |
Could not format ( ph0 <-> ( i e. n /\ si /\ f e. K /\ i e. dom f ) ) : No typesetting found for |- ( ph0 <-> ( i e. n /\ si /\ f e. K /\ i e. dom f ) ) with typecode |- |
6 |
|
bnj1090.28 |
Could not format ( ( th /\ ta /\ ch /\ ze ) -> A. i E. j ( ph0 -> ( f ` i ) C_ B ) ) : No typesetting found for |- ( ( th /\ ta /\ ch /\ ze ) -> A. i E. j ( ph0 -> ( f ` i ) C_ B ) ) with typecode |- |
7 |
|
impexp |
|
8 |
7
|
exbii |
|
9 |
4
|
imbi1i |
Could not format ( ( si -> et ) <-> ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) : No typesetting found for |- ( ( si -> et ) <-> ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) with typecode |- |
10 |
9
|
exbii |
Could not format ( E. j ( si -> et ) <-> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) : No typesetting found for |- ( E. j ( si -> et ) <-> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) with typecode |- |
11 |
10
|
imbi2i |
Could not format ( ( i e. n -> E. j ( si -> et ) ) <-> ( i e. n -> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) ) : No typesetting found for |- ( ( i e. n -> E. j ( si -> et ) ) <-> ( i e. n -> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) ) with typecode |- |
12 |
|
19.37v |
|
13 |
2
|
bnj115 |
|
14 |
3
|
imbi2i |
Could not format ( ( ( j e. n /\ j _E i ) -> et' ) <-> ( ( j e. n /\ j _E i ) -> [. j / i ]. et ) ) : No typesetting found for |- ( ( ( j e. n /\ j _E i ) -> et' ) <-> ( ( j e. n /\ j _E i ) -> [. j / i ]. et ) ) with typecode |- |
15 |
14
|
albii |
Could not format ( A. j ( ( j e. n /\ j _E i ) -> et' ) <-> A. j ( ( j e. n /\ j _E i ) -> [. j / i ]. et ) ) : No typesetting found for |- ( A. j ( ( j e. n /\ j _E i ) -> et' ) <-> A. j ( ( j e. n /\ j _E i ) -> [. j / i ]. et ) ) with typecode |- |
16 |
13 15
|
bitr4i |
Could not format ( rh <-> A. j ( ( j e. n /\ j _E i ) -> et' ) ) : No typesetting found for |- ( rh <-> A. j ( ( j e. n /\ j _E i ) -> et' ) ) with typecode |- |
17 |
16
|
imbi1i |
Could not format ( ( rh -> et ) <-> ( A. j ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) : No typesetting found for |- ( ( rh -> et ) <-> ( A. j ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) with typecode |- |
18 |
|
19.36v |
Could not format ( E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) <-> ( A. j ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) : No typesetting found for |- ( E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) <-> ( A. j ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) with typecode |- |
19 |
17 18
|
bitr4i |
Could not format ( ( rh -> et ) <-> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) : No typesetting found for |- ( ( rh -> et ) <-> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) with typecode |- |
20 |
19
|
imbi2i |
Could not format ( ( i e. n -> ( rh -> et ) ) <-> ( i e. n -> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) ) : No typesetting found for |- ( ( i e. n -> ( rh -> et ) ) <-> ( i e. n -> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) ) with typecode |- |
21 |
11 12 20
|
3bitr4i |
|
22 |
8 21
|
bitr2i |
|
23 |
|
impexp |
|
24 |
|
bnj256 |
|
25 |
24
|
imbi1i |
|
26 |
1
|
imbi2i |
|
27 |
23 25 26
|
3bitr4i |
|
28 |
22 27
|
bnj133 |
|
29 |
28
|
albii |
|
30 |
|
df-ral |
|
31 |
5
|
imbi1i |
Could not format ( ( ph0 -> ( f ` i ) C_ B ) <-> ( ( i e. n /\ si /\ f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) ) : No typesetting found for |- ( ( ph0 -> ( f ` i ) C_ B ) <-> ( ( i e. n /\ si /\ f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) ) with typecode |- |
32 |
31
|
exbii |
Could not format ( E. j ( ph0 -> ( f ` i ) C_ B ) <-> E. j ( ( i e. n /\ si /\ f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) ) : No typesetting found for |- ( E. j ( ph0 -> ( f ` i ) C_ B ) <-> E. j ( ( i e. n /\ si /\ f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) ) with typecode |- |
33 |
32
|
albii |
Could not format ( A. i E. j ( ph0 -> ( f ` i ) C_ B ) <-> A. i E. j ( ( i e. n /\ si /\ f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) ) : No typesetting found for |- ( A. i E. j ( ph0 -> ( f ` i ) C_ B ) <-> A. i E. j ( ( i e. n /\ si /\ f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) ) with typecode |- |
34 |
29 30 33
|
3bitr4i |
Could not format ( A. i e. n ( rh -> et ) <-> A. i E. j ( ph0 -> ( f ` i ) C_ B ) ) : No typesetting found for |- ( A. i e. n ( rh -> et ) <-> A. i E. j ( ph0 -> ( f ` i ) C_ B ) ) with typecode |- |
35 |
6 34
|
sylibr |
|