Metamath Proof Explorer

Theorem restbas

Description: A subspace topology basis is a basis. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Assertion restbas 
|- ( B e. TopBases -> ( B |`t A ) e. TopBases )

Proof

Step Hyp Ref Expression
1 elrest 
 |-  ( ( B e. TopBases /\ A e. _V ) -> ( a e. ( B |`t A ) <-> E. u e. B a = ( u i^i A ) ) )
2 elrest 
 |-  ( ( B e. TopBases /\ A e. _V ) -> ( b e. ( B |`t A ) <-> E. v e. B b = ( v i^i A ) ) )
3 1 2 anbi12d 
 |-  ( ( B e. TopBases /\ A e. _V ) -> ( ( a e. ( B |`t A ) /\ b e. ( B |`t A ) ) <-> ( E. u e. B a = ( u i^i A ) /\ E. v e. B b = ( v i^i A ) ) ) )
4 reeanv 
 |-  ( E. u e. B E. v e. B ( a = ( u i^i A ) /\ b = ( v i^i A ) ) <-> ( E. u e. B a = ( u i^i A ) /\ E. v e. B b = ( v i^i A ) ) )
5 3 4 bitr4di 
 |-  ( ( B e. TopBases /\ A e. _V ) -> ( ( a e. ( B |`t A ) /\ b e. ( B |`t A ) ) <-> E. u e. B E. v e. B ( a = ( u i^i A ) /\ b = ( v i^i A ) ) ) )
6 simplll 
 |-  ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) -> B e. TopBases )
7 simplrl 
 |-  ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) -> u e. B )
8 simplrr 
 |-  ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) -> v e. B )
9 simpr 
 |-  ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) -> c e. ( ( u i^i v ) i^i A ) )
10 9 elin1d 
 |-  ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) -> c e. ( u i^i v ) )
11 basis2 
 |-  ( ( ( B e. TopBases /\ u e. B ) /\ ( v e. B /\ c e. ( u i^i v ) ) ) -> E. z e. B ( c e. z /\ z C_ ( u i^i v ) ) )
12 6 7 8 10 11 syl22anc 
 |-  ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) -> E. z e. B ( c e. z /\ z C_ ( u i^i v ) ) )
13 simplll 
 |-  ( ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) /\ ( z e. B /\ ( c e. z /\ z C_ ( u i^i v ) ) ) ) -> ( B e. TopBases /\ A e. _V ) )
14 13 simpld 
 |-  ( ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) /\ ( z e. B /\ ( c e. z /\ z C_ ( u i^i v ) ) ) ) -> B e. TopBases )
15 13 simprd 
 |-  ( ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) /\ ( z e. B /\ ( c e. z /\ z C_ ( u i^i v ) ) ) ) -> A e. _V )
16 simprl 
 |-  ( ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) /\ ( z e. B /\ ( c e. z /\ z C_ ( u i^i v ) ) ) ) -> z e. B )
17 elrestr 
 |-  ( ( B e. TopBases /\ A e. _V /\ z e. B ) -> ( z i^i A ) e. ( B |`t A ) )
18 14 15 16 17 syl3anc 
 |-  ( ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) /\ ( z e. B /\ ( c e. z /\ z C_ ( u i^i v ) ) ) ) -> ( z i^i A ) e. ( B |`t A ) )
19 simprrl 
 |-  ( ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) /\ ( z e. B /\ ( c e. z /\ z C_ ( u i^i v ) ) ) ) -> c e. z )
20 simplr 
 |-  ( ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) /\ ( z e. B /\ ( c e. z /\ z C_ ( u i^i v ) ) ) ) -> c e. ( ( u i^i v ) i^i A ) )
21 20 elin2d 
 |-  ( ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) /\ ( z e. B /\ ( c e. z /\ z C_ ( u i^i v ) ) ) ) -> c e. A )
22 19 21 elind 
 |-  ( ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) /\ ( z e. B /\ ( c e. z /\ z C_ ( u i^i v ) ) ) ) -> c e. ( z i^i A ) )
23 simprrr 
 |-  ( ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) /\ ( z e. B /\ ( c e. z /\ z C_ ( u i^i v ) ) ) ) -> z C_ ( u i^i v ) )
24 23 ssrind 
 |-  ( ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) /\ ( z e. B /\ ( c e. z /\ z C_ ( u i^i v ) ) ) ) -> ( z i^i A ) C_ ( ( u i^i v ) i^i A ) )
25 eleq2 
 |-  ( w = ( z i^i A ) -> ( c e. w <-> c e. ( z i^i A ) ) )
26 sseq1 
 |-  ( w = ( z i^i A ) -> ( w C_ ( ( u i^i v ) i^i A ) <-> ( z i^i A ) C_ ( ( u i^i v ) i^i A ) ) )
27 25 26 anbi12d 
 |-  ( w = ( z i^i A ) -> ( ( c e. w /\ w C_ ( ( u i^i v ) i^i A ) ) <-> ( c e. ( z i^i A ) /\ ( z i^i A ) C_ ( ( u i^i v ) i^i A ) ) ) )
28 27 rspcev 
 |-  ( ( ( z i^i A ) e. ( B |`t A ) /\ ( c e. ( z i^i A ) /\ ( z i^i A ) C_ ( ( u i^i v ) i^i A ) ) ) -> E. w e. ( B |`t A ) ( c e. w /\ w C_ ( ( u i^i v ) i^i A ) ) )
29 18 22 24 28 syl12anc 
 |-  ( ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) /\ ( z e. B /\ ( c e. z /\ z C_ ( u i^i v ) ) ) ) -> E. w e. ( B |`t A ) ( c e. w /\ w C_ ( ( u i^i v ) i^i A ) ) )
30 12 29 rexlimddv 
 |-  ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) -> E. w e. ( B |`t A ) ( c e. w /\ w C_ ( ( u i^i v ) i^i A ) ) )
31 30 ralrimiva 
 |-  ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) -> A. c e. ( ( u i^i v ) i^i A ) E. w e. ( B |`t A ) ( c e. w /\ w C_ ( ( u i^i v ) i^i A ) ) )
32 ineq12 
 |-  ( ( a = ( u i^i A ) /\ b = ( v i^i A ) ) -> ( a i^i b ) = ( ( u i^i A ) i^i ( v i^i A ) ) )
33 inindir 
 |-  ( ( u i^i v ) i^i A ) = ( ( u i^i A ) i^i ( v i^i A ) )
34 32 33 eqtr4di 
 |-  ( ( a = ( u i^i A ) /\ b = ( v i^i A ) ) -> ( a i^i b ) = ( ( u i^i v ) i^i A ) )
35 34 sseq2d 
 |-  ( ( a = ( u i^i A ) /\ b = ( v i^i A ) ) -> ( w C_ ( a i^i b ) <-> w C_ ( ( u i^i v ) i^i A ) ) )
36 35 anbi2d 
 |-  ( ( a = ( u i^i A ) /\ b = ( v i^i A ) ) -> ( ( c e. w /\ w C_ ( a i^i b ) ) <-> ( c e. w /\ w C_ ( ( u i^i v ) i^i A ) ) ) )
37 36 rexbidv 
 |-  ( ( a = ( u i^i A ) /\ b = ( v i^i A ) ) -> ( E. w e. ( B |`t A ) ( c e. w /\ w C_ ( a i^i b ) ) <-> E. w e. ( B |`t A ) ( c e. w /\ w C_ ( ( u i^i v ) i^i A ) ) ) )
38 34 37 raleqbidv 
 |-  ( ( a = ( u i^i A ) /\ b = ( v i^i A ) ) -> ( A. c e. ( a i^i b ) E. w e. ( B |`t A ) ( c e. w /\ w C_ ( a i^i b ) ) <-> A. c e. ( ( u i^i v ) i^i A ) E. w e. ( B |`t A ) ( c e. w /\ w C_ ( ( u i^i v ) i^i A ) ) ) )
39 31 38 syl5ibrcom 
 |-  ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) -> ( ( a = ( u i^i A ) /\ b = ( v i^i A ) ) -> A. c e. ( a i^i b ) E. w e. ( B |`t A ) ( c e. w /\ w C_ ( a i^i b ) ) ) )
40 39 rexlimdvva 
 |-  ( ( B e. TopBases /\ A e. _V ) -> ( E. u e. B E. v e. B ( a = ( u i^i A ) /\ b = ( v i^i A ) ) -> A. c e. ( a i^i b ) E. w e. ( B |`t A ) ( c e. w /\ w C_ ( a i^i b ) ) ) )
41 5 40 sylbid 
 |-  ( ( B e. TopBases /\ A e. _V ) -> ( ( a e. ( B |`t A ) /\ b e. ( B |`t A ) ) -> A. c e. ( a i^i b ) E. w e. ( B |`t A ) ( c e. w /\ w C_ ( a i^i b ) ) ) )
42 41 ralrimivv 
 |-  ( ( B e. TopBases /\ A e. _V ) -> A. a e. ( B |`t A ) A. b e. ( B |`t A ) A. c e. ( a i^i b ) E. w e. ( B |`t A ) ( c e. w /\ w C_ ( a i^i b ) ) )
43 ovex 
 |-  ( B |`t A ) e. _V
44 isbasis2g 
 |-  ( ( B |`t A ) e. _V -> ( ( B |`t A ) e. TopBases <-> A. a e. ( B |`t A ) A. b e. ( B |`t A ) A. c e. ( a i^i b ) E. w e. ( B |`t A ) ( c e. w /\ w C_ ( a i^i b ) ) ) )
45 43 44 ax-mp 
 |-  ( ( B |`t A ) e. TopBases <-> A. a e. ( B |`t A ) A. b e. ( B |`t A ) A. c e. ( a i^i b ) E. w e. ( B |`t A ) ( c e. w /\ w C_ ( a i^i b ) ) )
46 42 45 sylibr 
 |-  ( ( B e. TopBases /\ A e. _V ) -> ( B |`t A ) e. TopBases )
47 relxp 
 |-  Rel ( _V X. _V )
48 restfn 
 |-  |`t Fn ( _V X. _V )
49 fndm 
 |-  ( |`t Fn ( _V X. _V ) -> dom |`t = ( _V X. _V ) )
50 48 49 ax-mp 
 |-  dom |`t = ( _V X. _V )
51 50 releqi 
 |-  ( Rel dom |`t <-> Rel ( _V X. _V ) )
52 47 51 mpbir 
 |-  Rel dom |`t
53 52 ovprc2 
 |-  ( -. A e. _V -> ( B |`t A ) = (/) )
54 53 adantl 
 |-  ( ( B e. TopBases /\ -. A e. _V ) -> ( B |`t A ) = (/) )
55 fi0 
 |-  ( fi ` (/) ) = (/)
56 fibas 
 |-  ( fi ` (/) ) e. TopBases
57 55 56 eqeltrri 
 |-  (/) e. TopBases
58 54 57 eqeltrdi 
 |-  ( ( B e. TopBases /\ -. A e. _V ) -> ( B |`t A ) e. TopBases )
59 46 58 pm2.61dan 
 |-  ( B e. TopBases -> ( B |`t A ) e. TopBases )