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 ( ( 𝐵𝑉𝐴𝑊 ) → ( topGen ‘ ( 𝐵t 𝐴 ) ) = ( ( topGen ‘ 𝐵 ) ↾t 𝐴 ) )

Proof

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