Metamath Proof Explorer


Theorem subislly

Description: The property of a subspace being locally A . (Contributed by Mario Carneiro, 10-Mar-2015)

Ref Expression
Assertion subislly JTopBVJ𝑡BLocally A xJyxBuJuBxyuJ𝑡uBA

Proof

Step Hyp Ref Expression
1 resttop JTopBVJ𝑡BTop
2 islly J𝑡BLocally A J𝑡BTopzJ𝑡ByzwJ𝑡B𝒫zywJ𝑡B𝑡wA
3 2 baib J𝑡BTopJ𝑡BLocally A zJ𝑡ByzwJ𝑡B𝒫zywJ𝑡B𝑡wA
4 1 3 syl JTopBVJ𝑡BLocally A zJ𝑡ByzwJ𝑡B𝒫zywJ𝑡B𝑡wA
5 vex xV
6 5 inex1 xBV
7 6 a1i JTopBVxJxBV
8 elrest JTopBVzJ𝑡BxJz=xB
9 simpr JTopBVz=xBz=xB
10 9 raleqdv JTopBVz=xByzwJ𝑡B𝒫zywJ𝑡B𝑡wAyxBwJ𝑡B𝒫zywJ𝑡B𝑡wA
11 rexin wJ𝑡B𝒫zywJ𝑡B𝑡wAwJ𝑡Bw𝒫zywJ𝑡B𝑡wA
12 vex uV
13 12 inex1 uBV
14 13 a1i JTopBVz=xByxBuJuBV
15 elrest JTopBVwJ𝑡BuJw=uB
16 15 ad2antrr JTopBVz=xByxBwJ𝑡BuJw=uB
17 3anass w𝒫zywJ𝑡B𝑡wAw𝒫zywJ𝑡B𝑡wA
18 simpr JTopBVz=xByxBw=uBw=uB
19 simpllr JTopBVz=xByxBw=uBz=xB
20 18 19 sseq12d JTopBVz=xByxBw=uBwzuBxB
21 velpw w𝒫zwz
22 inss2 uBB
23 22 biantru uBxuBxuBB
24 ssin uBxuBBuBxB
25 23 24 bitri uBxuBxB
26 20 21 25 3bitr4g JTopBVz=xByxBw=uBw𝒫zuBx
27 18 eleq2d JTopBVz=xByxBw=uBywyuB
28 simplr JTopBVz=xByxBw=uByxB
29 28 elin2d JTopBVz=xByxBw=uByB
30 29 biantrud JTopBVz=xByxBw=uByuyuyB
31 elin yuByuyB
32 30 31 bitr4di JTopBVz=xByxBw=uByuyuB
33 27 32 bitr4d JTopBVz=xByxBw=uBywyu
34 18 oveq2d JTopBVz=xByxBw=uBJ𝑡B𝑡w=J𝑡B𝑡uB
35 simp-4l JTopBVz=xByxBw=uBJTop
36 22 a1i JTopBVz=xByxBw=uBuBB
37 simplr JTopBVz=xBBV
38 37 ad2antrr JTopBVz=xByxBw=uBBV
39 restabs JTopuBBBVJ𝑡B𝑡uB=J𝑡uB
40 35 36 38 39 syl3anc JTopBVz=xByxBw=uBJ𝑡B𝑡uB=J𝑡uB
41 34 40 eqtrd JTopBVz=xByxBw=uBJ𝑡B𝑡w=J𝑡uB
42 41 eleq1d JTopBVz=xByxBw=uBJ𝑡B𝑡wAJ𝑡uBA
43 26 33 42 3anbi123d JTopBVz=xByxBw=uBw𝒫zywJ𝑡B𝑡wAuBxyuJ𝑡uBA
44 17 43 bitr3id JTopBVz=xByxBw=uBw𝒫zywJ𝑡B𝑡wAuBxyuJ𝑡uBA
45 14 16 44 rexxfr2d JTopBVz=xByxBwJ𝑡Bw𝒫zywJ𝑡B𝑡wAuJuBxyuJ𝑡uBA
46 11 45 syl5bb JTopBVz=xByxBwJ𝑡B𝒫zywJ𝑡B𝑡wAuJuBxyuJ𝑡uBA
47 46 ralbidva JTopBVz=xByxBwJ𝑡B𝒫zywJ𝑡B𝑡wAyxBuJuBxyuJ𝑡uBA
48 10 47 bitrd JTopBVz=xByzwJ𝑡B𝒫zywJ𝑡B𝑡wAyxBuJuBxyuJ𝑡uBA
49 7 8 48 ralxfr2d JTopBVzJ𝑡ByzwJ𝑡B𝒫zywJ𝑡B𝑡wAxJyxBuJuBxyuJ𝑡uBA
50 4 49 bitrd JTopBVJ𝑡BLocally A xJyxBuJuBxyuJ𝑡uBA