Step | Hyp | Ref
| Expression |
1 | | ovex 6577 |
. . . . 5
⊢ (𝐵 ↾t 𝐴) ∈ V |
2 | | eltg3 20577 |
. . . . 5
⊢ ((𝐵 ↾t 𝐴) ∈ V → (𝑥 ∈ (topGen‘(𝐵 ↾t 𝐴)) ↔ ∃𝑦(𝑦 ⊆ (𝐵 ↾t 𝐴) ∧ 𝑥 = ∪ 𝑦))) |
3 | 1, 2 | ax-mp 5 |
. . . 4
⊢ (𝑥 ∈ (topGen‘(𝐵 ↾t 𝐴)) ↔ ∃𝑦(𝑦 ⊆ (𝐵 ↾t 𝐴) ∧ 𝑥 = ∪ 𝑦)) |
4 | | simpll 786 |
. . . . . . . . 9
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑦 ⊆ (𝐵 ↾t 𝐴)) → 𝐵 ∈ 𝑉) |
5 | | funmpt 5840 |
. . . . . . . . . 10
⊢ Fun
(𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) |
6 | 5 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑦 ⊆ (𝐵 ↾t 𝐴)) → Fun (𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴))) |
7 | | restval 15910 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝐵 ↾t 𝐴) = ran (𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴))) |
8 | 7 | sseq2d 3596 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑦 ⊆ (𝐵 ↾t 𝐴) ↔ 𝑦 ⊆ ran (𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)))) |
9 | 8 | biimpa 500 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑦 ⊆ (𝐵 ↾t 𝐴)) → 𝑦 ⊆ ran (𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴))) |
10 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
11 | 10 | inex1 4727 |
. . . . . . . . . . . 12
⊢ (𝑥 ∩ 𝐴) ∈ V |
12 | 11 | rgenw 2908 |
. . . . . . . . . . 11
⊢
∀𝑥 ∈
𝐵 (𝑥 ∩ 𝐴) ∈ V |
13 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) = (𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) |
14 | 13 | fnmpt 5933 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝐵 (𝑥 ∩ 𝐴) ∈ V → (𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) Fn 𝐵) |
15 | | fnima 5923 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) Fn 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝐵) = ran (𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴))) |
16 | 12, 14, 15 | mp2b 10 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝐵) = ran (𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) |
17 | 9, 16 | syl6sseqr 3615 |
. . . . . . . . 9
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑦 ⊆ (𝐵 ↾t 𝐴)) → 𝑦 ⊆ ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝐵)) |
18 | | ssimaexg 6174 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑉 ∧ Fun (𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) ∧ 𝑦 ⊆ ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝐵)) → ∃𝑧(𝑧 ⊆ 𝐵 ∧ 𝑦 = ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧))) |
19 | 4, 6, 17, 18 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑦 ⊆ (𝐵 ↾t 𝐴)) → ∃𝑧(𝑧 ⊆ 𝐵 ∧ 𝑦 = ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧))) |
20 | | df-ima 5051 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧) = ran ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) ↾ 𝑧) |
21 | | resmpt 5369 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ⊆ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) ↾ 𝑧) = (𝑥 ∈ 𝑧 ↦ (𝑥 ∩ 𝐴))) |
22 | 21 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) ↾ 𝑧) = (𝑥 ∈ 𝑧 ↦ (𝑥 ∩ 𝐴))) |
23 | 22 | rneqd 5274 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → ran ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) ↾ 𝑧) = ran (𝑥 ∈ 𝑧 ↦ (𝑥 ∩ 𝐴))) |
24 | 20, 23 | syl5eq 2656 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧) = ran (𝑥 ∈ 𝑧 ↦ (𝑥 ∩ 𝐴))) |
25 | 24 | unieqd 4382 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → ∪
((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧) = ∪ ran (𝑥 ∈ 𝑧 ↦ (𝑥 ∩ 𝐴))) |
26 | 11 | dfiun3 5301 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑥 ∈ 𝑧 (𝑥 ∩ 𝐴) = ∪ ran (𝑥 ∈ 𝑧 ↦ (𝑥 ∩ 𝐴)) |
27 | 25, 26 | syl6eqr 2662 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → ∪
((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧) = ∪ 𝑥 ∈ 𝑧 (𝑥 ∩ 𝐴)) |
28 | | iunin1 4521 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑥 ∈ 𝑧 (𝑥 ∩ 𝐴) = (∪
𝑥 ∈ 𝑧 𝑥 ∩ 𝐴) |
29 | 27, 28 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → ∪
((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧) = (∪
𝑥 ∈ 𝑧 𝑥 ∩ 𝐴)) |
30 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢
(topGen‘𝐵)
∈ V |
31 | 30 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → (topGen‘𝐵) ∈ V) |
32 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → 𝐴 ∈ 𝑊) |
33 | 32 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → 𝐴 ∈ 𝑊) |
34 | | uniiun 4509 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑧 =
∪ 𝑥 ∈ 𝑧 𝑥 |
35 | | eltg3i 20576 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑧 ⊆ 𝐵) → ∪ 𝑧 ∈ (topGen‘𝐵)) |
36 | 34, 35 | syl5eqelr 2693 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑧 ⊆ 𝐵) → ∪
𝑥 ∈ 𝑧 𝑥 ∈ (topGen‘𝐵)) |
37 | 36 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → ∪
𝑥 ∈ 𝑧 𝑥 ∈ (topGen‘𝐵)) |
38 | | elrestr 15912 |
. . . . . . . . . . . . . 14
⊢
(((topGen‘𝐵)
∈ V ∧ 𝐴 ∈
𝑊 ∧ ∪ 𝑥 ∈ 𝑧 𝑥 ∈ (topGen‘𝐵)) → (∪ 𝑥 ∈ 𝑧 𝑥 ∩ 𝐴) ∈ ((topGen‘𝐵) ↾t 𝐴)) |
39 | 31, 33, 37, 38 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → (∪ 𝑥 ∈ 𝑧 𝑥 ∩ 𝐴) ∈ ((topGen‘𝐵) ↾t 𝐴)) |
40 | 29, 39 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → ∪
((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧) ∈ ((topGen‘𝐵) ↾t 𝐴)) |
41 | | unieq 4380 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧) → ∪ 𝑦 = ∪
((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧)) |
42 | 41 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (𝑦 = ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧) → (∪ 𝑦 ∈ ((topGen‘𝐵) ↾t 𝐴) ↔ ∪ ((𝑥
∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧) ∈ ((topGen‘𝐵) ↾t 𝐴))) |
43 | 40, 42 | syl5ibrcom 236 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → (𝑦 = ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧) → ∪ 𝑦 ∈ ((topGen‘𝐵) ↾t 𝐴))) |
44 | 43 | expimpd 627 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ((𝑧 ⊆ 𝐵 ∧ 𝑦 = ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧)) → ∪ 𝑦 ∈ ((topGen‘𝐵) ↾t 𝐴))) |
45 | 44 | exlimdv 1848 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (∃𝑧(𝑧 ⊆ 𝐵 ∧ 𝑦 = ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧)) → ∪ 𝑦 ∈ ((topGen‘𝐵) ↾t 𝐴))) |
46 | 45 | adantr 480 |
. . . . . . . 8
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑦 ⊆ (𝐵 ↾t 𝐴)) → (∃𝑧(𝑧 ⊆ 𝐵 ∧ 𝑦 = ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧)) → ∪ 𝑦 ∈ ((topGen‘𝐵) ↾t 𝐴))) |
47 | 19, 46 | mpd 15 |
. . . . . . 7
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑦 ⊆ (𝐵 ↾t 𝐴)) → ∪ 𝑦 ∈ ((topGen‘𝐵) ↾t 𝐴)) |
48 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑥 = ∪
𝑦 → (𝑥 ∈ ((topGen‘𝐵) ↾t 𝐴) ↔ ∪ 𝑦
∈ ((topGen‘𝐵)
↾t 𝐴))) |
49 | 47, 48 | syl5ibrcom 236 |
. . . . . 6
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑦 ⊆ (𝐵 ↾t 𝐴)) → (𝑥 = ∪ 𝑦 → 𝑥 ∈ ((topGen‘𝐵) ↾t 𝐴))) |
50 | 49 | expimpd 627 |
. . . . 5
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ((𝑦 ⊆ (𝐵 ↾t 𝐴) ∧ 𝑥 = ∪ 𝑦) → 𝑥 ∈ ((topGen‘𝐵) ↾t 𝐴))) |
51 | 50 | exlimdv 1848 |
. . . 4
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (∃𝑦(𝑦 ⊆ (𝐵 ↾t 𝐴) ∧ 𝑥 = ∪ 𝑦) → 𝑥 ∈ ((topGen‘𝐵) ↾t 𝐴))) |
52 | 3, 51 | syl5bi 231 |
. . 3
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑥 ∈ (topGen‘(𝐵 ↾t 𝐴)) → 𝑥 ∈ ((topGen‘𝐵) ↾t 𝐴))) |
53 | 52 | ssrdv 3574 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (topGen‘(𝐵 ↾t 𝐴)) ⊆ ((topGen‘𝐵) ↾t 𝐴)) |
54 | | restval 15910 |
. . . 4
⊢
(((topGen‘𝐵)
∈ V ∧ 𝐴 ∈
𝑊) →
((topGen‘𝐵)
↾t 𝐴) =
ran (𝑤 ∈
(topGen‘𝐵) ↦
(𝑤 ∩ 𝐴))) |
55 | 30, 32, 54 | sylancr 694 |
. . 3
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ((topGen‘𝐵) ↾t 𝐴) = ran (𝑤 ∈ (topGen‘𝐵) ↦ (𝑤 ∩ 𝐴))) |
56 | | eltg3 20577 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝑉 → (𝑤 ∈ (topGen‘𝐵) ↔ ∃𝑧(𝑧 ⊆ 𝐵 ∧ 𝑤 = ∪ 𝑧))) |
57 | 56 | adantr 480 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑤 ∈ (topGen‘𝐵) ↔ ∃𝑧(𝑧 ⊆ 𝐵 ∧ 𝑤 = ∪ 𝑧))) |
58 | 34 | ineq1i 3772 |
. . . . . . . . . . . 12
⊢ (∪ 𝑧
∩ 𝐴) = (∪ 𝑥 ∈ 𝑧 𝑥 ∩ 𝐴) |
59 | 58, 28 | eqtr4i 2635 |
. . . . . . . . . . 11
⊢ (∪ 𝑧
∩ 𝐴) = ∪ 𝑥 ∈ 𝑧 (𝑥 ∩ 𝐴) |
60 | | simplll 794 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) ∧ 𝑥 ∈ 𝑧) → 𝐵 ∈ 𝑉) |
61 | | simpllr 795 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) ∧ 𝑥 ∈ 𝑧) → 𝐴 ∈ 𝑊) |
62 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → 𝑧 ⊆ 𝐵) |
63 | 62 | sselda 3568 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) ∧ 𝑥 ∈ 𝑧) → 𝑥 ∈ 𝐵) |
64 | | elrestr 15912 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝑥 ∈ 𝐵) → (𝑥 ∩ 𝐴) ∈ (𝐵 ↾t 𝐴)) |
65 | 60, 61, 63, 64 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) ∧ 𝑥 ∈ 𝑧) → (𝑥 ∩ 𝐴) ∈ (𝐵 ↾t 𝐴)) |
66 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑧 ↦ (𝑥 ∩ 𝐴)) = (𝑥 ∈ 𝑧 ↦ (𝑥 ∩ 𝐴)) |
67 | 65, 66 | fmptd 6292 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → (𝑥 ∈ 𝑧 ↦ (𝑥 ∩ 𝐴)):𝑧⟶(𝐵 ↾t 𝐴)) |
68 | | frn 5966 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑧 ↦ (𝑥 ∩ 𝐴)):𝑧⟶(𝐵 ↾t 𝐴) → ran (𝑥 ∈ 𝑧 ↦ (𝑥 ∩ 𝐴)) ⊆ (𝐵 ↾t 𝐴)) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → ran (𝑥 ∈ 𝑧 ↦ (𝑥 ∩ 𝐴)) ⊆ (𝐵 ↾t 𝐴)) |
70 | | eltg3i 20576 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ↾t 𝐴) ∈ V ∧ ran (𝑥 ∈ 𝑧 ↦ (𝑥 ∩ 𝐴)) ⊆ (𝐵 ↾t 𝐴)) → ∪ ran
(𝑥 ∈ 𝑧 ↦ (𝑥 ∩ 𝐴)) ∈ (topGen‘(𝐵 ↾t 𝐴))) |
71 | 1, 69, 70 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → ∪ ran
(𝑥 ∈ 𝑧 ↦ (𝑥 ∩ 𝐴)) ∈ (topGen‘(𝐵 ↾t 𝐴))) |
72 | 26, 71 | syl5eqel 2692 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → ∪
𝑥 ∈ 𝑧 (𝑥 ∩ 𝐴) ∈ (topGen‘(𝐵 ↾t 𝐴))) |
73 | 59, 72 | syl5eqel 2692 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → (∪ 𝑧 ∩ 𝐴) ∈ (topGen‘(𝐵 ↾t 𝐴))) |
74 | | ineq1 3769 |
. . . . . . . . . . 11
⊢ (𝑤 = ∪
𝑧 → (𝑤 ∩ 𝐴) = (∪ 𝑧 ∩ 𝐴)) |
75 | 74 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑤 = ∪
𝑧 → ((𝑤 ∩ 𝐴) ∈ (topGen‘(𝐵 ↾t 𝐴)) ↔ (∪
𝑧 ∩ 𝐴) ∈ (topGen‘(𝐵 ↾t 𝐴)))) |
76 | 73, 75 | syl5ibrcom 236 |
. . . . . . . . 9
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → (𝑤 = ∪ 𝑧 → (𝑤 ∩ 𝐴) ∈ (topGen‘(𝐵 ↾t 𝐴)))) |
77 | 76 | expimpd 627 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ((𝑧 ⊆ 𝐵 ∧ 𝑤 = ∪ 𝑧) → (𝑤 ∩ 𝐴) ∈ (topGen‘(𝐵 ↾t 𝐴)))) |
78 | 77 | exlimdv 1848 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (∃𝑧(𝑧 ⊆ 𝐵 ∧ 𝑤 = ∪ 𝑧) → (𝑤 ∩ 𝐴) ∈ (topGen‘(𝐵 ↾t 𝐴)))) |
79 | 57, 78 | sylbid 229 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑤 ∈ (topGen‘𝐵) → (𝑤 ∩ 𝐴) ∈ (topGen‘(𝐵 ↾t 𝐴)))) |
80 | 79 | imp 444 |
. . . . 5
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑤 ∈ (topGen‘𝐵)) → (𝑤 ∩ 𝐴) ∈ (topGen‘(𝐵 ↾t 𝐴))) |
81 | | eqid 2610 |
. . . . 5
⊢ (𝑤 ∈ (topGen‘𝐵) ↦ (𝑤 ∩ 𝐴)) = (𝑤 ∈ (topGen‘𝐵) ↦ (𝑤 ∩ 𝐴)) |
82 | 80, 81 | fmptd 6292 |
. . . 4
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑤 ∈ (topGen‘𝐵) ↦ (𝑤 ∩ 𝐴)):(topGen‘𝐵)⟶(topGen‘(𝐵 ↾t 𝐴))) |
83 | | frn 5966 |
. . . 4
⊢ ((𝑤 ∈ (topGen‘𝐵) ↦ (𝑤 ∩ 𝐴)):(topGen‘𝐵)⟶(topGen‘(𝐵 ↾t 𝐴)) → ran (𝑤 ∈ (topGen‘𝐵) ↦ (𝑤 ∩ 𝐴)) ⊆ (topGen‘(𝐵 ↾t 𝐴))) |
84 | 82, 83 | syl 17 |
. . 3
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ran (𝑤 ∈ (topGen‘𝐵) ↦ (𝑤 ∩ 𝐴)) ⊆ (topGen‘(𝐵 ↾t 𝐴))) |
85 | 55, 84 | eqsstrd 3602 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ((topGen‘𝐵) ↾t 𝐴) ⊆ (topGen‘(𝐵 ↾t 𝐴))) |
86 | 53, 85 | eqssd 3585 |
1
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (topGen‘(𝐵 ↾t 𝐴)) = ((topGen‘𝐵) ↾t 𝐴)) |