| Step | Hyp | Ref
| Expression |
| 1 | | ovex 7464 |
. . . . 5
⊢ (𝐵 ↾t 𝐴) ∈ V |
| 2 | | eltg3 22969 |
. . . . 5
⊢ ((𝐵 ↾t 𝐴) ∈ V → (𝑥 ∈ (topGen‘(𝐵 ↾t 𝐴)) ↔ ∃𝑦(𝑦 ⊆ (𝐵 ↾t 𝐴) ∧ 𝑥 = ∪ 𝑦))) |
| 3 | 1, 2 | ax-mp 5 |
. . . 4
⊢ (𝑥 ∈ (topGen‘(𝐵 ↾t 𝐴)) ↔ ∃𝑦(𝑦 ⊆ (𝐵 ↾t 𝐴) ∧ 𝑥 = ∪ 𝑦)) |
| 4 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑦 ⊆ (𝐵 ↾t 𝐴)) → 𝐵 ∈ 𝑉) |
| 5 | | funmpt 6604 |
. . . . . . . . . 10
⊢ Fun
(𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) |
| 6 | 5 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑦 ⊆ (𝐵 ↾t 𝐴)) → Fun (𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴))) |
| 7 | | restval 17471 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝐵 ↾t 𝐴) = ran (𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴))) |
| 8 | 7 | sseq2d 4016 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑦 ⊆ (𝐵 ↾t 𝐴) ↔ 𝑦 ⊆ ran (𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)))) |
| 9 | 8 | biimpa 476 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑦 ⊆ (𝐵 ↾t 𝐴)) → 𝑦 ⊆ ran (𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴))) |
| 10 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
| 11 | 10 | inex1 5317 |
. . . . . . . . . . . 12
⊢ (𝑥 ∩ 𝐴) ∈ V |
| 12 | 11 | rgenw 3065 |
. . . . . . . . . . 11
⊢
∀𝑥 ∈
𝐵 (𝑥 ∩ 𝐴) ∈ V |
| 13 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) = (𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) |
| 14 | 13 | fnmpt 6708 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝐵 (𝑥 ∩ 𝐴) ∈ V → (𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) Fn 𝐵) |
| 15 | | fnima 6698 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) Fn 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝐵) = ran (𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴))) |
| 16 | 12, 14, 15 | mp2b 10 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝐵) = ran (𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) |
| 17 | 9, 16 | sseqtrrdi 4025 |
. . . . . . . . 9
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑦 ⊆ (𝐵 ↾t 𝐴)) → 𝑦 ⊆ ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝐵)) |
| 18 | | ssimaexg 6995 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑉 ∧ Fun (𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) ∧ 𝑦 ⊆ ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝐵)) → ∃𝑧(𝑧 ⊆ 𝐵 ∧ 𝑦 = ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧))) |
| 19 | 4, 6, 17, 18 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑦 ⊆ (𝐵 ↾t 𝐴)) → ∃𝑧(𝑧 ⊆ 𝐵 ∧ 𝑦 = ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧))) |
| 20 | | df-ima 5698 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧) = ran ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) ↾ 𝑧) |
| 21 | | resmpt 6055 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ⊆ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) ↾ 𝑧) = (𝑥 ∈ 𝑧 ↦ (𝑥 ∩ 𝐴))) |
| 22 | 21 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) ↾ 𝑧) = (𝑥 ∈ 𝑧 ↦ (𝑥 ∩ 𝐴))) |
| 23 | 22 | rneqd 5949 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → ran ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) ↾ 𝑧) = ran (𝑥 ∈ 𝑧 ↦ (𝑥 ∩ 𝐴))) |
| 24 | 20, 23 | eqtrid 2789 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧) = ran (𝑥 ∈ 𝑧 ↦ (𝑥 ∩ 𝐴))) |
| 25 | 24 | unieqd 4920 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → ∪
((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧) = ∪ ran (𝑥 ∈ 𝑧 ↦ (𝑥 ∩ 𝐴))) |
| 26 | 11 | dfiun3 5980 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑥 ∈ 𝑧 (𝑥 ∩ 𝐴) = ∪ ran (𝑥 ∈ 𝑧 ↦ (𝑥 ∩ 𝐴)) |
| 27 | 25, 26 | eqtr4di 2795 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → ∪
((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧) = ∪ 𝑥 ∈ 𝑧 (𝑥 ∩ 𝐴)) |
| 28 | | iunin1 5072 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑥 ∈ 𝑧 (𝑥 ∩ 𝐴) = (∪
𝑥 ∈ 𝑧 𝑥 ∩ 𝐴) |
| 29 | 27, 28 | eqtrdi 2793 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → ∪
((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧) = (∪
𝑥 ∈ 𝑧 𝑥 ∩ 𝐴)) |
| 30 | | fvex 6919 |
. . . . . . . . . . . . . 14
⊢
(topGen‘𝐵)
∈ V |
| 31 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → 𝐴 ∈ 𝑊) |
| 32 | | uniiun 5058 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑧 =
∪ 𝑥 ∈ 𝑧 𝑥 |
| 33 | | eltg3i 22968 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑧 ⊆ 𝐵) → ∪ 𝑧 ∈ (topGen‘𝐵)) |
| 34 | 32, 33 | eqeltrrid 2846 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑧 ⊆ 𝐵) → ∪
𝑥 ∈ 𝑧 𝑥 ∈ (topGen‘𝐵)) |
| 35 | 34 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → ∪
𝑥 ∈ 𝑧 𝑥 ∈ (topGen‘𝐵)) |
| 36 | | elrestr 17473 |
. . . . . . . . . . . . . 14
⊢
(((topGen‘𝐵)
∈ V ∧ 𝐴 ∈
𝑊 ∧ ∪ 𝑥 ∈ 𝑧 𝑥 ∈ (topGen‘𝐵)) → (∪ 𝑥 ∈ 𝑧 𝑥 ∩ 𝐴) ∈ ((topGen‘𝐵) ↾t 𝐴)) |
| 37 | 30, 31, 35, 36 | mp3an2ani 1470 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → (∪ 𝑥 ∈ 𝑧 𝑥 ∩ 𝐴) ∈ ((topGen‘𝐵) ↾t 𝐴)) |
| 38 | 29, 37 | eqeltrd 2841 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → ∪
((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧) ∈ ((topGen‘𝐵) ↾t 𝐴)) |
| 39 | | unieq 4918 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧) → ∪ 𝑦 = ∪
((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧)) |
| 40 | 39 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ (𝑦 = ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧) → (∪ 𝑦 ∈ ((topGen‘𝐵) ↾t 𝐴) ↔ ∪ ((𝑥
∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧) ∈ ((topGen‘𝐵) ↾t 𝐴))) |
| 41 | 38, 40 | syl5ibrcom 247 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → (𝑦 = ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧) → ∪ 𝑦 ∈ ((topGen‘𝐵) ↾t 𝐴))) |
| 42 | 41 | expimpd 453 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ((𝑧 ⊆ 𝐵 ∧ 𝑦 = ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧)) → ∪ 𝑦 ∈ ((topGen‘𝐵) ↾t 𝐴))) |
| 43 | 42 | exlimdv 1933 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (∃𝑧(𝑧 ⊆ 𝐵 ∧ 𝑦 = ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧)) → ∪ 𝑦 ∈ ((topGen‘𝐵) ↾t 𝐴))) |
| 44 | 43 | adantr 480 |
. . . . . . . 8
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑦 ⊆ (𝐵 ↾t 𝐴)) → (∃𝑧(𝑧 ⊆ 𝐵 ∧ 𝑦 = ((𝑥 ∈ 𝐵 ↦ (𝑥 ∩ 𝐴)) “ 𝑧)) → ∪ 𝑦 ∈ ((topGen‘𝐵) ↾t 𝐴))) |
| 45 | 19, 44 | mpd 15 |
. . . . . . 7
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑦 ⊆ (𝐵 ↾t 𝐴)) → ∪ 𝑦 ∈ ((topGen‘𝐵) ↾t 𝐴)) |
| 46 | | eleq1 2829 |
. . . . . . 7
⊢ (𝑥 = ∪
𝑦 → (𝑥 ∈ ((topGen‘𝐵) ↾t 𝐴) ↔ ∪ 𝑦
∈ ((topGen‘𝐵)
↾t 𝐴))) |
| 47 | 45, 46 | syl5ibrcom 247 |
. . . . . 6
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑦 ⊆ (𝐵 ↾t 𝐴)) → (𝑥 = ∪ 𝑦 → 𝑥 ∈ ((topGen‘𝐵) ↾t 𝐴))) |
| 48 | 47 | expimpd 453 |
. . . . 5
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ((𝑦 ⊆ (𝐵 ↾t 𝐴) ∧ 𝑥 = ∪ 𝑦) → 𝑥 ∈ ((topGen‘𝐵) ↾t 𝐴))) |
| 49 | 48 | exlimdv 1933 |
. . . 4
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (∃𝑦(𝑦 ⊆ (𝐵 ↾t 𝐴) ∧ 𝑥 = ∪ 𝑦) → 𝑥 ∈ ((topGen‘𝐵) ↾t 𝐴))) |
| 50 | 3, 49 | biimtrid 242 |
. . 3
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑥 ∈ (topGen‘(𝐵 ↾t 𝐴)) → 𝑥 ∈ ((topGen‘𝐵) ↾t 𝐴))) |
| 51 | 50 | ssrdv 3989 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (topGen‘(𝐵 ↾t 𝐴)) ⊆ ((topGen‘𝐵) ↾t 𝐴)) |
| 52 | | restval 17471 |
. . . 4
⊢
(((topGen‘𝐵)
∈ V ∧ 𝐴 ∈
𝑊) →
((topGen‘𝐵)
↾t 𝐴) =
ran (𝑤 ∈
(topGen‘𝐵) ↦
(𝑤 ∩ 𝐴))) |
| 53 | 30, 31, 52 | sylancr 587 |
. . 3
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ((topGen‘𝐵) ↾t 𝐴) = ran (𝑤 ∈ (topGen‘𝐵) ↦ (𝑤 ∩ 𝐴))) |
| 54 | | eltg3 22969 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝑉 → (𝑤 ∈ (topGen‘𝐵) ↔ ∃𝑧(𝑧 ⊆ 𝐵 ∧ 𝑤 = ∪ 𝑧))) |
| 55 | 54 | adantr 480 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑤 ∈ (topGen‘𝐵) ↔ ∃𝑧(𝑧 ⊆ 𝐵 ∧ 𝑤 = ∪ 𝑧))) |
| 56 | 32 | ineq1i 4216 |
. . . . . . . . . . . 12
⊢ (∪ 𝑧
∩ 𝐴) = (∪ 𝑥 ∈ 𝑧 𝑥 ∩ 𝐴) |
| 57 | 56, 28 | eqtr4i 2768 |
. . . . . . . . . . 11
⊢ (∪ 𝑧
∩ 𝐴) = ∪ 𝑥 ∈ 𝑧 (𝑥 ∩ 𝐴) |
| 58 | | simplll 775 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) ∧ 𝑥 ∈ 𝑧) → 𝐵 ∈ 𝑉) |
| 59 | | simpllr 776 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) ∧ 𝑥 ∈ 𝑧) → 𝐴 ∈ 𝑊) |
| 60 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → 𝑧 ⊆ 𝐵) |
| 61 | 60 | sselda 3983 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) ∧ 𝑥 ∈ 𝑧) → 𝑥 ∈ 𝐵) |
| 62 | | elrestr 17473 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝑥 ∈ 𝐵) → (𝑥 ∩ 𝐴) ∈ (𝐵 ↾t 𝐴)) |
| 63 | 58, 59, 61, 62 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) ∧ 𝑥 ∈ 𝑧) → (𝑥 ∩ 𝐴) ∈ (𝐵 ↾t 𝐴)) |
| 64 | 63 | fmpttd 7135 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → (𝑥 ∈ 𝑧 ↦ (𝑥 ∩ 𝐴)):𝑧⟶(𝐵 ↾t 𝐴)) |
| 65 | 64 | frnd 6744 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → ran (𝑥 ∈ 𝑧 ↦ (𝑥 ∩ 𝐴)) ⊆ (𝐵 ↾t 𝐴)) |
| 66 | | eltg3i 22968 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ↾t 𝐴) ∈ V ∧ ran (𝑥 ∈ 𝑧 ↦ (𝑥 ∩ 𝐴)) ⊆ (𝐵 ↾t 𝐴)) → ∪ ran
(𝑥 ∈ 𝑧 ↦ (𝑥 ∩ 𝐴)) ∈ (topGen‘(𝐵 ↾t 𝐴))) |
| 67 | 1, 65, 66 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → ∪ ran
(𝑥 ∈ 𝑧 ↦ (𝑥 ∩ 𝐴)) ∈ (topGen‘(𝐵 ↾t 𝐴))) |
| 68 | 26, 67 | eqeltrid 2845 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → ∪
𝑥 ∈ 𝑧 (𝑥 ∩ 𝐴) ∈ (topGen‘(𝐵 ↾t 𝐴))) |
| 69 | 57, 68 | eqeltrid 2845 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → (∪ 𝑧 ∩ 𝐴) ∈ (topGen‘(𝐵 ↾t 𝐴))) |
| 70 | | ineq1 4213 |
. . . . . . . . . . 11
⊢ (𝑤 = ∪
𝑧 → (𝑤 ∩ 𝐴) = (∪ 𝑧 ∩ 𝐴)) |
| 71 | 70 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑤 = ∪
𝑧 → ((𝑤 ∩ 𝐴) ∈ (topGen‘(𝐵 ↾t 𝐴)) ↔ (∪
𝑧 ∩ 𝐴) ∈ (topGen‘(𝐵 ↾t 𝐴)))) |
| 72 | 69, 71 | syl5ibrcom 247 |
. . . . . . . . 9
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑧 ⊆ 𝐵) → (𝑤 = ∪ 𝑧 → (𝑤 ∩ 𝐴) ∈ (topGen‘(𝐵 ↾t 𝐴)))) |
| 73 | 72 | expimpd 453 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ((𝑧 ⊆ 𝐵 ∧ 𝑤 = ∪ 𝑧) → (𝑤 ∩ 𝐴) ∈ (topGen‘(𝐵 ↾t 𝐴)))) |
| 74 | 73 | exlimdv 1933 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (∃𝑧(𝑧 ⊆ 𝐵 ∧ 𝑤 = ∪ 𝑧) → (𝑤 ∩ 𝐴) ∈ (topGen‘(𝐵 ↾t 𝐴)))) |
| 75 | 55, 74 | sylbid 240 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑤 ∈ (topGen‘𝐵) → (𝑤 ∩ 𝐴) ∈ (topGen‘(𝐵 ↾t 𝐴)))) |
| 76 | 75 | imp 406 |
. . . . 5
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) ∧ 𝑤 ∈ (topGen‘𝐵)) → (𝑤 ∩ 𝐴) ∈ (topGen‘(𝐵 ↾t 𝐴))) |
| 77 | 76 | fmpttd 7135 |
. . . 4
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑤 ∈ (topGen‘𝐵) ↦ (𝑤 ∩ 𝐴)):(topGen‘𝐵)⟶(topGen‘(𝐵 ↾t 𝐴))) |
| 78 | 77 | frnd 6744 |
. . 3
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ran (𝑤 ∈ (topGen‘𝐵) ↦ (𝑤 ∩ 𝐴)) ⊆ (topGen‘(𝐵 ↾t 𝐴))) |
| 79 | 53, 78 | eqsstrd 4018 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ((topGen‘𝐵) ↾t 𝐴) ⊆ (topGen‘(𝐵 ↾t 𝐴))) |
| 80 | 51, 79 | eqssd 4001 |
1
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (topGen‘(𝐵 ↾t 𝐴)) = ((topGen‘𝐵) ↾t 𝐴)) |