# Metamath Proof Explorer

## Theorem elptr2

Description: A basic open set in the product topology. (Contributed by Mario Carneiro, 3-Feb-2015)

Ref Expression
Hypotheses 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\}$
elptr2.1 ${⊢}{\phi }\to {A}\in {V}$
elptr2.2 ${⊢}{\phi }\to {W}\in \mathrm{Fin}$
elptr2.3 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {S}\in {F}\left({k}\right)$
elptr2.4 ${⊢}\left({\phi }\wedge {k}\in \left({A}\setminus {W}\right)\right)\to {S}=\bigcup {F}\left({k}\right)$
Assertion elptr2 ${⊢}{\phi }\to \underset{{k}\in {A}}{⨉}{S}\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 elptr2.1 ${⊢}{\phi }\to {A}\in {V}$
3 elptr2.2 ${⊢}{\phi }\to {W}\in \mathrm{Fin}$
4 elptr2.3 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {S}\in {F}\left({k}\right)$
5 elptr2.4 ${⊢}\left({\phi }\wedge {k}\in \left({A}\setminus {W}\right)\right)\to {S}=\bigcup {F}\left({k}\right)$
6 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{S}\right)\left({y}\right)$
7 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{S}\right)\left({k}\right)$
8 fveq2 ${⊢}{y}={k}\to \left({k}\in {A}⟼{S}\right)\left({y}\right)=\left({k}\in {A}⟼{S}\right)\left({k}\right)$
9 6 7 8 cbvixp ${⊢}\underset{{y}\in {A}}{⨉}\left({k}\in {A}⟼{S}\right)\left({y}\right)=\underset{{k}\in {A}}{⨉}\left({k}\in {A}⟼{S}\right)\left({k}\right)$
10 simpr ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {k}\in {A}$
11 eqid ${⊢}\left({k}\in {A}⟼{S}\right)=\left({k}\in {A}⟼{S}\right)$
12 11 fvmpt2 ${⊢}\left({k}\in {A}\wedge {S}\in {F}\left({k}\right)\right)\to \left({k}\in {A}⟼{S}\right)\left({k}\right)={S}$
13 10 4 12 syl2anc ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({k}\in {A}⟼{S}\right)\left({k}\right)={S}$
14 13 ixpeq2dva ${⊢}{\phi }\to \underset{{k}\in {A}}{⨉}\left({k}\in {A}⟼{S}\right)\left({k}\right)=\underset{{k}\in {A}}{⨉}{S}$
15 9 14 syl5eq ${⊢}{\phi }\to \underset{{y}\in {A}}{⨉}\left({k}\in {A}⟼{S}\right)\left({y}\right)=\underset{{k}\in {A}}{⨉}{S}$
16 4 ralrimiva ${⊢}{\phi }\to \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{S}\in {F}\left({k}\right)$
17 11 fnmpt ${⊢}\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{S}\in {F}\left({k}\right)\to \left({k}\in {A}⟼{S}\right)Fn{A}$
18 16 17 syl ${⊢}{\phi }\to \left({k}\in {A}⟼{S}\right)Fn{A}$
19 13 4 eqeltrd ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({k}\in {A}⟼{S}\right)\left({k}\right)\in {F}\left({k}\right)$
20 19 ralrimiva ${⊢}{\phi }\to \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{S}\right)\left({k}\right)\in {F}\left({k}\right)$
21 6 nfel1 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{S}\right)\left({y}\right)\in {F}\left({y}\right)$
22 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{S}\right)\left({k}\right)\in {F}\left({k}\right)$
23 fveq2 ${⊢}{y}={k}\to {F}\left({y}\right)={F}\left({k}\right)$
24 8 23 eleq12d ${⊢}{y}={k}\to \left(\left({k}\in {A}⟼{S}\right)\left({y}\right)\in {F}\left({y}\right)↔\left({k}\in {A}⟼{S}\right)\left({k}\right)\in {F}\left({k}\right)\right)$
25 21 22 24 cbvralw ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{S}\right)\left({y}\right)\in {F}\left({y}\right)↔\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{S}\right)\left({k}\right)\in {F}\left({k}\right)$
26 20 25 sylibr ${⊢}{\phi }\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{S}\right)\left({y}\right)\in {F}\left({y}\right)$
27 eldifi ${⊢}{k}\in \left({A}\setminus {W}\right)\to {k}\in {A}$
28 27 13 sylan2 ${⊢}\left({\phi }\wedge {k}\in \left({A}\setminus {W}\right)\right)\to \left({k}\in {A}⟼{S}\right)\left({k}\right)={S}$
29 28 5 eqtrd ${⊢}\left({\phi }\wedge {k}\in \left({A}\setminus {W}\right)\right)\to \left({k}\in {A}⟼{S}\right)\left({k}\right)=\bigcup {F}\left({k}\right)$
30 29 ralrimiva ${⊢}{\phi }\to \forall {k}\in \left({A}\setminus {W}\right)\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{S}\right)\left({k}\right)=\bigcup {F}\left({k}\right)$
31 6 nfeq1 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{S}\right)\left({y}\right)=\bigcup {F}\left({y}\right)$
32 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{S}\right)\left({k}\right)=\bigcup {F}\left({k}\right)$
33 23 unieqd ${⊢}{y}={k}\to \bigcup {F}\left({y}\right)=\bigcup {F}\left({k}\right)$
34 8 33 eqeq12d ${⊢}{y}={k}\to \left(\left({k}\in {A}⟼{S}\right)\left({y}\right)=\bigcup {F}\left({y}\right)↔\left({k}\in {A}⟼{S}\right)\left({k}\right)=\bigcup {F}\left({k}\right)\right)$
35 31 32 34 cbvralw ${⊢}\forall {y}\in \left({A}\setminus {W}\right)\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{S}\right)\left({y}\right)=\bigcup {F}\left({y}\right)↔\forall {k}\in \left({A}\setminus {W}\right)\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{S}\right)\left({k}\right)=\bigcup {F}\left({k}\right)$
36 30 35 sylibr ${⊢}{\phi }\to \forall {y}\in \left({A}\setminus {W}\right)\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{S}\right)\left({y}\right)=\bigcup {F}\left({y}\right)$
37 1 elptr ${⊢}\left({A}\in {V}\wedge \left(\left({k}\in {A}⟼{S}\right)Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{S}\right)\left({y}\right)\in {F}\left({y}\right)\right)\wedge \left({W}\in \mathrm{Fin}\wedge \forall {y}\in \left({A}\setminus {W}\right)\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{S}\right)\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\to \underset{{y}\in {A}}{⨉}\left({k}\in {A}⟼{S}\right)\left({y}\right)\in {B}$
38 2 18 26 3 36 37 syl122anc ${⊢}{\phi }\to \underset{{y}\in {A}}{⨉}\left({k}\in {A}⟼{S}\right)\left({y}\right)\in {B}$
39 15 38 eqeltrrd ${⊢}{\phi }\to \underset{{k}\in {A}}{⨉}{S}\in {B}$