# 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 ${⊢}\left({B}\in {V}\wedge {A}\in {W}\right)\to \mathrm{topGen}\left({B}{↾}_{𝑡}{A}\right)=\mathrm{topGen}\left({B}\right){↾}_{𝑡}{A}$

### Proof

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