# Metamath Proof Explorer

## Theorem ptbasid

Description: The base set of the product topology is a basic open set. (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 ptbasid ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\to \underset{{k}\in {A}}{⨉}\bigcup {F}\left({k}\right)\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 simpl ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\to {A}\in {V}$
3 0fin ${⊢}\varnothing \in \mathrm{Fin}$
4 3 a1i ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\to \varnothing \in \mathrm{Fin}$
5 ffvelrn ${⊢}\left({F}:{A}⟶\mathrm{Top}\wedge {k}\in {A}\right)\to {F}\left({k}\right)\in \mathrm{Top}$
6 5 adantll ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge {k}\in {A}\right)\to {F}\left({k}\right)\in \mathrm{Top}$
7 eqid ${⊢}\bigcup {F}\left({k}\right)=\bigcup {F}\left({k}\right)$
8 7 topopn ${⊢}{F}\left({k}\right)\in \mathrm{Top}\to \bigcup {F}\left({k}\right)\in {F}\left({k}\right)$
9 6 8 syl ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge {k}\in {A}\right)\to \bigcup {F}\left({k}\right)\in {F}\left({k}\right)$
10 eqidd ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge {k}\in \left({A}\setminus \varnothing \right)\right)\to \bigcup {F}\left({k}\right)=\bigcup {F}\left({k}\right)$
11 1 2 4 9 10 elptr2 ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\to \underset{{k}\in {A}}{⨉}\bigcup {F}\left({k}\right)\in {B}$