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 V A W topGen B 𝑡 A = topGen B 𝑡 A

Proof

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