Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1030.1 |
|
2 |
|
bnj1030.2 |
|
3 |
|
bnj1030.3 |
|
4 |
|
bnj1030.4 |
|
5 |
|
bnj1030.5 |
|
6 |
|
bnj1030.6 |
|
7 |
|
bnj1030.7 |
|
8 |
|
bnj1030.8 |
|
9 |
|
bnj1030.9 |
|
10 |
|
bnj1030.10 |
|
11 |
|
bnj1030.11 |
Could not format ( ph' <-> [. j / i ]. ph ) : No typesetting found for |- ( ph' <-> [. j / i ]. ph ) with typecode |- |
12 |
|
bnj1030.12 |
Could not format ( ps' <-> [. j / i ]. ps ) : No typesetting found for |- ( ps' <-> [. j / i ]. ps ) with typecode |- |
13 |
|
bnj1030.13 |
Could not format ( ch' <-> [. j / i ]. ch ) : No typesetting found for |- ( ch' <-> [. j / i ]. ch ) with typecode |- |
14 |
|
bnj1030.14 |
Could not format ( th' <-> [. j / i ]. th ) : No typesetting found for |- ( th' <-> [. j / i ]. th ) with typecode |- |
15 |
|
bnj1030.15 |
Could not format ( ta' <-> [. j / i ]. ta ) : No typesetting found for |- ( ta' <-> [. j / i ]. ta ) with typecode |- |
16 |
|
bnj1030.16 |
Could not format ( ze' <-> [. j / i ]. ze ) : No typesetting found for |- ( ze' <-> [. j / i ]. ze ) with typecode |- |
17 |
|
bnj1030.17 |
Could not format ( et' <-> [. j / i ]. et ) : No typesetting found for |- ( et' <-> [. j / i ]. et ) with typecode |- |
18 |
|
bnj1030.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 |- |
19 |
|
bnj1030.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 |- |
20 |
|
19.23vv |
|
21 |
20
|
albii |
|
22 |
|
19.23v |
|
23 |
21 22
|
bitri |
|
24 |
7
|
bnj1071 |
|
25 |
3 24
|
bnj769 |
|
26 |
25
|
bnj707 |
|
27 |
2 8 9 17
|
bnj1123 |
Could not format ( et' <-> ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B ) ) : No typesetting found for |- ( et' <-> ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B ) ) with typecode |- |
28 |
2 3 5 7 18 19 27
|
bnj1118 |
Could not format E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f ` i ) C_ B ) : No typesetting found for |- E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f ` i ) C_ B ) with typecode |- |
29 |
1 3 5
|
bnj1097 |
Could not format ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f ` i ) C_ B ) : No typesetting found for |- ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f ` i ) C_ B ) with typecode |- |
30 |
28 29
|
bnj1109 |
Could not format E. j ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( f ` i ) C_ B ) : No typesetting found for |- E. j ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( f ` i ) C_ B ) with typecode |- |
31 |
30 2 3
|
bnj1093 |
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 |- |
32 |
9 10 17 18 19 31
|
bnj1090 |
|
33 |
|
vex |
|
34 |
33 10
|
bnj110 |
|
35 |
26 32 34
|
syl2anc |
|
36 |
4 5 3 6 9 35 8
|
bnj1121 |
|
37 |
36
|
gen2 |
|
38 |
23 37
|
mpgbi |
|
39 |
1 2 3 4 5 6 7 8 38
|
bnj1034 |
|