# Metamath Proof Explorer

## Theorem ptbasin

Description: The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 3-Feb-2015)

Ref Expression
Hypothesis ptbas.1 ${⊢}{B}=\left\{{x}|\exists {g}\phantom{\rule{.4em}{0ex}}\left(\left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {z}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {z}\right)\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge {x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)\right\}$
Assertion ptbasin ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {X}\cap {Y}\in {B}$

### Proof

Step Hyp Ref Expression
1 ptbas.1 ${⊢}{B}=\left\{{x}|\exists {g}\phantom{\rule{.4em}{0ex}}\left(\left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {z}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {z}\right)\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge {x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)\right\}$
2 1 elpt ${⊢}{X}\in {B}↔\exists {a}\phantom{\rule{.4em}{0ex}}\left(\left({a}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {c}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge {X}=\underset{{y}\in {A}}{⨉}{a}\left({y}\right)\right)$
3 1 elpt ${⊢}{Y}\in {B}↔\exists {b}\phantom{\rule{.4em}{0ex}}\left(\left({b}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {d}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge {Y}=\underset{{y}\in {A}}{⨉}{b}\left({y}\right)\right)$
4 2 3 anbi12i ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)↔\left(\exists {a}\phantom{\rule{.4em}{0ex}}\left(\left({a}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {c}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge {X}=\underset{{y}\in {A}}{⨉}{a}\left({y}\right)\right)\wedge \exists {b}\phantom{\rule{.4em}{0ex}}\left(\left({b}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {d}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge {Y}=\underset{{y}\in {A}}{⨉}{b}\left({y}\right)\right)\right)$
5 exdistrv ${⊢}\exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left(\left(\left({a}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {c}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge {X}=\underset{{y}\in {A}}{⨉}{a}\left({y}\right)\right)\wedge \left(\left({b}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {d}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge {Y}=\underset{{y}\in {A}}{⨉}{b}\left({y}\right)\right)\right)↔\left(\exists {a}\phantom{\rule{.4em}{0ex}}\left(\left({a}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {c}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge {X}=\underset{{y}\in {A}}{⨉}{a}\left({y}\right)\right)\wedge \exists {b}\phantom{\rule{.4em}{0ex}}\left(\left({b}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {d}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge {Y}=\underset{{y}\in {A}}{⨉}{b}\left({y}\right)\right)\right)$
6 4 5 bitr4i ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)↔\exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left(\left(\left({a}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {c}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge {X}=\underset{{y}\in {A}}{⨉}{a}\left({y}\right)\right)\wedge \left(\left({b}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {d}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge {Y}=\underset{{y}\in {A}}{⨉}{b}\left({y}\right)\right)\right)$
7 an4 ${⊢}\left(\left(\left({a}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {c}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge {X}=\underset{{y}\in {A}}{⨉}{a}\left({y}\right)\right)\wedge \left(\left({b}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {d}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge {Y}=\underset{{y}\in {A}}{⨉}{b}\left({y}\right)\right)\right)↔\left(\left(\left({a}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {c}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge \left({b}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {d}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\wedge \left({X}=\underset{{y}\in {A}}{⨉}{a}\left({y}\right)\wedge {Y}=\underset{{y}\in {A}}{⨉}{b}\left({y}\right)\right)\right)$
8 an6 ${⊢}\left(\left({a}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {c}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge \left({b}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {d}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)↔\left(\left({a}Fn{A}\wedge {b}Fn{A}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\right)\wedge \left(\exists {c}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \exists {d}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)$
9 df-3an ${⊢}\left(\left({a}Fn{A}\wedge {b}Fn{A}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\right)\wedge \left(\exists {c}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \exists {d}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)↔\left(\left(\left({a}Fn{A}\wedge {b}Fn{A}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\right)\right)\wedge \left(\exists {c}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \exists {d}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)$
10 8 9 bitri ${⊢}\left(\left({a}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {c}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge \left({b}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {d}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)↔\left(\left(\left({a}Fn{A}\wedge {b}Fn{A}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\right)\right)\wedge \left(\exists {c}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \exists {d}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)$
11 reeanv ${⊢}\exists {c}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {d}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)↔\left(\exists {c}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \exists {d}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)$
12 fveq2 ${⊢}{y}={k}\to {a}\left({y}\right)={a}\left({k}\right)$
13 fveq2 ${⊢}{y}={k}\to {b}\left({y}\right)={b}\left({k}\right)$
14 12 13 ineq12d ${⊢}{y}={k}\to {a}\left({y}\right)\cap {b}\left({y}\right)={a}\left({k}\right)\cap {b}\left({k}\right)$
15 14 cbvixpv ${⊢}\underset{{y}\in {A}}{⨉}\left({a}\left({y}\right)\cap {b}\left({y}\right)\right)=\underset{{k}\in {A}}{⨉}\left({a}\left({k}\right)\cap {b}\left({k}\right)\right)$
16 simpl1l ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \left({a}Fn{A}\wedge {b}Fn{A}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\right)\right)\wedge \left(\left({c}\in \mathrm{Fin}\wedge {d}\in \mathrm{Fin}\right)\wedge \left(\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\right)\to {A}\in {V}$
17 unfi ${⊢}\left({c}\in \mathrm{Fin}\wedge {d}\in \mathrm{Fin}\right)\to {c}\cup {d}\in \mathrm{Fin}$
18 17 ad2antrl ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \left({a}Fn{A}\wedge {b}Fn{A}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\right)\right)\wedge \left(\left({c}\in \mathrm{Fin}\wedge {d}\in \mathrm{Fin}\right)\wedge \left(\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\right)\to {c}\cup {d}\in \mathrm{Fin}$
19 simpl1r ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \left({a}Fn{A}\wedge {b}Fn{A}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\right)\right)\wedge \left(\left({c}\in \mathrm{Fin}\wedge {d}\in \mathrm{Fin}\right)\wedge \left(\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\right)\to {F}:{A}⟶\mathrm{Top}$
20 19 ffvelrnda ${⊢}\left(\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \left({a}Fn{A}\wedge {b}Fn{A}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\right)\right)\wedge \left(\left({c}\in \mathrm{Fin}\wedge {d}\in \mathrm{Fin}\right)\wedge \left(\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\right)\wedge {k}\in {A}\right)\to {F}\left({k}\right)\in \mathrm{Top}$
21 simpl3l ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \left({a}Fn{A}\wedge {b}Fn{A}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\right)\right)\wedge \left(\left({c}\in \mathrm{Fin}\wedge {d}\in \mathrm{Fin}\right)\wedge \left(\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\right)\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)$
22 fveq2 ${⊢}{y}={k}\to {F}\left({y}\right)={F}\left({k}\right)$
23 12 22 eleq12d ${⊢}{y}={k}\to \left({a}\left({y}\right)\in {F}\left({y}\right)↔{a}\left({k}\right)\in {F}\left({k}\right)\right)$
24 23 rspccva ${⊢}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge {k}\in {A}\right)\to {a}\left({k}\right)\in {F}\left({k}\right)$
25 21 24 sylan ${⊢}\left(\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \left({a}Fn{A}\wedge {b}Fn{A}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\right)\right)\wedge \left(\left({c}\in \mathrm{Fin}\wedge {d}\in \mathrm{Fin}\right)\wedge \left(\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\right)\wedge {k}\in {A}\right)\to {a}\left({k}\right)\in {F}\left({k}\right)$
26 simpl3r ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \left({a}Fn{A}\wedge {b}Fn{A}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\right)\right)\wedge \left(\left({c}\in \mathrm{Fin}\wedge {d}\in \mathrm{Fin}\right)\wedge \left(\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\right)\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)$
27 13 22 eleq12d ${⊢}{y}={k}\to \left({b}\left({y}\right)\in {F}\left({y}\right)↔{b}\left({k}\right)\in {F}\left({k}\right)\right)$
28 27 rspccva ${⊢}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\wedge {k}\in {A}\right)\to {b}\left({k}\right)\in {F}\left({k}\right)$
29 26 28 sylan ${⊢}\left(\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \left({a}Fn{A}\wedge {b}Fn{A}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\right)\right)\wedge \left(\left({c}\in \mathrm{Fin}\wedge {d}\in \mathrm{Fin}\right)\wedge \left(\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\right)\wedge {k}\in {A}\right)\to {b}\left({k}\right)\in {F}\left({k}\right)$
30 inopn ${⊢}\left({F}\left({k}\right)\in \mathrm{Top}\wedge {a}\left({k}\right)\in {F}\left({k}\right)\wedge {b}\left({k}\right)\in {F}\left({k}\right)\right)\to {a}\left({k}\right)\cap {b}\left({k}\right)\in {F}\left({k}\right)$
31 20 25 29 30 syl3anc ${⊢}\left(\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \left({a}Fn{A}\wedge {b}Fn{A}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\right)\right)\wedge \left(\left({c}\in \mathrm{Fin}\wedge {d}\in \mathrm{Fin}\right)\wedge \left(\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\right)\wedge {k}\in {A}\right)\to {a}\left({k}\right)\cap {b}\left({k}\right)\in {F}\left({k}\right)$
32 simprrl ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \left({a}Fn{A}\wedge {b}Fn{A}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\right)\right)\wedge \left(\left({c}\in \mathrm{Fin}\wedge {d}\in \mathrm{Fin}\right)\wedge \left(\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\right)\to \forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)$
33 ssun1 ${⊢}{c}\subseteq {c}\cup {d}$
34 sscon ${⊢}{c}\subseteq {c}\cup {d}\to {A}\setminus \left({c}\cup {d}\right)\subseteq {A}\setminus {c}$
35 33 34 ax-mp ${⊢}{A}\setminus \left({c}\cup {d}\right)\subseteq {A}\setminus {c}$
36 35 sseli ${⊢}{k}\in \left({A}\setminus \left({c}\cup {d}\right)\right)\to {k}\in \left({A}\setminus {c}\right)$
37 22 unieqd ${⊢}{y}={k}\to \bigcup {F}\left({y}\right)=\bigcup {F}\left({k}\right)$
38 12 37 eqeq12d ${⊢}{y}={k}\to \left({a}\left({y}\right)=\bigcup {F}\left({y}\right)↔{a}\left({k}\right)=\bigcup {F}\left({k}\right)\right)$
39 38 rspccva ${⊢}\left(\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge {k}\in \left({A}\setminus {c}\right)\right)\to {a}\left({k}\right)=\bigcup {F}\left({k}\right)$
40 32 36 39 syl2an ${⊢}\left(\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \left({a}Fn{A}\wedge {b}Fn{A}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\right)\right)\wedge \left(\left({c}\in \mathrm{Fin}\wedge {d}\in \mathrm{Fin}\right)\wedge \left(\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\right)\wedge {k}\in \left({A}\setminus \left({c}\cup {d}\right)\right)\right)\to {a}\left({k}\right)=\bigcup {F}\left({k}\right)$
41 simprrr ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \left({a}Fn{A}\wedge {b}Fn{A}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\right)\right)\wedge \left(\left({c}\in \mathrm{Fin}\wedge {d}\in \mathrm{Fin}\right)\wedge \left(\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\right)\to \forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)$
42 ssun2 ${⊢}{d}\subseteq {c}\cup {d}$
43 sscon ${⊢}{d}\subseteq {c}\cup {d}\to {A}\setminus \left({c}\cup {d}\right)\subseteq {A}\setminus {d}$
44 42 43 ax-mp ${⊢}{A}\setminus \left({c}\cup {d}\right)\subseteq {A}\setminus {d}$
45 44 sseli ${⊢}{k}\in \left({A}\setminus \left({c}\cup {d}\right)\right)\to {k}\in \left({A}\setminus {d}\right)$
46 13 37 eqeq12d ${⊢}{y}={k}\to \left({b}\left({y}\right)=\bigcup {F}\left({y}\right)↔{b}\left({k}\right)=\bigcup {F}\left({k}\right)\right)$
47 46 rspccva ${⊢}\left(\forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge {k}\in \left({A}\setminus {d}\right)\right)\to {b}\left({k}\right)=\bigcup {F}\left({k}\right)$
48 41 45 47 syl2an ${⊢}\left(\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \left({a}Fn{A}\wedge {b}Fn{A}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\right)\right)\wedge \left(\left({c}\in \mathrm{Fin}\wedge {d}\in \mathrm{Fin}\right)\wedge \left(\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\right)\wedge {k}\in \left({A}\setminus \left({c}\cup {d}\right)\right)\right)\to {b}\left({k}\right)=\bigcup {F}\left({k}\right)$
49 40 48 ineq12d ${⊢}\left(\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \left({a}Fn{A}\wedge {b}Fn{A}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\right)\right)\wedge \left(\left({c}\in \mathrm{Fin}\wedge {d}\in \mathrm{Fin}\right)\wedge \left(\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\right)\wedge {k}\in \left({A}\setminus \left({c}\cup {d}\right)\right)\right)\to {a}\left({k}\right)\cap {b}\left({k}\right)=\bigcup {F}\left({k}\right)\cap \bigcup {F}\left({k}\right)$
50 inidm ${⊢}\bigcup {F}\left({k}\right)\cap \bigcup {F}\left({k}\right)=\bigcup {F}\left({k}\right)$
51 49 50 eqtrdi ${⊢}\left(\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \left({a}Fn{A}\wedge {b}Fn{A}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\right)\right)\wedge \left(\left({c}\in \mathrm{Fin}\wedge {d}\in \mathrm{Fin}\right)\wedge \left(\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\right)\wedge {k}\in \left({A}\setminus \left({c}\cup {d}\right)\right)\right)\to {a}\left({k}\right)\cap {b}\left({k}\right)=\bigcup {F}\left({k}\right)$
52 1 16 18 31 51 elptr2 ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \left({a}Fn{A}\wedge {b}Fn{A}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\right)\right)\wedge \left(\left({c}\in \mathrm{Fin}\wedge {d}\in \mathrm{Fin}\right)\wedge \left(\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\right)\to \underset{{k}\in {A}}{⨉}\left({a}\left({k}\right)\cap {b}\left({k}\right)\right)\in {B}$
53 15 52 eqeltrid ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \left({a}Fn{A}\wedge {b}Fn{A}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\right)\right)\wedge \left(\left({c}\in \mathrm{Fin}\wedge {d}\in \mathrm{Fin}\right)\wedge \left(\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\right)\to \underset{{y}\in {A}}{⨉}\left({a}\left({y}\right)\cap {b}\left({y}\right)\right)\in {B}$
54 53 expr ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \left({a}Fn{A}\wedge {b}Fn{A}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\right)\right)\wedge \left({c}\in \mathrm{Fin}\wedge {d}\in \mathrm{Fin}\right)\right)\to \left(\left(\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\to \underset{{y}\in {A}}{⨉}\left({a}\left({y}\right)\cap {b}\left({y}\right)\right)\in {B}\right)$
55 54 rexlimdvva ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \left({a}Fn{A}\wedge {b}Fn{A}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\right)\right)\to \left(\exists {c}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {d}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\to \underset{{y}\in {A}}{⨉}\left({a}\left({y}\right)\cap {b}\left({y}\right)\right)\in {B}\right)$
56 11 55 syl5bir ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \left({a}Fn{A}\wedge {b}Fn{A}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\right)\right)\to \left(\left(\exists {c}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \exists {d}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\to \underset{{y}\in {A}}{⨉}\left({a}\left({y}\right)\cap {b}\left({y}\right)\right)\in {B}\right)$
57 56 3expb ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \left(\left({a}Fn{A}\wedge {b}Fn{A}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\right)\right)\right)\to \left(\left(\exists {c}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \exists {d}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\to \underset{{y}\in {A}}{⨉}\left({a}\left({y}\right)\cap {b}\left({y}\right)\right)\in {B}\right)$
58 57 impr ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \left(\left(\left({a}Fn{A}\wedge {b}Fn{A}\right)\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\right)\right)\wedge \left(\exists {c}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\wedge \exists {d}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\right)\to \underset{{y}\in {A}}{⨉}\left({a}\left({y}\right)\cap {b}\left({y}\right)\right)\in {B}$
59 10 58 sylan2b ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \left(\left({a}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {c}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge \left({b}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {d}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\right)\to \underset{{y}\in {A}}{⨉}\left({a}\left({y}\right)\cap {b}\left({y}\right)\right)\in {B}$
60 ineq12 ${⊢}\left({X}=\underset{{y}\in {A}}{⨉}{a}\left({y}\right)\wedge {Y}=\underset{{y}\in {A}}{⨉}{b}\left({y}\right)\right)\to {X}\cap {Y}=\underset{{y}\in {A}}{⨉}{a}\left({y}\right)\cap \underset{{y}\in {A}}{⨉}{b}\left({y}\right)$
61 ixpin ${⊢}\underset{{y}\in {A}}{⨉}\left({a}\left({y}\right)\cap {b}\left({y}\right)\right)=\underset{{y}\in {A}}{⨉}{a}\left({y}\right)\cap \underset{{y}\in {A}}{⨉}{b}\left({y}\right)$
62 60 61 eqtr4di ${⊢}\left({X}=\underset{{y}\in {A}}{⨉}{a}\left({y}\right)\wedge {Y}=\underset{{y}\in {A}}{⨉}{b}\left({y}\right)\right)\to {X}\cap {Y}=\underset{{y}\in {A}}{⨉}\left({a}\left({y}\right)\cap {b}\left({y}\right)\right)$
63 62 eleq1d ${⊢}\left({X}=\underset{{y}\in {A}}{⨉}{a}\left({y}\right)\wedge {Y}=\underset{{y}\in {A}}{⨉}{b}\left({y}\right)\right)\to \left({X}\cap {Y}\in {B}↔\underset{{y}\in {A}}{⨉}\left({a}\left({y}\right)\cap {b}\left({y}\right)\right)\in {B}\right)$
64 59 63 syl5ibrcom ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \left(\left({a}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {c}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge \left({b}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {d}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\right)\to \left(\left({X}=\underset{{y}\in {A}}{⨉}{a}\left({y}\right)\wedge {Y}=\underset{{y}\in {A}}{⨉}{b}\left({y}\right)\right)\to {X}\cap {Y}\in {B}\right)$
65 64 expimpd ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\to \left(\left(\left(\left({a}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {c}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge \left({b}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {d}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\wedge \left({X}=\underset{{y}\in {A}}{⨉}{a}\left({y}\right)\wedge {Y}=\underset{{y}\in {A}}{⨉}{b}\left({y}\right)\right)\right)\to {X}\cap {Y}\in {B}\right)$
66 7 65 syl5bi ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\to \left(\left(\left(\left({a}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {c}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge {X}=\underset{{y}\in {A}}{⨉}{a}\left({y}\right)\right)\wedge \left(\left({b}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {d}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge {Y}=\underset{{y}\in {A}}{⨉}{b}\left({y}\right)\right)\right)\to {X}\cap {Y}\in {B}\right)$
67 66 exlimdvv ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\to \left(\exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left(\left(\left({a}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {c}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {c}\right)\phantom{\rule{.4em}{0ex}}{a}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge {X}=\underset{{y}\in {A}}{⨉}{a}\left({y}\right)\right)\wedge \left(\left({b}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {d}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {d}\right)\phantom{\rule{.4em}{0ex}}{b}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge {Y}=\underset{{y}\in {A}}{⨉}{b}\left({y}\right)\right)\right)\to {X}\cap {Y}\in {B}\right)$
68 6 67 syl5bi ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\to \left(\left({X}\in {B}\wedge {Y}\in {B}\right)\to {X}\cap {Y}\in {B}\right)$
69 68 imp ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {X}\cap {Y}\in {B}$