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 eqtrid ⊢ 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 eqtr4di ⊢ 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 eqtrdi ⊢ 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 biimtrid ⊢ 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