Metamath Proof Explorer


Theorem tgrest

Description: A subspace can be generated by restricted sets from a basis for the original topology. (Contributed by Mario Carneiro, 19-Mar-2015) (Proof shortened by Mario Carneiro, 30-Aug-2015)

Ref Expression
Assertion tgrest
|- ( ( B e. V /\ A e. W ) -> ( topGen ` ( B |`t A ) ) = ( ( topGen ` B ) |`t A ) )

Proof

Step Hyp Ref Expression
1 ovex
 |-  ( B |`t A ) e. _V
2 eltg3
 |-  ( ( B |`t A ) e. _V -> ( x e. ( topGen ` ( B |`t A ) ) <-> E. y ( y C_ ( B |`t A ) /\ x = U. y ) ) )
3 1 2 ax-mp
 |-  ( x e. ( topGen ` ( B |`t A ) ) <-> E. y ( y C_ ( B |`t A ) /\ x = U. y ) )
4 simpll
 |-  ( ( ( B e. V /\ A e. W ) /\ y C_ ( B |`t A ) ) -> B e. V )
5 funmpt
 |-  Fun ( x e. B |-> ( x i^i A ) )
6 5 a1i
 |-  ( ( ( B e. V /\ A e. W ) /\ y C_ ( B |`t A ) ) -> Fun ( x e. B |-> ( x i^i A ) ) )
7 restval
 |-  ( ( B e. V /\ A e. W ) -> ( B |`t A ) = ran ( x e. B |-> ( x i^i A ) ) )
8 7 sseq2d
 |-  ( ( B e. V /\ A e. W ) -> ( y C_ ( B |`t A ) <-> y C_ ran ( x e. B |-> ( x i^i A ) ) ) )
9 8 biimpa
 |-  ( ( ( B e. V /\ A e. W ) /\ y C_ ( B |`t A ) ) -> y C_ ran ( x e. B |-> ( x i^i A ) ) )
10 vex
 |-  x e. _V
11 10 inex1
 |-  ( x i^i A ) e. _V
12 11 rgenw
 |-  A. x e. B ( x i^i A ) e. _V
13 eqid
 |-  ( x e. B |-> ( x i^i A ) ) = ( x e. B |-> ( x i^i A ) )
14 13 fnmpt
 |-  ( A. x e. B ( x i^i A ) e. _V -> ( x e. B |-> ( x i^i A ) ) Fn B )
15 fnima
 |-  ( ( x e. B |-> ( x i^i A ) ) Fn B -> ( ( x e. B |-> ( x i^i A ) ) " B ) = ran ( x e. B |-> ( x i^i A ) ) )
16 12 14 15 mp2b
 |-  ( ( x e. B |-> ( x i^i A ) ) " B ) = ran ( x e. B |-> ( x i^i A ) )
17 9 16 sseqtrrdi
 |-  ( ( ( B e. V /\ A e. W ) /\ y C_ ( B |`t A ) ) -> y C_ ( ( x e. B |-> ( x i^i A ) ) " B ) )
18 ssimaexg
 |-  ( ( B e. V /\ Fun ( x e. B |-> ( x i^i A ) ) /\ y C_ ( ( x e. B |-> ( x i^i A ) ) " B ) ) -> E. z ( z C_ B /\ y = ( ( x e. B |-> ( x i^i A ) ) " z ) ) )
19 4 6 17 18 syl3anc
 |-  ( ( ( B e. V /\ A e. W ) /\ y C_ ( B |`t A ) ) -> E. z ( z C_ B /\ y = ( ( x e. B |-> ( x i^i A ) ) " z ) ) )
20 df-ima
 |-  ( ( x e. B |-> ( x i^i A ) ) " z ) = ran ( ( x e. B |-> ( x i^i A ) ) |` z )
21 resmpt
 |-  ( z C_ B -> ( ( x e. B |-> ( x i^i A ) ) |` z ) = ( x e. z |-> ( x i^i A ) ) )
22 21 adantl
 |-  ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> ( ( x e. B |-> ( x i^i A ) ) |` z ) = ( x e. z |-> ( x i^i A ) ) )
23 22 rneqd
 |-  ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> ran ( ( x e. B |-> ( x i^i A ) ) |` z ) = ran ( x e. z |-> ( x i^i A ) ) )
24 20 23 syl5eq
 |-  ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> ( ( x e. B |-> ( x i^i A ) ) " z ) = ran ( x e. z |-> ( x i^i A ) ) )
25 24 unieqd
 |-  ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> U. ( ( x e. B |-> ( x i^i A ) ) " z ) = U. ran ( x e. z |-> ( x i^i A ) ) )
26 11 dfiun3
 |-  U_ x e. z ( x i^i A ) = U. ran ( x e. z |-> ( x i^i A ) )
27 25 26 eqtr4di
 |-  ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> U. ( ( x e. B |-> ( x i^i A ) ) " z ) = U_ x e. z ( x i^i A ) )
28 iunin1
 |-  U_ x e. z ( x i^i A ) = ( U_ x e. z x i^i A )
29 27 28 eqtrdi
 |-  ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> U. ( ( x e. B |-> ( x i^i A ) ) " z ) = ( U_ x e. z x i^i A ) )
30 fvex
 |-  ( topGen ` B ) e. _V
31 simpr
 |-  ( ( B e. V /\ A e. W ) -> A e. W )
32 uniiun
 |-  U. z = U_ x e. z x
33 eltg3i
 |-  ( ( B e. V /\ z C_ B ) -> U. z e. ( topGen ` B ) )
34 32 33 eqeltrrid
 |-  ( ( B e. V /\ z C_ B ) -> U_ x e. z x e. ( topGen ` B ) )
35 34 adantlr
 |-  ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> U_ x e. z x e. ( topGen ` B ) )
36 elrestr
 |-  ( ( ( topGen ` B ) e. _V /\ A e. W /\ U_ x e. z x e. ( topGen ` B ) ) -> ( U_ x e. z x i^i A ) e. ( ( topGen ` B ) |`t A ) )
37 30 31 35 36 mp3an2ani
 |-  ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> ( U_ x e. z x i^i A ) e. ( ( topGen ` B ) |`t A ) )
38 29 37 eqeltrd
 |-  ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> U. ( ( x e. B |-> ( x i^i A ) ) " z ) e. ( ( topGen ` B ) |`t A ) )
39 unieq
 |-  ( y = ( ( x e. B |-> ( x i^i A ) ) " z ) -> U. y = U. ( ( x e. B |-> ( x i^i A ) ) " z ) )
40 39 eleq1d
 |-  ( y = ( ( x e. B |-> ( x i^i A ) ) " z ) -> ( U. y e. ( ( topGen ` B ) |`t A ) <-> U. ( ( x e. B |-> ( x i^i A ) ) " z ) e. ( ( topGen ` B ) |`t A ) ) )
41 38 40 syl5ibrcom
 |-  ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> ( y = ( ( x e. B |-> ( x i^i A ) ) " z ) -> U. y e. ( ( topGen ` B ) |`t A ) ) )
42 41 expimpd
 |-  ( ( B e. V /\ A e. W ) -> ( ( z C_ B /\ y = ( ( x e. B |-> ( x i^i A ) ) " z ) ) -> U. y e. ( ( topGen ` B ) |`t A ) ) )
43 42 exlimdv
 |-  ( ( B e. V /\ A e. W ) -> ( E. z ( z C_ B /\ y = ( ( x e. B |-> ( x i^i A ) ) " z ) ) -> U. y e. ( ( topGen ` B ) |`t A ) ) )
44 43 adantr
 |-  ( ( ( B e. V /\ A e. W ) /\ y C_ ( B |`t A ) ) -> ( E. z ( z C_ B /\ y = ( ( x e. B |-> ( x i^i A ) ) " z ) ) -> U. y e. ( ( topGen ` B ) |`t A ) ) )
45 19 44 mpd
 |-  ( ( ( B e. V /\ A e. W ) /\ y C_ ( B |`t A ) ) -> U. y e. ( ( topGen ` B ) |`t A ) )
46 eleq1
 |-  ( x = U. y -> ( x e. ( ( topGen ` B ) |`t A ) <-> U. y e. ( ( topGen ` B ) |`t A ) ) )
47 45 46 syl5ibrcom
 |-  ( ( ( B e. V /\ A e. W ) /\ y C_ ( B |`t A ) ) -> ( x = U. y -> x e. ( ( topGen ` B ) |`t A ) ) )
48 47 expimpd
 |-  ( ( B e. V /\ A e. W ) -> ( ( y C_ ( B |`t A ) /\ x = U. y ) -> x e. ( ( topGen ` B ) |`t A ) ) )
49 48 exlimdv
 |-  ( ( B e. V /\ A e. W ) -> ( E. y ( y C_ ( B |`t A ) /\ x = U. y ) -> x e. ( ( topGen ` B ) |`t A ) ) )
50 3 49 syl5bi
 |-  ( ( B e. V /\ A e. W ) -> ( x e. ( topGen ` ( B |`t A ) ) -> x e. ( ( topGen ` B ) |`t A ) ) )
51 50 ssrdv
 |-  ( ( B e. V /\ A e. W ) -> ( topGen ` ( B |`t A ) ) C_ ( ( topGen ` B ) |`t A ) )
52 restval
 |-  ( ( ( topGen ` B ) e. _V /\ A e. W ) -> ( ( topGen ` B ) |`t A ) = ran ( w e. ( topGen ` B ) |-> ( w i^i A ) ) )
53 30 31 52 sylancr
 |-  ( ( B e. V /\ A e. W ) -> ( ( topGen ` B ) |`t A ) = ran ( w e. ( topGen ` B ) |-> ( w i^i A ) ) )
54 eltg3
 |-  ( B e. V -> ( w e. ( topGen ` B ) <-> E. z ( z C_ B /\ w = U. z ) ) )
55 54 adantr
 |-  ( ( B e. V /\ A e. W ) -> ( w e. ( topGen ` B ) <-> E. z ( z C_ B /\ w = U. z ) ) )
56 32 ineq1i
 |-  ( U. z i^i A ) = ( U_ x e. z x i^i A )
57 56 28 eqtr4i
 |-  ( U. z i^i A ) = U_ x e. z ( x i^i A )
58 simplll
 |-  ( ( ( ( B e. V /\ A e. W ) /\ z C_ B ) /\ x e. z ) -> B e. V )
59 simpllr
 |-  ( ( ( ( B e. V /\ A e. W ) /\ z C_ B ) /\ x e. z ) -> A e. W )
60 simpr
 |-  ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> z C_ B )
61 60 sselda
 |-  ( ( ( ( B e. V /\ A e. W ) /\ z C_ B ) /\ x e. z ) -> x e. B )
62 elrestr
 |-  ( ( B e. V /\ A e. W /\ x e. B ) -> ( x i^i A ) e. ( B |`t A ) )
63 58 59 61 62 syl3anc
 |-  ( ( ( ( B e. V /\ A e. W ) /\ z C_ B ) /\ x e. z ) -> ( x i^i A ) e. ( B |`t A ) )
64 63 fmpttd
 |-  ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> ( x e. z |-> ( x i^i A ) ) : z --> ( B |`t A ) )
65 64 frnd
 |-  ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> ran ( x e. z |-> ( x i^i A ) ) C_ ( B |`t A ) )
66 eltg3i
 |-  ( ( ( B |`t A ) e. _V /\ ran ( x e. z |-> ( x i^i A ) ) C_ ( B |`t A ) ) -> U. ran ( x e. z |-> ( x i^i A ) ) e. ( topGen ` ( B |`t A ) ) )
67 1 65 66 sylancr
 |-  ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> U. ran ( x e. z |-> ( x i^i A ) ) e. ( topGen ` ( B |`t A ) ) )
68 26 67 eqeltrid
 |-  ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> U_ x e. z ( x i^i A ) e. ( topGen ` ( B |`t A ) ) )
69 57 68 eqeltrid
 |-  ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> ( U. z i^i A ) e. ( topGen ` ( B |`t A ) ) )
70 ineq1
 |-  ( w = U. z -> ( w i^i A ) = ( U. z i^i A ) )
71 70 eleq1d
 |-  ( w = U. z -> ( ( w i^i A ) e. ( topGen ` ( B |`t A ) ) <-> ( U. z i^i A ) e. ( topGen ` ( B |`t A ) ) ) )
72 69 71 syl5ibrcom
 |-  ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> ( w = U. z -> ( w i^i A ) e. ( topGen ` ( B |`t A ) ) ) )
73 72 expimpd
 |-  ( ( B e. V /\ A e. W ) -> ( ( z C_ B /\ w = U. z ) -> ( w i^i A ) e. ( topGen ` ( B |`t A ) ) ) )
74 73 exlimdv
 |-  ( ( B e. V /\ A e. W ) -> ( E. z ( z C_ B /\ w = U. z ) -> ( w i^i A ) e. ( topGen ` ( B |`t A ) ) ) )
75 55 74 sylbid
 |-  ( ( B e. V /\ A e. W ) -> ( w e. ( topGen ` B ) -> ( w i^i A ) e. ( topGen ` ( B |`t A ) ) ) )
76 75 imp
 |-  ( ( ( B e. V /\ A e. W ) /\ w e. ( topGen ` B ) ) -> ( w i^i A ) e. ( topGen ` ( B |`t A ) ) )
77 76 fmpttd
 |-  ( ( B e. V /\ A e. W ) -> ( w e. ( topGen ` B ) |-> ( w i^i A ) ) : ( topGen ` B ) --> ( topGen ` ( B |`t A ) ) )
78 77 frnd
 |-  ( ( B e. V /\ A e. W ) -> ran ( w e. ( topGen ` B ) |-> ( w i^i A ) ) C_ ( topGen ` ( B |`t A ) ) )
79 53 78 eqsstrd
 |-  ( ( B e. V /\ A e. W ) -> ( ( topGen ` B ) |`t A ) C_ ( topGen ` ( B |`t A ) ) )
80 51 79 eqssd
 |-  ( ( B e. V /\ A e. W ) -> ( topGen ` ( B |`t A ) ) = ( ( topGen ` B ) |`t A ) )