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 | bnj1280.1 | |
|
bnj1280.2 | |
||
bnj1280.3 | |
||
bnj1280.4 | |
||
bnj1280.5 | |
||
bnj1280.6 | |
||
bnj1280.7 | |
||
bnj1280.17 | |
||
Assertion | bnj1280 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bnj1280.1 | |
|
2 | bnj1280.2 | |
|
3 | bnj1280.3 | |
|
4 | bnj1280.4 | |
|
5 | bnj1280.5 | |
|
6 | bnj1280.6 | |
|
7 | bnj1280.7 | |
|
8 | bnj1280.17 | |
|
9 | 1 2 3 4 5 6 7 | bnj1286 | |
10 | 9 | sseld | |
11 | disj1 | |
|
12 | 8 11 | sylib | |
13 | 12 | 19.21bi | |
14 | fveq2 | |
|
15 | fveq2 | |
|
16 | 14 15 | neeq12d | |
17 | 16 5 | elrab2 | |
18 | 17 | notbii | |
19 | imnan | |
|
20 | nne | |
|
21 | 20 | imbi2i | |
22 | 18 19 21 | 3bitr2i | |
23 | 13 22 | imbitrdi | |
24 | 10 23 | mpdd | |
25 | 24 | imp | |
26 | fvres | |
|
27 | 10 26 | syl6 | |
28 | 27 | imp | |
29 | fvres | |
|
30 | 10 29 | syl6 | |
31 | 30 | imp | |
32 | 25 28 31 | 3eqtr4d | |
33 | 32 | ralrimiva | |
34 | 9 | resabs1d | |
35 | 9 | resabs1d | |
36 | 34 35 | eqeq12d | |
37 | 1 2 3 4 5 6 7 | bnj1256 | |
38 | 4 | bnj1292 | |
39 | fndm | |
|
40 | 38 39 | sseqtrid | |
41 | fnssres | |
|
42 | 40 41 | mpdan | |
43 | 37 42 | bnj31 | |
44 | 43 | bnj1265 | |
45 | 7 44 | bnj835 | |
46 | 1 2 3 4 5 6 7 | bnj1259 | |
47 | 4 | bnj1293 | |
48 | fndm | |
|
49 | 47 48 | sseqtrid | |
50 | fnssres | |
|
51 | 49 50 | mpdan | |
52 | 46 51 | bnj31 | |
53 | 52 | bnj1265 | |
54 | 7 53 | bnj835 | |
55 | fvreseq | |
|
56 | 45 54 9 55 | syl21anc | |
57 | 36 56 | bitr3d | |
58 | 33 57 | mpbird | |