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 )