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