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 ) )