Description: The property of a subspace being locally A . (Contributed by Mario Carneiro, 10-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | subislly | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resttop | |
|
2 | islly | |
|
3 | 2 | baib | |
4 | 1 3 | syl | |
5 | vex | |
|
6 | 5 | inex1 | |
7 | 6 | a1i | |
8 | elrest | |
|
9 | simpr | |
|
10 | 9 | raleqdv | |
11 | rexin | |
|
12 | vex | |
|
13 | 12 | inex1 | |
14 | 13 | a1i | |
15 | elrest | |
|
16 | 15 | ad2antrr | |
17 | 3anass | |
|
18 | simpr | |
|
19 | simpllr | |
|
20 | 18 19 | sseq12d | |
21 | velpw | |
|
22 | inss2 | |
|
23 | 22 | biantru | |
24 | ssin | |
|
25 | 23 24 | bitri | |
26 | 20 21 25 | 3bitr4g | |
27 | 18 | eleq2d | |
28 | simplr | |
|
29 | 28 | elin2d | |
30 | 29 | biantrud | |
31 | elin | |
|
32 | 30 31 | bitr4di | |
33 | 27 32 | bitr4d | |
34 | 18 | oveq2d | |
35 | simp-4l | |
|
36 | 22 | a1i | |
37 | simplr | |
|
38 | 37 | ad2antrr | |
39 | restabs | |
|
40 | 35 36 38 39 | syl3anc | |
41 | 34 40 | eqtrd | |
42 | 41 | eleq1d | |
43 | 26 33 42 | 3anbi123d | |
44 | 17 43 | bitr3id | |
45 | 14 16 44 | rexxfr2d | |
46 | 11 45 | syl5bb | |
47 | 46 | ralbidva | |
48 | 10 47 | bitrd | |
49 | 7 8 48 | ralxfr2d | |
50 | 4 49 | bitrd | |