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 
|- ( ( J e. Top /\ B e. V ) -> ( ( J |`t B ) e. Locally A <-> A. x e. J A. y e. ( x i^i B ) E. u e. J ( ( u i^i B ) C_ x /\ y e. u /\ ( J |`t ( u i^i B ) ) e. A ) ) )

Proof

Step Hyp Ref Expression
1 resttop 
 |-  ( ( J e. Top /\ B e. V ) -> ( J |`t B ) e. Top )
2 islly 
 |-  ( ( J |`t B ) e. Locally A <-> ( ( J |`t B ) e. Top /\ A. z e. ( J |`t B ) A. y e. z E. w e. ( ( J |`t B ) i^i ~P z ) ( y e. w /\ ( ( J |`t B ) |`t w ) e. A ) ) )
3 2 baib 
 |-  ( ( J |`t B ) e. Top -> ( ( J |`t B ) e. Locally A <-> A. z e. ( J |`t B ) A. y e. z E. w e. ( ( J |`t B ) i^i ~P z ) ( y e. w /\ ( ( J |`t B ) |`t w ) e. A ) ) )
4 1 3 syl 
 |-  ( ( J e. Top /\ B e. V ) -> ( ( J |`t B ) e. Locally A <-> A. z e. ( J |`t B ) A. y e. z E. w e. ( ( J |`t B ) i^i ~P z ) ( y e. w /\ ( ( J |`t B ) |`t w ) e. A ) ) )
5 vex 
 |-  x e. _V
6 5 inex1 
 |-  ( x i^i B ) e. _V
7 6 a1i 
 |-  ( ( ( J e. Top /\ B e. V ) /\ x e. J ) -> ( x i^i B ) e. _V )
8 elrest 
 |-  ( ( J e. Top /\ B e. V ) -> ( z e. ( J |`t B ) <-> E. x e. J z = ( x i^i B ) ) )
9 simpr 
 |-  ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) -> z = ( x i^i B ) )
10 9 raleqdv 
 |-  ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) -> ( A. y e. z E. w e. ( ( J |`t B ) i^i ~P z ) ( y e. w /\ ( ( J |`t B ) |`t w ) e. A ) <-> A. y e. ( x i^i B ) E. w e. ( ( J |`t B ) i^i ~P z ) ( y e. w /\ ( ( J |`t B ) |`t w ) e. A ) ) )
11 rexin 
 |-  ( E. w e. ( ( J |`t B ) i^i ~P z ) ( y e. w /\ ( ( J |`t B ) |`t w ) e. A ) <-> E. w e. ( J |`t B ) ( w e. ~P z /\ ( y e. w /\ ( ( J |`t B ) |`t w ) e. A ) ) )
12 vex 
 |-  u e. _V
13 12 inex1 
 |-  ( u i^i B ) e. _V
14 13 a1i 
 |-  ( ( ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) /\ y e. ( x i^i B ) ) /\ u e. J ) -> ( u i^i B ) e. _V )
15 elrest 
 |-  ( ( J e. Top /\ B e. V ) -> ( w e. ( J |`t B ) <-> E. u e. J w = ( u i^i B ) ) )
16 15 ad2antrr 
 |-  ( ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) /\ y e. ( x i^i B ) ) -> ( w e. ( J |`t B ) <-> E. u e. J w = ( u i^i B ) ) )
17 3anass 
 |-  ( ( w e. ~P z /\ y e. w /\ ( ( J |`t B ) |`t w ) e. A ) <-> ( w e. ~P z /\ ( y e. w /\ ( ( J |`t B ) |`t w ) e. A ) ) )
18 simpr 
 |-  ( ( ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) /\ y e. ( x i^i B ) ) /\ w = ( u i^i B ) ) -> w = ( u i^i B ) )
19 simpllr 
 |-  ( ( ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) /\ y e. ( x i^i B ) ) /\ w = ( u i^i B ) ) -> z = ( x i^i B ) )
20 18 19 sseq12d 
 |-  ( ( ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) /\ y e. ( x i^i B ) ) /\ w = ( u i^i B ) ) -> ( w C_ z <-> ( u i^i B ) C_ ( x i^i B ) ) )
21 velpw 
 |-  ( w e. ~P z <-> w C_ z )
22 inss2 
 |-  ( u i^i B ) C_ B
23 22 biantru 
 |-  ( ( u i^i B ) C_ x <-> ( ( u i^i B ) C_ x /\ ( u i^i B ) C_ B ) )
24 ssin 
 |-  ( ( ( u i^i B ) C_ x /\ ( u i^i B ) C_ B ) <-> ( u i^i B ) C_ ( x i^i B ) )
25 23 24 bitri 
 |-  ( ( u i^i B ) C_ x <-> ( u i^i B ) C_ ( x i^i B ) )
26 20 21 25 3bitr4g 
 |-  ( ( ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) /\ y e. ( x i^i B ) ) /\ w = ( u i^i B ) ) -> ( w e. ~P z <-> ( u i^i B ) C_ x ) )
27 18 eleq2d 
 |-  ( ( ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) /\ y e. ( x i^i B ) ) /\ w = ( u i^i B ) ) -> ( y e. w <-> y e. ( u i^i B ) ) )
28 simplr 
 |-  ( ( ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) /\ y e. ( x i^i B ) ) /\ w = ( u i^i B ) ) -> y e. ( x i^i B ) )
29 28 elin2d 
 |-  ( ( ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) /\ y e. ( x i^i B ) ) /\ w = ( u i^i B ) ) -> y e. B )
30 29 biantrud 
 |-  ( ( ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) /\ y e. ( x i^i B ) ) /\ w = ( u i^i B ) ) -> ( y e. u <-> ( y e. u /\ y e. B ) ) )
31 elin 
 |-  ( y e. ( u i^i B ) <-> ( y e. u /\ y e. B ) )
32 30 31 bitr4di 
 |-  ( ( ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) /\ y e. ( x i^i B ) ) /\ w = ( u i^i B ) ) -> ( y e. u <-> y e. ( u i^i B ) ) )
33 27 32 bitr4d 
 |-  ( ( ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) /\ y e. ( x i^i B ) ) /\ w = ( u i^i B ) ) -> ( y e. w <-> y e. u ) )
34 18 oveq2d 
 |-  ( ( ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) /\ y e. ( x i^i B ) ) /\ w = ( u i^i B ) ) -> ( ( J |`t B ) |`t w ) = ( ( J |`t B ) |`t ( u i^i B ) ) )
35 simp-4l 
 |-  ( ( ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) /\ y e. ( x i^i B ) ) /\ w = ( u i^i B ) ) -> J e. Top )
36 22 a1i 
 |-  ( ( ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) /\ y e. ( x i^i B ) ) /\ w = ( u i^i B ) ) -> ( u i^i B ) C_ B )
37 simplr 
 |-  ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) -> B e. V )
38 37 ad2antrr 
 |-  ( ( ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) /\ y e. ( x i^i B ) ) /\ w = ( u i^i B ) ) -> B e. V )
39 restabs 
 |-  ( ( J e. Top /\ ( u i^i B ) C_ B /\ B e. V ) -> ( ( J |`t B ) |`t ( u i^i B ) ) = ( J |`t ( u i^i B ) ) )
40 35 36 38 39 syl3anc 
 |-  ( ( ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) /\ y e. ( x i^i B ) ) /\ w = ( u i^i B ) ) -> ( ( J |`t B ) |`t ( u i^i B ) ) = ( J |`t ( u i^i B ) ) )
41 34 40 eqtrd 
 |-  ( ( ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) /\ y e. ( x i^i B ) ) /\ w = ( u i^i B ) ) -> ( ( J |`t B ) |`t w ) = ( J |`t ( u i^i B ) ) )
42 41 eleq1d 
 |-  ( ( ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) /\ y e. ( x i^i B ) ) /\ w = ( u i^i B ) ) -> ( ( ( J |`t B ) |`t w ) e. A <-> ( J |`t ( u i^i B ) ) e. A ) )
43 26 33 42 3anbi123d 
 |-  ( ( ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) /\ y e. ( x i^i B ) ) /\ w = ( u i^i B ) ) -> ( ( w e. ~P z /\ y e. w /\ ( ( J |`t B ) |`t w ) e. A ) <-> ( ( u i^i B ) C_ x /\ y e. u /\ ( J |`t ( u i^i B ) ) e. A ) ) )
44 17 43 bitr3id 
 |-  ( ( ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) /\ y e. ( x i^i B ) ) /\ w = ( u i^i B ) ) -> ( ( w e. ~P z /\ ( y e. w /\ ( ( J |`t B ) |`t w ) e. A ) ) <-> ( ( u i^i B ) C_ x /\ y e. u /\ ( J |`t ( u i^i B ) ) e. A ) ) )
45 14 16 44 rexxfr2d 
 |-  ( ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) /\ y e. ( x i^i B ) ) -> ( E. w e. ( J |`t B ) ( w e. ~P z /\ ( y e. w /\ ( ( J |`t B ) |`t w ) e. A ) ) <-> E. u e. J ( ( u i^i B ) C_ x /\ y e. u /\ ( J |`t ( u i^i B ) ) e. A ) ) )
46 11 45 syl5bb 
 |-  ( ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) /\ y e. ( x i^i B ) ) -> ( E. w e. ( ( J |`t B ) i^i ~P z ) ( y e. w /\ ( ( J |`t B ) |`t w ) e. A ) <-> E. u e. J ( ( u i^i B ) C_ x /\ y e. u /\ ( J |`t ( u i^i B ) ) e. A ) ) )
47 46 ralbidva 
 |-  ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) -> ( A. y e. ( x i^i B ) E. w e. ( ( J |`t B ) i^i ~P z ) ( y e. w /\ ( ( J |`t B ) |`t w ) e. A ) <-> A. y e. ( x i^i B ) E. u e. J ( ( u i^i B ) C_ x /\ y e. u /\ ( J |`t ( u i^i B ) ) e. A ) ) )
48 10 47 bitrd 
 |-  ( ( ( J e. Top /\ B e. V ) /\ z = ( x i^i B ) ) -> ( A. y e. z E. w e. ( ( J |`t B ) i^i ~P z ) ( y e. w /\ ( ( J |`t B ) |`t w ) e. A ) <-> A. y e. ( x i^i B ) E. u e. J ( ( u i^i B ) C_ x /\ y e. u /\ ( J |`t ( u i^i B ) ) e. A ) ) )
49 7 8 48 ralxfr2d 
 |-  ( ( J e. Top /\ B e. V ) -> ( A. z e. ( J |`t B ) A. y e. z E. w e. ( ( J |`t B ) i^i ~P z ) ( y e. w /\ ( ( J |`t B ) |`t w ) e. A ) <-> A. x e. J A. y e. ( x i^i B ) E. u e. J ( ( u i^i B ) C_ x /\ y e. u /\ ( J |`t ( u i^i B ) ) e. A ) ) )
50 4 49 bitrd 
 |-  ( ( J e. Top /\ B e. V ) -> ( ( J |`t B ) e. Locally A <-> A. x e. J A. y e. ( x i^i B ) E. u e. J ( ( u i^i B ) C_ x /\ y e. u /\ ( J |`t ( u i^i B ) ) e. A ) ) )