| Step | Hyp | Ref
| Expression |
| 1 | | firest 17477 |
. . . 4
⊢
(fi‘(({∪
(∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↾t X𝑘 ∈
𝐴 𝑆)) = ((fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ↾t X𝑘 ∈
𝐴 𝑆) |
| 2 | | snex 5436 |
. . . . . . . 8
⊢ {∪ (∏t‘𝐹)} ∈ V |
| 3 | | ptrest.0 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 4 | | fvex 6919 |
. . . . . . . . . . 11
⊢ (𝐹‘𝑢) ∈ V |
| 5 | 4 | rgenw 3065 |
. . . . . . . . . 10
⊢
∀𝑢 ∈
𝐴 (𝐹‘𝑢) ∈ V |
| 6 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) = (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) |
| 7 | 6 | mpoexxg 8100 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑢 ∈ 𝐴 (𝐹‘𝑢) ∈ V) → (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V) |
| 8 | 3, 5, 7 | sylancl 586 |
. . . . . . . . 9
⊢ (𝜑 → (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V) |
| 9 | | rnexg 7924 |
. . . . . . . . 9
⊢ ((𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V → ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V) |
| 10 | 8, 9 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V) |
| 11 | | unexg 7763 |
. . . . . . . 8
⊢ (({∪ (∏t‘𝐹)} ∈ V ∧ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ∈ V) → ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ∈ V) |
| 12 | 2, 10, 11 | sylancr 587 |
. . . . . . 7
⊢ (𝜑 → ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ∈ V) |
| 13 | | ptrest.2 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ∈ 𝑊) |
| 14 | 13 | ralrimiva 3146 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝑆 ∈ 𝑊) |
| 15 | | ixpexg 8962 |
. . . . . . . 8
⊢
(∀𝑘 ∈
𝐴 𝑆 ∈ 𝑊 → X𝑘 ∈ 𝐴 𝑆 ∈ V) |
| 16 | 14, 15 | syl 17 |
. . . . . . 7
⊢ (𝜑 → X𝑘 ∈
𝐴 𝑆 ∈ V) |
| 17 | | restval 17471 |
. . . . . . 7
⊢ ((({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ∈ V ∧ X𝑘 ∈
𝐴 𝑆 ∈ V) → (({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↾t X𝑘 ∈
𝐴 𝑆) = ran (𝑥 ∈ ({∪
(∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆))) |
| 18 | 12, 16, 17 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↾t X𝑘 ∈
𝐴 𝑆) = ran (𝑥 ∈ ({∪
(∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆))) |
| 19 | | mptun 6714 |
. . . . . . . . 9
⊢ (𝑥 ∈ ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = ((𝑥 ∈ {∪
(∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) ∪ (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆))) |
| 20 | 19 | rneqi 5948 |
. . . . . . . 8
⊢ ran
(𝑥 ∈ ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = ran ((𝑥 ∈ {∪
(∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) ∪ (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆))) |
| 21 | | rnun 6165 |
. . . . . . . 8
⊢ ran
((𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) ∪ (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆))) = (ran (𝑥 ∈ {∪
(∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) ∪ ran (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆))) |
| 22 | 20, 21 | eqtri 2765 |
. . . . . . 7
⊢ ran
(𝑥 ∈ ({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = (ran (𝑥 ∈ {∪
(∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) ∪ ran (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆))) |
| 23 | | elsni 4643 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ {∪ (∏t‘𝐹)} → 𝑥 = ∪
(∏t‘𝐹)) |
| 24 | 23 | ineq1d 4219 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ {∪ (∏t‘𝐹)} → (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) = (∪
(∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)) |
| 25 | 24 | mpteq2ia 5245 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = (𝑥 ∈ {∪
(∏t‘𝐹)} ↦ (∪
(∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)) |
| 26 | | fvex 6919 |
. . . . . . . . . . . . . 14
⊢
(∏t‘𝐹) ∈ V |
| 27 | 26 | uniex 7761 |
. . . . . . . . . . . . 13
⊢ ∪ (∏t‘𝐹) ∈ V |
| 28 | 27 | inex1 5317 |
. . . . . . . . . . . . 13
⊢ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆) ∈ V |
| 29 | | fmptsn 7187 |
. . . . . . . . . . . . 13
⊢ ((∪ (∏t‘𝐹) ∈ V ∧ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆) ∈ V) → {〈∪ (∏t‘𝐹), (∪
(∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)〉} = (𝑥 ∈ {∪
(∏t‘𝐹)} ↦ (∪
(∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆))) |
| 30 | 27, 28, 29 | mp2an 692 |
. . . . . . . . . . . 12
⊢
{〈∪ (∏t‘𝐹), (∪
(∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)〉} = (𝑥 ∈ {∪
(∏t‘𝐹)} ↦ (∪
(∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)) |
| 31 | 25, 30 | eqtr4i 2768 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = {〈∪
(∏t‘𝐹), (∪
(∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)〉} |
| 32 | 31 | rneqi 5948 |
. . . . . . . . . 10
⊢ ran
(𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = ran {〈∪
(∏t‘𝐹), (∪
(∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)〉} |
| 33 | 27 | rnsnop 6244 |
. . . . . . . . . 10
⊢ ran
{〈∪ (∏t‘𝐹), (∪
(∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)〉} = {(∪
(∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)} |
| 34 | 32, 33 | eqtri 2765 |
. . . . . . . . 9
⊢ ran
(𝑥 ∈ {∪ (∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = {(∪
(∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)} |
| 35 | | ptrest.1 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:𝐴⟶Top) |
| 36 | 35 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ Top) |
| 37 | | inss1 4237 |
. . . . . . . . . . . . . . 15
⊢ (∪ (𝐹‘𝑘) ∩ 𝑆) ⊆ ∪
(𝐹‘𝑘) |
| 38 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ ∪ (𝐹‘𝑘) = ∪ (𝐹‘𝑘) |
| 39 | 38 | restuni 23170 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑘) ∈ Top ∧ (∪ (𝐹‘𝑘) ∩ 𝑆) ⊆ ∪
(𝐹‘𝑘)) → (∪
(𝐹‘𝑘) ∩ 𝑆) = ∪ ((𝐹‘𝑘) ↾t (∪ (𝐹‘𝑘) ∩ 𝑆))) |
| 40 | 36, 37, 39 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (∪
(𝐹‘𝑘) ∩ 𝑆) = ∪ ((𝐹‘𝑘) ↾t (∪ (𝐹‘𝑘) ∩ 𝑆))) |
| 41 | | fvex 6919 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹‘𝑘) ∈ V |
| 42 | 38 | restin 23174 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘𝑘) ∈ V ∧ 𝑆 ∈ 𝑊) → ((𝐹‘𝑘) ↾t 𝑆) = ((𝐹‘𝑘) ↾t (𝑆 ∩ ∪ (𝐹‘𝑘)))) |
| 43 | 41, 13, 42 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘) ↾t 𝑆) = ((𝐹‘𝑘) ↾t (𝑆 ∩ ∪ (𝐹‘𝑘)))) |
| 44 | | incom 4209 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑆 ∩ ∪ (𝐹‘𝑘)) = (∪ (𝐹‘𝑘) ∩ 𝑆) |
| 45 | 44 | oveq2i 7442 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑘) ↾t (𝑆 ∩ ∪ (𝐹‘𝑘))) = ((𝐹‘𝑘) ↾t (∪ (𝐹‘𝑘) ∩ 𝑆)) |
| 46 | 43, 45 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘) ↾t 𝑆) = ((𝐹‘𝑘) ↾t (∪ (𝐹‘𝑘) ∩ 𝑆))) |
| 47 | 46 | unieqd 4920 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∪
((𝐹‘𝑘) ↾t 𝑆) = ∪
((𝐹‘𝑘) ↾t (∪ (𝐹‘𝑘) ∩ 𝑆))) |
| 48 | 40, 47 | eqtr4d 2780 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (∪
(𝐹‘𝑘) ∩ 𝑆) = ∪ ((𝐹‘𝑘) ↾t 𝑆)) |
| 49 | 48 | ixpeq2dva 8952 |
. . . . . . . . . . . 12
⊢ (𝜑 → X𝑘 ∈
𝐴 (∪ (𝐹‘𝑘) ∩ 𝑆) = X𝑘 ∈ 𝐴 ∪ ((𝐹‘𝑘) ↾t 𝑆)) |
| 50 | | ixpin 8963 |
. . . . . . . . . . . 12
⊢ X𝑘 ∈
𝐴 (∪ (𝐹‘𝑘) ∩ 𝑆) = (X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ∩ X𝑘 ∈ 𝐴 𝑆) |
| 51 | | nfcv 2905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦∪ ((𝐹‘𝑘) ↾t 𝑆) |
| 52 | | nfcv 2905 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘(𝐹‘𝑦) |
| 53 | | nfcv 2905 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘
↾t |
| 54 | | nfcsb1v 3923 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘⦋𝑦 / 𝑘⦌𝑆 |
| 55 | 52, 53, 54 | nfov 7461 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆) |
| 56 | 55 | nfuni 4914 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆) |
| 57 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑦 → (𝐹‘𝑘) = (𝐹‘𝑦)) |
| 58 | | csbeq1a 3913 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑦 → 𝑆 = ⦋𝑦 / 𝑘⦌𝑆) |
| 59 | 57, 58 | oveq12d 7449 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑦 → ((𝐹‘𝑘) ↾t 𝑆) = ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆)) |
| 60 | 59 | unieqd 4920 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑦 → ∪ ((𝐹‘𝑘) ↾t 𝑆) = ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆)) |
| 61 | 51, 56, 60 | cbvixp 8954 |
. . . . . . . . . . . . 13
⊢ X𝑘 ∈
𝐴 ∪ ((𝐹‘𝑘) ↾t 𝑆) = X𝑦 ∈ 𝐴 ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆) |
| 62 | | ixpeq2 8951 |
. . . . . . . . . . . . . 14
⊢
(∀𝑦 ∈
𝐴 ∪ ((𝑘
∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆) → X𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = X𝑦 ∈ 𝐴 ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆)) |
| 63 | | ovex 7464 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆) ∈ V |
| 64 | | nfcv 2905 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘𝑦 |
| 65 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)) = (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)) |
| 66 | 64, 55, 59, 65 | fvmptf 7037 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝐴 ∧ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆) ∈ V) → ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆)) |
| 67 | 63, 66 | mpan2 691 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝐴 → ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆)) |
| 68 | 67 | unieqd 4920 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝐴 → ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆)) |
| 69 | 62, 68 | mprg 3067 |
. . . . . . . . . . . . 13
⊢ X𝑦 ∈
𝐴 ∪ ((𝑘
∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = X𝑦 ∈ 𝐴 ∪ ((𝐹‘𝑦) ↾t ⦋𝑦 / 𝑘⦌𝑆) |
| 70 | 61, 69 | eqtr4i 2768 |
. . . . . . . . . . . 12
⊢ X𝑘 ∈
𝐴 ∪ ((𝐹‘𝑘) ↾t 𝑆) = X𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) |
| 71 | 49, 50, 70 | 3eqtr3g 2800 |
. . . . . . . . . . 11
⊢ (𝜑 → (X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘) ∩ X𝑘 ∈ 𝐴 𝑆) = X𝑦 ∈ 𝐴 ∪ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦)) |
| 72 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(∏t‘𝐹) = (∏t‘𝐹) |
| 73 | 72 | ptuni 23602 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘) = ∪
(∏t‘𝐹)) |
| 74 | 3, 35, 73 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘) = ∪
(∏t‘𝐹)) |
| 75 | 74 | ineq1d 4219 |
. . . . . . . . . . 11
⊢ (𝜑 → (X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘) ∩ X𝑘 ∈ 𝐴 𝑆) = (∪
(∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)) |
| 76 | | resttop 23168 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑘) ∈ Top ∧ 𝑆 ∈ 𝑊) → ((𝐹‘𝑘) ↾t 𝑆) ∈ Top) |
| 77 | 36, 13, 76 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘) ↾t 𝑆) ∈ Top) |
| 78 | 77 | fmpttd 7135 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)):𝐴⟶Top) |
| 79 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) = (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) |
| 80 | 79 | ptuni 23602 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)):𝐴⟶Top) → X𝑦 ∈
𝐴 ∪ ((𝑘
∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))) |
| 81 | 3, 78, 80 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → X𝑦 ∈
𝐴 ∪ ((𝑘
∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑦) = ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))) |
| 82 | 71, 75, 81 | 3eqtr3d 2785 |
. . . . . . . . . 10
⊢ (𝜑 → (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆) = ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))) |
| 83 | 82 | sneqd 4638 |
. . . . . . . . 9
⊢ (𝜑 → {(∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆)} = {∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))}) |
| 84 | 34, 83 | eqtrid 2789 |
. . . . . . . 8
⊢ (𝜑 → ran (𝑥 ∈ {∪
(∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = {∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))}) |
| 85 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑤 ∈ V |
| 86 | 85 | elixp 8944 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ X𝑘 ∈
𝐴 𝑆 ↔ (𝑤 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑤‘𝑘) ∈ 𝑆)) |
| 87 | 86 | simprbi 496 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ X𝑘 ∈
𝐴 𝑆 → ∀𝑘 ∈ 𝐴 (𝑤‘𝑘) ∈ 𝑆) |
| 88 | | nfcsb1v 3923 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑘⦋𝑢 / 𝑘⦌𝑆 |
| 89 | 88 | nfel2 2924 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑘(𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆 |
| 90 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = 𝑢 → (𝑤‘𝑘) = (𝑤‘𝑢)) |
| 91 | | csbeq1a 3913 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = 𝑢 → 𝑆 = ⦋𝑢 / 𝑘⦌𝑆) |
| 92 | 90, 91 | eleq12d 2835 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = 𝑢 → ((𝑤‘𝑘) ∈ 𝑆 ↔ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)) |
| 93 | 89, 92 | rspc 3610 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 (𝑤‘𝑘) ∈ 𝑆 → (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)) |
| 94 | 87, 93 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 ∈ 𝐴 → (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 → (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)) |
| 95 | 94 | pm4.71d 561 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 ∈ 𝐴 → (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ↔ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆))) |
| 96 | 95 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ 𝐴 → (((𝑤 ∈ ∪
(∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ↔ ((𝑤 ∈ ∪
(∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)))) |
| 97 | | an4 656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)) ↔ ((𝑤 ∈ ∪
(∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ ((𝑤‘𝑢) ∈ 𝑣 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆))) |
| 98 | | elin 3967 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆) ↔ ((𝑤‘𝑢) ∈ 𝑣 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)) |
| 99 | 98 | anbi2i 623 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) ↔ ((𝑤 ∈ ∪
(∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ ((𝑤‘𝑢) ∈ 𝑣 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆))) |
| 100 | 97, 99 | bitr4i 278 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ∪ (∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ (𝑤 ∈ X𝑘 ∈ 𝐴 𝑆 ∧ (𝑤‘𝑢) ∈ ⦋𝑢 / 𝑘⦌𝑆)) ↔ ((𝑤 ∈ ∪
(∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))) |
| 101 | 96, 100 | bitrdi 287 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ 𝐴 → (((𝑤 ∈ ∪
(∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ↔ ((𝑤 ∈ ∪
(∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)))) |
| 102 | | elin 3967 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ (∪ (∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ (𝑤 ∈ ∪
(∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆)) |
| 103 | 82 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑤 ∈ (∪
(∏t‘𝐹) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ 𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))))) |
| 104 | 102, 103 | bitr3id 285 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑤 ∈ ∪
(∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ↔ 𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))))) |
| 105 | 104 | anbi1d 631 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝑤 ∈ ∪
(∏t‘𝐹) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) ↔ (𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)))) |
| 106 | 101, 105 | sylan9bbr 510 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (((𝑤 ∈ ∪
(∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆) ↔ (𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)))) |
| 107 | 106 | abbidv 2808 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → {𝑤 ∣ ((𝑤 ∈ ∪
(∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆)} = {𝑤 ∣ (𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))}) |
| 108 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) = (𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) |
| 109 | 108 | mptpreima 6258 |
. . . . . . . . . . . . . . . . . . 19
⊢ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) = {𝑤 ∈ ∪
(∏t‘𝐹) ∣ (𝑤‘𝑢) ∈ 𝑣} |
| 110 | | df-rab 3437 |
. . . . . . . . . . . . . . . . . . 19
⊢ {𝑤 ∈ ∪ (∏t‘𝐹) ∣ (𝑤‘𝑢) ∈ 𝑣} = {𝑤 ∣ (𝑤 ∈ ∪
(∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣)} |
| 111 | 109, 110 | eqtr2i 2766 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑤 ∣ (𝑤 ∈ ∪
(∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣)} = (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) |
| 112 | | abid2 2879 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑤 ∣ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆} = X𝑘 ∈ 𝐴 𝑆 |
| 113 | 111, 112 | ineq12i 4218 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑤 ∣ (𝑤 ∈ ∪
(∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣)} ∩ {𝑤 ∣ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆}) = ((◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) |
| 114 | | inab 4309 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑤 ∣ (𝑤 ∈ ∪
(∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣)} ∩ {𝑤 ∣ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆}) = {𝑤 ∣ ((𝑤 ∈ ∪
(∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆)} |
| 115 | 113, 114 | eqtr3i 2767 |
. . . . . . . . . . . . . . . 16
⊢ ((◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) = {𝑤 ∣ ((𝑤 ∈ ∪
(∏t‘𝐹) ∧ (𝑤‘𝑢) ∈ 𝑣) ∧ 𝑤 ∈ X𝑘 ∈ 𝐴 𝑆)} |
| 116 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) = (𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) |
| 117 | 116 | mptpreima 6258 |
. . . . . . . . . . . . . . . . 17
⊢ (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) = {𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∣ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)} |
| 118 | | df-rab 3437 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑤 ∈ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∣ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)} = {𝑤 ∣ (𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))} |
| 119 | 117, 118 | eqtri 2765 |
. . . . . . . . . . . . . . . 16
⊢ (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) = {𝑤 ∣ (𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ∧ (𝑤‘𝑢) ∈ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))} |
| 120 | 107, 115,
119 | 3eqtr4g 2802 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → ((◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) = (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆))) |
| 121 | 120 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (𝑥 = ((◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ 𝑥 = (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)))) |
| 122 | 121 | rexbidv 3179 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)))) |
| 123 | | ineq1 4213 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = 𝑦 → (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆) = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)) |
| 124 | 123 | imaeq2d 6078 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 𝑦 → (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) = (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))) |
| 125 | 124 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝑦 → (𝑥 = (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) ↔ 𝑥 = (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))) |
| 126 | 125 | cbvrexvw 3238 |
. . . . . . . . . . . . 13
⊢
(∃𝑣 ∈
(𝐹‘𝑢)𝑥 = (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑣 ∩ ⦋𝑢 / 𝑘⦌𝑆)) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑥 = (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))) |
| 127 | 122, 126 | bitrdi 287 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑥 = (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))) |
| 128 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V |
| 129 | 128 | inex1 5317 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆) ∈ V |
| 130 | 129 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑦 ∈ (𝐹‘𝑢)) → (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆) ∈ V) |
| 131 | | ovex 7464 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆) ∈ V |
| 132 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘𝑢 |
| 133 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑘(𝐹‘𝑢) |
| 134 | 133, 53, 88 | nfov 7461 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆) |
| 135 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑢 → (𝐹‘𝑘) = (𝐹‘𝑢)) |
| 136 | 135, 91 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑢 → ((𝐹‘𝑘) ↾t 𝑆) = ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆)) |
| 137 | 132, 134,
136, 65 | fvmptf 7037 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ 𝐴 ∧ ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆) ∈ V) → ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) = ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆)) |
| 138 | 131, 137 | mpan2 691 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ 𝐴 → ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) = ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆)) |
| 139 | 138 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) = ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆)) |
| 140 | 139 | eleq2d 2827 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↔ 𝑣 ∈ ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆))) |
| 141 | | nfv 1914 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘(𝜑 ∧ 𝑢 ∈ 𝐴) |
| 142 | | nfcsb1v 3923 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘⦋𝑢 / 𝑘⦌𝑊 |
| 143 | 88, 142 | nfel 2920 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊 |
| 144 | 141, 143 | nfim 1896 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘((𝜑 ∧ 𝑢 ∈ 𝐴) → ⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊) |
| 145 | | eleq1w 2824 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑢 → (𝑘 ∈ 𝐴 ↔ 𝑢 ∈ 𝐴)) |
| 146 | 145 | anbi2d 630 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑢 → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ 𝑢 ∈ 𝐴))) |
| 147 | | csbeq1a 3913 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑢 → 𝑊 = ⦋𝑢 / 𝑘⦌𝑊) |
| 148 | 91, 147 | eleq12d 2835 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑢 → (𝑆 ∈ 𝑊 ↔ ⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊)) |
| 149 | 146, 148 | imbi12d 344 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑢 → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ∈ 𝑊) ↔ ((𝜑 ∧ 𝑢 ∈ 𝐴) → ⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊))) |
| 150 | 144, 149,
13 | chvarfv 2240 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → ⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊) |
| 151 | | elrest 17472 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑢) ∈ V ∧ ⦋𝑢 / 𝑘⦌𝑆 ∈ ⦋𝑢 / 𝑘⦌𝑊) → (𝑣 ∈ ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))) |
| 152 | 4, 150, 151 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (𝑣 ∈ ((𝐹‘𝑢) ↾t ⦋𝑢 / 𝑘⦌𝑆) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))) |
| 153 | 140, 152 | bitrd 279 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))) |
| 154 | | imaeq2 6074 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆) → (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣) = (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆))) |
| 155 | 154 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆) → (𝑥 = (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣) ↔ 𝑥 = (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))) |
| 156 | 155 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐴) ∧ 𝑣 = (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)) → (𝑥 = (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣) ↔ 𝑥 = (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))) |
| 157 | 130, 153,
156 | rexxfr2d 5411 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (∃𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢)𝑥 = (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣) ↔ ∃𝑦 ∈ (𝐹‘𝑢)𝑥 = (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ (𝑦 ∩ ⦋𝑢 / 𝑘⦌𝑆)))) |
| 158 | 127, 157 | bitr4d 282 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢)𝑥 = (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))) |
| 159 | 158 | rexbidva 3177 |
. . . . . . . . . 10
⊢ (𝜑 → (∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢)𝑥 = (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))) |
| 160 | 159 | abbidv 2808 |
. . . . . . . . 9
⊢ (𝜑 → {𝑥 ∣ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)} = {𝑥 ∣ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢)𝑥 = (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)}) |
| 161 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) |
| 162 | 161 | rnmpt 5968 |
. . . . . . . . . 10
⊢ ran
(𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = {𝑦 ∣ ∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)} |
| 163 | | nfre1 3285 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) |
| 164 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) |
| 165 | 27 | mptex 7243 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ∪ (∏t‘𝐹) ↦ (𝑤‘𝑢)) ∈ V |
| 166 | 165 | cnvex 7947 |
. . . . . . . . . . . . . . 15
⊢ ◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) ∈ V |
| 167 | 166 | imaex 7936 |
. . . . . . . . . . . . . 14
⊢ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∈ V |
| 168 | 167 | rgen2w 3066 |
. . . . . . . . . . . . 13
⊢
∀𝑢 ∈
𝐴 ∀𝑣 ∈ (𝐹‘𝑢)(◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∈ V |
| 169 | | ineq1 4213 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) → (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) = ((◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)) |
| 170 | 169 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) → (𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) ↔ 𝑦 = ((◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆))) |
| 171 | 6, 170 | rexrnmpo 7573 |
. . . . . . . . . . . . 13
⊢
(∀𝑢 ∈
𝐴 ∀𝑣 ∈ (𝐹‘𝑢)(◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∈ V → (∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑦 = ((◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆))) |
| 172 | 168, 171 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(∃𝑥 ∈ ran
(𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑦 = ((◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)) |
| 173 | | eqeq1 2741 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑥 → (𝑦 = ((◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ 𝑥 = ((◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆))) |
| 174 | 173 | 2rexbidv 3222 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → (∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑦 = ((◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆))) |
| 175 | 172, 174 | bitrid 283 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆) ↔ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆))) |
| 176 | 163, 164,
175 | cbvabw 2813 |
. . . . . . . . . 10
⊢ {𝑦 ∣ ∃𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))𝑦 = (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)} = {𝑥 ∣ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)} |
| 177 | 162, 176 | eqtri 2765 |
. . . . . . . . 9
⊢ ran
(𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = {𝑥 ∣ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ (𝐹‘𝑢)𝑥 = ((◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣) ∩ X𝑘 ∈ 𝐴 𝑆)} |
| 178 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)) = (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)) |
| 179 | 178 | rnmpo 7566 |
. . . . . . . . 9
⊢ ran
(𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)) = {𝑥 ∣ ∃𝑢 ∈ 𝐴 ∃𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢)𝑥 = (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)} |
| 180 | 160, 177,
179 | 3eqtr4g 2802 |
. . . . . . . 8
⊢ (𝜑 → ran (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))) |
| 181 | 84, 180 | uneq12d 4169 |
. . . . . . 7
⊢ (𝜑 → (ran (𝑥 ∈ {∪
(∏t‘𝐹)} ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) ∪ ran (𝑥 ∈ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆))) = ({∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)))) |
| 182 | 22, 181 | eqtrid 2789 |
. . . . . 6
⊢ (𝜑 → ran (𝑥 ∈ ({∪
(∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↦ (𝑥 ∩ X𝑘 ∈ 𝐴 𝑆)) = ({∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)))) |
| 183 | 18, 182 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → (({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↾t X𝑘 ∈
𝐴 𝑆) = ({∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)))) |
| 184 | 183 | fveq2d 6910 |
. . . 4
⊢ (𝜑 → (fi‘(({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))) ↾t X𝑘 ∈
𝐴 𝑆)) = (fi‘({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))))) |
| 185 | 1, 184 | eqtr3id 2791 |
. . 3
⊢ (𝜑 → ((fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ↾t X𝑘 ∈
𝐴 𝑆) = (fi‘({∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣))))) |
| 186 | 185 | fveq2d 6910 |
. 2
⊢ (𝜑 →
(topGen‘((fi‘({∪
(∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ↾t X𝑘 ∈
𝐴 𝑆)) = (topGen‘(fi‘({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)))))) |
| 187 | | eqid 2737 |
. . . . . 6
⊢ ∪ (∏t‘𝐹) = ∪
(∏t‘𝐹) |
| 188 | 72, 187, 6 | ptval2 23609 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) →
(∏t‘𝐹) = (topGen‘(fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))))) |
| 189 | 3, 35, 188 | syl2anc 584 |
. . . 4
⊢ (𝜑 →
(∏t‘𝐹) = (topGen‘(fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))))) |
| 190 | 189 | oveq1d 7446 |
. . 3
⊢ (𝜑 →
((∏t‘𝐹) ↾t X𝑘 ∈
𝐴 𝑆) = ((topGen‘(fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))))) ↾t X𝑘 ∈
𝐴 𝑆)) |
| 191 | | fvex 6919 |
. . . 4
⊢
(fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ∈ V |
| 192 | | tgrest 23167 |
. . . 4
⊢
(((fi‘({∪
(∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ∈ V ∧ X𝑘 ∈
𝐴 𝑆 ∈ V) →
(topGen‘((fi‘({∪
(∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ↾t X𝑘 ∈
𝐴 𝑆)) = ((topGen‘(fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))))) ↾t X𝑘 ∈
𝐴 𝑆)) |
| 193 | 191, 16, 192 | sylancr 587 |
. . 3
⊢ (𝜑 →
(topGen‘((fi‘({∪
(∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ↾t X𝑘 ∈
𝐴 𝑆)) = ((topGen‘(fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣))))) ↾t X𝑘 ∈
𝐴 𝑆)) |
| 194 | 190, 193 | eqtr4d 2780 |
. 2
⊢ (𝜑 →
((∏t‘𝐹) ↾t X𝑘 ∈
𝐴 𝑆) = (topGen‘((fi‘({∪ (∏t‘𝐹)} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ (𝐹‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘𝐹) ↦ (𝑤‘𝑢)) “ 𝑣)))) ↾t X𝑘 ∈
𝐴 𝑆))) |
| 195 | | eqid 2737 |
. . . 4
⊢ ∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) = ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) |
| 196 | 79, 195, 178 | ptval2 23609 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)):𝐴⟶Top) →
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) = (topGen‘(fi‘({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)))))) |
| 197 | 3, 78, 196 | syl2anc 584 |
. 2
⊢ (𝜑 →
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) = (topGen‘(fi‘({∪ (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))} ∪ ran (𝑢 ∈ 𝐴, 𝑣 ∈ ((𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))‘𝑢) ↦ (◡(𝑤 ∈ ∪
(∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))) ↦ (𝑤‘𝑢)) “ 𝑣)))))) |
| 198 | 186, 194,
197 | 3eqtr4d 2787 |
1
⊢ (𝜑 →
((∏t‘𝐹) ↾t X𝑘 ∈
𝐴 𝑆) = (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))) |