Step |
Hyp |
Ref |
Expression |
1 |
|
bnj149.1 |
Could not format ( th1 <-> ( ( R _FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( th1 <-> ( ( R _FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |- |
2 |
|
bnj149.2 |
Could not format ( ze0 <-> ( f Fn 1o /\ ph' /\ ps' ) ) : No typesetting found for |- ( ze0 <-> ( f Fn 1o /\ ph' /\ ps' ) ) with typecode |- |
3 |
|
bnj149.3 |
Could not format ( ze1 <-> [. g / f ]. ze0 ) : No typesetting found for |- ( ze1 <-> [. g / f ]. ze0 ) with typecode |- |
4 |
|
bnj149.4 |
Could not format ( ph1 <-> [. g / f ]. ph' ) : No typesetting found for |- ( ph1 <-> [. g / f ]. ph' ) with typecode |- |
5 |
|
bnj149.5 |
Could not format ( ps1 <-> [. g / f ]. ps' ) : No typesetting found for |- ( ps1 <-> [. g / f ]. ps' ) with typecode |- |
6 |
|
bnj149.6 |
Could not format ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode |- |
7 |
|
simpr1 |
Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> f Fn 1o ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> f Fn 1o ) with typecode |- |
8 |
|
df1o2 |
|
9 |
8
|
fneq2i |
|
10 |
7 9
|
sylib |
Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> f Fn { (/) } ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> f Fn { (/) } ) with typecode |- |
11 |
|
simpr2 |
Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> ph' ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> ph' ) with typecode |- |
12 |
11 6
|
sylib |
Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> ( f ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode |- |
13 |
|
fvex |
|
14 |
13
|
elsn |
|
15 |
12 14
|
sylibr |
Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> ( f ` (/) ) e. { _pred ( x , A , R ) } ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> ( f ` (/) ) e. { _pred ( x , A , R ) } ) with typecode |- |
16 |
|
0ex |
|
17 |
|
fveq2 |
|
18 |
17
|
eleq1d |
|
19 |
16 18
|
ralsn |
|
20 |
15 19
|
sylibr |
Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> A. g e. { (/) } ( f ` g ) e. { _pred ( x , A , R ) } ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> A. g e. { (/) } ( f ` g ) e. { _pred ( x , A , R ) } ) with typecode |- |
21 |
|
ffnfv |
|
22 |
10 20 21
|
sylanbrc |
Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> f : { (/) } --> { _pred ( x , A , R ) } ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> f : { (/) } --> { _pred ( x , A , R ) } ) with typecode |- |
23 |
|
bnj93 |
|
24 |
23
|
adantr |
Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> _pred ( x , A , R ) e. _V ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> _pred ( x , A , R ) e. _V ) with typecode |- |
25 |
|
fsng |
|
26 |
16 24 25
|
sylancr |
Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> ( f : { (/) } --> { _pred ( x , A , R ) } <-> f = { <. (/) , _pred ( x , A , R ) >. } ) ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> ( f : { (/) } --> { _pred ( x , A , R ) } <-> f = { <. (/) , _pred ( x , A , R ) >. } ) ) with typecode |- |
27 |
22 26
|
mpbid |
Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> f = { <. (/) , _pred ( x , A , R ) >. } ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> f = { <. (/) , _pred ( x , A , R ) >. } ) with typecode |- |
28 |
27
|
ex |
Could not format ( ( R _FrSe A /\ x e. A ) -> ( ( f Fn 1o /\ ph' /\ ps' ) -> f = { <. (/) , _pred ( x , A , R ) >. } ) ) : No typesetting found for |- ( ( R _FrSe A /\ x e. A ) -> ( ( f Fn 1o /\ ph' /\ ps' ) -> f = { <. (/) , _pred ( x , A , R ) >. } ) ) with typecode |- |
29 |
28
|
alrimiv |
Could not format ( ( R _FrSe A /\ x e. A ) -> A. f ( ( f Fn 1o /\ ph' /\ ps' ) -> f = { <. (/) , _pred ( x , A , R ) >. } ) ) : No typesetting found for |- ( ( R _FrSe A /\ x e. A ) -> A. f ( ( f Fn 1o /\ ph' /\ ps' ) -> f = { <. (/) , _pred ( x , A , R ) >. } ) ) with typecode |- |
30 |
|
mo2icl |
Could not format ( A. f ( ( f Fn 1o /\ ph' /\ ps' ) -> f = { <. (/) , _pred ( x , A , R ) >. } ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) : No typesetting found for |- ( A. f ( ( f Fn 1o /\ ph' /\ ps' ) -> f = { <. (/) , _pred ( x , A , R ) >. } ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) with typecode |- |
31 |
29 30
|
syl |
Could not format ( ( R _FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) : No typesetting found for |- ( ( R _FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) with typecode |- |
32 |
31 1
|
mpbir |
Could not format th1 : No typesetting found for |- th1 with typecode |- |