Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1489.1 |
|
2 |
|
bnj1489.2 |
|
3 |
|
bnj1489.3 |
|
4 |
|
bnj1489.4 |
|
5 |
|
bnj1489.5 |
|
6 |
|
bnj1489.6 |
|
7 |
|
bnj1489.7 |
|
8 |
|
bnj1489.8 |
Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |- |
9 |
|
bnj1489.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 |
|
bnj1489.10 |
|
11 |
|
bnj1489.11 |
|
12 |
|
bnj1489.12 |
|
13 |
|
bnj1364 |
|
14 |
|
df-bnj13 |
|
15 |
13 14
|
sylib |
|
16 |
6 15
|
bnj832 |
|
17 |
7 16
|
bnj835 |
|
18 |
5 7
|
bnj1212 |
|
19 |
17 18
|
bnj1294 |
|
20 |
|
nfv |
|
21 |
|
nfv |
|
22 |
|
nfra1 |
|
23 |
20 21 22
|
nf3an |
|
24 |
7 23
|
nfxfr |
|
25 |
6
|
simplbi |
|
26 |
7 25
|
bnj835 |
|
27 |
26
|
adantr |
|
28 |
1 2 3 4 5 6 7 8
|
bnj1388 |
Could not format ( ch -> A. y e. _pred ( x , A , R ) E. f ta' ) : No typesetting found for |- ( ch -> A. y e. _pred ( x , A , R ) E. f ta' ) with typecode |- |
29 |
28
|
r19.21bi |
Could not format ( ( ch /\ y e. _pred ( x , A , R ) ) -> E. f ta' ) : No typesetting found for |- ( ( ch /\ y e. _pred ( x , A , R ) ) -> E. f ta' ) with typecode |- |
30 |
|
nfv |
|
31 |
|
nfsbc1v |
|
32 |
8 31
|
nfxfr |
Could not format F/ x ta' : No typesetting found for |- F/ x ta' with typecode |- |
33 |
32
|
nfex |
Could not format F/ x E. f ta' : No typesetting found for |- F/ x E. f ta' with typecode |- |
34 |
30 33
|
nfan |
Could not format F/ x ( R _FrSe A /\ E. f ta' ) : No typesetting found for |- F/ x ( R _FrSe A /\ E. f ta' ) with typecode |- |
35 |
32
|
nfeuw |
Could not format F/ x E! f ta' : No typesetting found for |- F/ x E! f ta' with typecode |- |
36 |
34 35
|
nfim |
Could not format F/ x ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) : No typesetting found for |- F/ x ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) with typecode |- |
37 |
|
sneq |
|
38 |
|
bnj1318 |
|
39 |
37 38
|
uneq12d |
|
40 |
39
|
eqeq2d |
|
41 |
40
|
anbi2d |
|
42 |
1 2 3 4 8
|
bnj1373 |
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 |- |
43 |
41 42
|
bitr4di |
Could not format ( x = y -> ( ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> ta' ) ) : No typesetting found for |- ( x = y -> ( ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> ta' ) ) with typecode |- |
44 |
43
|
exbidv |
Could not format ( x = y -> ( E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> E. f ta' ) ) : No typesetting found for |- ( x = y -> ( E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> E. f ta' ) ) with typecode |- |
45 |
44
|
anbi2d |
Could not format ( x = y -> ( ( R _FrSe A /\ E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) <-> ( R _FrSe A /\ E. f ta' ) ) ) : No typesetting found for |- ( x = y -> ( ( R _FrSe A /\ E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) <-> ( R _FrSe A /\ E. f ta' ) ) ) with typecode |- |
46 |
43
|
eubidv |
Could not format ( x = y -> ( E! f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> E! f ta' ) ) : No typesetting found for |- ( x = y -> ( E! f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> E! f ta' ) ) with typecode |- |
47 |
45 46
|
imbi12d |
Could not format ( x = y -> ( ( ( R _FrSe A /\ E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) -> E! f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) <-> ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) ) ) : No typesetting found for |- ( x = y -> ( ( ( R _FrSe A /\ E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) -> E! f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) <-> ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) ) ) with typecode |- |
48 |
|
biid |
|
49 |
1 2 3 48
|
bnj1321 |
|
50 |
36 47 49
|
chvarfv |
Could not format ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) : No typesetting found for |- ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) with typecode |- |
51 |
27 29 50
|
syl2anc |
Could not format ( ( ch /\ y e. _pred ( x , A , R ) ) -> E! f ta' ) : No typesetting found for |- ( ( ch /\ y e. _pred ( x , A , R ) ) -> E! f ta' ) with typecode |- |
52 |
51
|
ex |
Could not format ( ch -> ( y e. _pred ( x , A , R ) -> E! f ta' ) ) : No typesetting found for |- ( ch -> ( y e. _pred ( x , A , R ) -> E! f ta' ) ) with typecode |- |
53 |
24 52
|
ralrimi |
Could not format ( ch -> A. y e. _pred ( x , A , R ) E! f ta' ) : No typesetting found for |- ( ch -> A. y e. _pred ( x , A , R ) E! f ta' ) with typecode |- |
54 |
9
|
a1i |
Could not format ( ch -> H = { f | E. y e. _pred ( x , A , R ) ta' } ) : No typesetting found for |- ( ch -> H = { f | E. y e. _pred ( x , A , R ) ta' } ) with typecode |- |
55 |
|
biid |
Could not format ( ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f | E. y e. _pred ( x , A , R ) ta' } ) <-> ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f | E. y e. _pred ( x , A , R ) ta' } ) ) : No typesetting found for |- ( ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f | E. y e. _pred ( x , A , R ) ta' } ) <-> ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f | E. y e. _pred ( x , A , R ) ta' } ) ) with typecode |- |
56 |
55
|
bnj1366 |
Could not format ( ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f | E. y e. _pred ( x , A , R ) ta' } ) -> H e. _V ) : No typesetting found for |- ( ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f | E. y e. _pred ( x , A , R ) ta' } ) -> H e. _V ) with typecode |- |
57 |
19 53 54 56
|
syl3anc |
|
58 |
57
|
uniexd |
|
59 |
10 58
|
eqeltrid |
|
60 |
|
snex |
|
61 |
60
|
a1i |
|
62 |
59 61
|
bnj1149 |
|
63 |
12 62
|
eqeltrid |
|