# Metamath Proof Explorer

## Theorem elptr

Description: A basic open set in 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 elptr ${⊢}\left({A}\in {V}\wedge \left({G}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{G}\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}}{G}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\to \underset{{y}\in {A}}{⨉}{G}\left({y}\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 simp2l ${⊢}\left({A}\in {V}\wedge \left({G}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{G}\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}}{G}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\to {G}Fn{A}$
3 simp1 ${⊢}\left({A}\in {V}\wedge \left({G}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{G}\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}}{G}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\to {A}\in {V}$
4 fnex ${⊢}\left({G}Fn{A}\wedge {A}\in {V}\right)\to {G}\in \mathrm{V}$
5 2 3 4 syl2anc ${⊢}\left({A}\in {V}\wedge \left({G}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{G}\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}}{G}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\to {G}\in \mathrm{V}$
6 simp2r ${⊢}\left({A}\in {V}\wedge \left({G}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{G}\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}}{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)$
7 difeq2 ${⊢}{w}={W}\to {A}\setminus {w}={A}\setminus {W}$
8 7 raleqdv ${⊢}{w}={W}\to \left(\forall {y}\in \left({A}\setminus {w}\right)\phantom{\rule{.4em}{0ex}}{G}\left({y}\right)=\bigcup {F}\left({y}\right)↔\forall {y}\in \left({A}\setminus {W}\right)\phantom{\rule{.4em}{0ex}}{G}\left({y}\right)=\bigcup {F}\left({y}\right)\right)$
9 8 rspcev ${⊢}\left({W}\in \mathrm{Fin}\wedge \forall {y}\in \left({A}\setminus {W}\right)\phantom{\rule{.4em}{0ex}}{G}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\to \exists {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {w}\right)\phantom{\rule{.4em}{0ex}}{G}\left({y}\right)=\bigcup {F}\left({y}\right)$
10 9 3ad2ant3 ${⊢}\left({A}\in {V}\wedge \left({G}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{G}\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}}{G}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\to \exists {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {w}\right)\phantom{\rule{.4em}{0ex}}{G}\left({y}\right)=\bigcup {F}\left({y}\right)$
11 2 6 10 3jca ${⊢}\left({A}\in {V}\wedge \left({G}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{G}\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}}{G}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\to \left({G}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{G}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {w}\right)\phantom{\rule{.4em}{0ex}}{G}\left({y}\right)=\bigcup {F}\left({y}\right)\right)$
12 fveq1 ${⊢}{h}={G}\to {h}\left({y}\right)={G}\left({y}\right)$
13 12 eqcomd ${⊢}{h}={G}\to {G}\left({y}\right)={h}\left({y}\right)$
14 13 ixpeq2dv ${⊢}{h}={G}\to \underset{{y}\in {A}}{⨉}{G}\left({y}\right)=\underset{{y}\in {A}}{⨉}{h}\left({y}\right)$
15 14 biantrud ${⊢}{h}={G}\to \left(\left({h}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{h}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {w}\right)\phantom{\rule{.4em}{0ex}}{h}\left({y}\right)=\bigcup {F}\left({y}\right)\right)↔\left(\left({h}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{h}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {w}\right)\phantom{\rule{.4em}{0ex}}{h}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge \underset{{y}\in {A}}{⨉}{G}\left({y}\right)=\underset{{y}\in {A}}{⨉}{h}\left({y}\right)\right)\right)$
16 fneq1 ${⊢}{h}={G}\to \left({h}Fn{A}↔{G}Fn{A}\right)$
17 12 eleq1d ${⊢}{h}={G}\to \left({h}\left({y}\right)\in {F}\left({y}\right)↔{G}\left({y}\right)\in {F}\left({y}\right)\right)$
18 17 ralbidv ${⊢}{h}={G}\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{h}\left({y}\right)\in {F}\left({y}\right)↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{G}\left({y}\right)\in {F}\left({y}\right)\right)$
19 12 eqeq1d ${⊢}{h}={G}\to \left({h}\left({y}\right)=\bigcup {F}\left({y}\right)↔{G}\left({y}\right)=\bigcup {F}\left({y}\right)\right)$
20 19 rexralbidv ${⊢}{h}={G}\to \left(\exists {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {w}\right)\phantom{\rule{.4em}{0ex}}{h}\left({y}\right)=\bigcup {F}\left({y}\right)↔\exists {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {w}\right)\phantom{\rule{.4em}{0ex}}{G}\left({y}\right)=\bigcup {F}\left({y}\right)\right)$
21 16 18 20 3anbi123d ${⊢}{h}={G}\to \left(\left({h}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{h}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {w}\right)\phantom{\rule{.4em}{0ex}}{h}\left({y}\right)=\bigcup {F}\left({y}\right)\right)↔\left({G}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{G}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {w}\right)\phantom{\rule{.4em}{0ex}}{G}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)$
22 15 21 bitr3d ${⊢}{h}={G}\to \left(\left(\left({h}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{h}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {w}\right)\phantom{\rule{.4em}{0ex}}{h}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge \underset{{y}\in {A}}{⨉}{G}\left({y}\right)=\underset{{y}\in {A}}{⨉}{h}\left({y}\right)\right)↔\left({G}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{G}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {w}\right)\phantom{\rule{.4em}{0ex}}{G}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)$
23 5 11 22 spcedv ${⊢}\left({A}\in {V}\wedge \left({G}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{G}\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}}{G}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\to \exists {h}\phantom{\rule{.4em}{0ex}}\left(\left({h}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{h}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {w}\right)\phantom{\rule{.4em}{0ex}}{h}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge \underset{{y}\in {A}}{⨉}{G}\left({y}\right)=\underset{{y}\in {A}}{⨉}{h}\left({y}\right)\right)$
24 1 elpt ${⊢}\underset{{y}\in {A}}{⨉}{G}\left({y}\right)\in {B}↔\exists {h}\phantom{\rule{.4em}{0ex}}\left(\left({h}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{h}\left({y}\right)\in {F}\left({y}\right)\wedge \exists {w}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {w}\right)\phantom{\rule{.4em}{0ex}}{h}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\wedge \underset{{y}\in {A}}{⨉}{G}\left({y}\right)=\underset{{y}\in {A}}{⨉}{h}\left({y}\right)\right)$
25 23 24 sylibr ${⊢}\left({A}\in {V}\wedge \left({G}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{G}\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}}{G}\left({y}\right)=\bigcup {F}\left({y}\right)\right)\right)\to \underset{{y}\in {A}}{⨉}{G}\left({y}\right)\in {B}$