Description: Technical lemma for bnj60 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | bnj1447.1 | |
|
bnj1447.2 | |
||
bnj1447.3 | |
||
bnj1447.4 | |
||
bnj1447.5 | |
||
bnj1447.6 | |
||
bnj1447.7 | |
||
bnj1447.8 | No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |- | ||
bnj1447.9 | No typesetting found for |- H = { f | E. y e. _pred ( x , A , R ) ta' } with typecode |- | ||
bnj1447.10 | |
||
bnj1447.11 | |
||
bnj1447.12 | |
||
bnj1447.13 | |
||
Assertion | bnj1447 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bnj1447.1 | |
|
2 | bnj1447.2 | |
|
3 | bnj1447.3 | |
|
4 | bnj1447.4 | |
|
5 | bnj1447.5 | |
|
6 | bnj1447.6 | |
|
7 | bnj1447.7 | |
|
8 | bnj1447.8 | Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |- | |
9 | bnj1447.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 | bnj1447.10 | |
|
11 | bnj1447.11 | |
|
12 | bnj1447.12 | |
|
13 | bnj1447.13 | |
|
14 | nfre1 | Could not format F/ y E. y e. _pred ( x , A , R ) ta' : No typesetting found for |- F/ y E. y e. _pred ( x , A , R ) ta' with typecode |- | |
15 | 14 | nfab | Could not format F/_ y { f | E. y e. _pred ( x , A , R ) ta' } : No typesetting found for |- F/_ y { f | E. y e. _pred ( x , A , R ) ta' } with typecode |- |
16 | 9 15 | nfcxfr | |
17 | 16 | nfuni | |
18 | 10 17 | nfcxfr | |
19 | nfcv | |
|
20 | nfcv | |
|
21 | nfcv | |
|
22 | 18 21 | nfres | |
23 | 19 22 | nfop | |
24 | 11 23 | nfcxfr | |
25 | 20 24 | nffv | |
26 | 19 25 | nfop | |
27 | 26 | nfsn | |
28 | 18 27 | nfun | |
29 | 12 28 | nfcxfr | |
30 | nfcv | |
|
31 | 29 30 | nffv | |
32 | nfcv | |
|
33 | 29 32 | nfres | |
34 | 30 33 | nfop | |
35 | 13 34 | nfcxfr | |
36 | 20 35 | nffv | |
37 | 31 36 | nfeq | |
38 | 37 | nf5ri | |