Description: Lemma for ipassi . Show that ( ( w S A ) P B ) - ( w x. ( A P B ) ) is continuous on RR . (Contributed by NM, 23-Aug-2007) (Revised by Mario Carneiro, 6-May-2014) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ip1i.1 | |
|
ip1i.2 | |
||
ip1i.4 | |
||
ip1i.7 | |
||
ip1i.9 | |
||
ipasslem7.a | |
||
ipasslem7.b | |
||
ipasslem7.f | |
||
ipasslem7.j | |
||
ipasslem7.k | |
||
Assertion | ipasslem7 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ip1i.1 | |
|
2 | ip1i.2 | |
|
3 | ip1i.4 | |
|
4 | ip1i.7 | |
|
5 | ip1i.9 | |
|
6 | ipasslem7.a | |
|
7 | ipasslem7.b | |
|
8 | ipasslem7.f | |
|
9 | ipasslem7.j | |
|
10 | ipasslem7.k | |
|
11 | 10 | tgioo2 | |
12 | 9 11 | eqtri | |
13 | 10 | cnfldtopon | |
14 | 13 | a1i | |
15 | ax-resscn | |
|
16 | 15 | a1i | |
17 | 14 | cnmptid | |
18 | 5 | phnvi | |
19 | eqid | |
|
20 | 1 19 | imsxmet | |
21 | 18 20 | ax-mp | |
22 | eqid | |
|
23 | 22 | mopntopon | |
24 | 21 23 | mp1i | |
25 | 6 | a1i | |
26 | 14 24 25 | cnmptc | |
27 | 19 22 3 10 | smcn | |
28 | 18 27 | mp1i | |
29 | 14 17 26 28 | cnmpt12f | |
30 | 7 | a1i | |
31 | 14 24 30 | cnmptc | |
32 | 4 19 22 10 | dipcn | |
33 | 18 32 | mp1i | |
34 | 14 29 31 33 | cnmpt12f | |
35 | 1 4 | dipcl | |
36 | 18 6 7 35 | mp3an | |
37 | 36 | a1i | |
38 | 14 14 37 | cnmptc | |
39 | 10 | mulcn | |
40 | 39 | a1i | |
41 | 14 17 38 40 | cnmpt12f | |
42 | 10 | subcn | |
43 | 42 | a1i | |
44 | 14 34 41 43 | cnmpt12f | |
45 | 12 14 16 44 | cnmpt1res | |
46 | 45 | mptru | |
47 | 8 46 | eqeltri | |