# Metamath Proof Explorer

## Theorem ptuni2

Description: The base set for the product topology. (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 ptuni2 ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\to \underset{{k}\in {A}}{⨉}\bigcup {F}\left({k}\right)=\bigcup {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 ptbasid ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\to \underset{{k}\in {A}}{⨉}\bigcup {F}\left({k}\right)\in {B}$
3 elssuni ${⊢}\underset{{k}\in {A}}{⨉}\bigcup {F}\left({k}\right)\in {B}\to \underset{{k}\in {A}}{⨉}\bigcup {F}\left({k}\right)\subseteq \bigcup {B}$
4 2 3 syl ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\to \underset{{k}\in {A}}{⨉}\bigcup {F}\left({k}\right)\subseteq \bigcup {B}$
5 simpr2 ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \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)\right)\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in {F}\left({y}\right)$
6 elssuni ${⊢}{g}\left({y}\right)\in {F}\left({y}\right)\to {g}\left({y}\right)\subseteq \bigcup {F}\left({y}\right)$
7 6 ralimi ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in {F}\left({y}\right)\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\subseteq \bigcup {F}\left({y}\right)$
8 ss2ixp ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\subseteq \bigcup {F}\left({y}\right)\to \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \underset{{y}\in {A}}{⨉}\bigcup {F}\left({y}\right)$
9 5 7 8 3syl ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \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)\right)\to \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \underset{{y}\in {A}}{⨉}\bigcup {F}\left({y}\right)$
10 fveq2 ${⊢}{y}={k}\to {F}\left({y}\right)={F}\left({k}\right)$
11 10 unieqd ${⊢}{y}={k}\to \bigcup {F}\left({y}\right)=\bigcup {F}\left({k}\right)$
12 11 cbvixpv ${⊢}\underset{{y}\in {A}}{⨉}\bigcup {F}\left({y}\right)=\underset{{k}\in {A}}{⨉}\bigcup {F}\left({k}\right)$
13 9 12 sseqtrdi ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \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)\right)\to \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \underset{{k}\in {A}}{⨉}\bigcup {F}\left({k}\right)$
14 velpw ${⊢}{x}\in 𝒫\underset{{k}\in {A}}{⨉}\bigcup {F}\left({k}\right)↔{x}\subseteq \underset{{k}\in {A}}{⨉}\bigcup {F}\left({k}\right)$
15 sseq1 ${⊢}{x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\to \left({x}\subseteq \underset{{k}\in {A}}{⨉}\bigcup {F}\left({k}\right)↔\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \underset{{k}\in {A}}{⨉}\bigcup {F}\left({k}\right)\right)$
16 14 15 syl5bb ${⊢}{x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\to \left({x}\in 𝒫\underset{{k}\in {A}}{⨉}\bigcup {F}\left({k}\right)↔\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \underset{{k}\in {A}}{⨉}\bigcup {F}\left({k}\right)\right)$
17 13 16 syl5ibrcom ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\wedge \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)\right)\to \left({x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\to {x}\in 𝒫\underset{{k}\in {A}}{⨉}\bigcup {F}\left({k}\right)\right)$
18 17 expimpd ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\to \left(\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)\to {x}\in 𝒫\underset{{k}\in {A}}{⨉}\bigcup {F}\left({k}\right)\right)$
19 18 exlimdv ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\to \left(\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)\to {x}\in 𝒫\underset{{k}\in {A}}{⨉}\bigcup {F}\left({k}\right)\right)$
20 19 abssdv ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\to \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\}\subseteq 𝒫\underset{{k}\in {A}}{⨉}\bigcup {F}\left({k}\right)$
21 1 20 eqsstrid ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\to {B}\subseteq 𝒫\underset{{k}\in {A}}{⨉}\bigcup {F}\left({k}\right)$
22 sspwuni ${⊢}{B}\subseteq 𝒫\underset{{k}\in {A}}{⨉}\bigcup {F}\left({k}\right)↔\bigcup {B}\subseteq \underset{{k}\in {A}}{⨉}\bigcup {F}\left({k}\right)$
23 21 22 sylib ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\to \bigcup {B}\subseteq \underset{{k}\in {A}}{⨉}\bigcup {F}\left({k}\right)$
24 4 23 eqssd ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\to \underset{{k}\in {A}}{⨉}\bigcup {F}\left({k}\right)=\bigcup {B}$