# Metamath Proof Explorer

## Theorem elpt

Description: Elementhood in the bases of a 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 elpt ${⊢}{S}\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 {S}=\underset{{y}\in {A}}{⨉}{h}\left({y}\right)\right)$

### 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 eleq2i ${⊢}{S}\in {B}↔{S}\in \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\}$
3 simpr ${⊢}\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 {S}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)\to {S}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)$
4 ixpexg ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \mathrm{V}\to \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\in \mathrm{V}$
5 fvexd ${⊢}{y}\in {A}\to {g}\left({y}\right)\in \mathrm{V}$
6 4 5 mprg ${⊢}\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\in \mathrm{V}$
7 3 6 eqeltrdi ${⊢}\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 {S}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)\to {S}\in \mathrm{V}$
8 7 exlimiv ${⊢}\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 {S}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)\to {S}\in \mathrm{V}$
9 eqeq1 ${⊢}{x}={S}\to \left({x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)↔{S}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)$
10 9 anbi2d ${⊢}{x}={S}\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)↔\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 {S}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)\right)$
11 10 exbidv ${⊢}{x}={S}\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)↔\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 {S}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)\right)$
12 8 11 elab3 ${⊢}{S}\in \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\}↔\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 {S}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)$
13 fneq1 ${⊢}{g}={h}\to \left({g}Fn{A}↔{h}Fn{A}\right)$
14 fveq1 ${⊢}{g}={h}\to {g}\left({y}\right)={h}\left({y}\right)$
15 14 eleq1d ${⊢}{g}={h}\to \left({g}\left({y}\right)\in {F}\left({y}\right)↔{h}\left({y}\right)\in {F}\left({y}\right)\right)$
16 15 ralbidv ${⊢}{g}={h}\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in {F}\left({y}\right)↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{h}\left({y}\right)\in {F}\left({y}\right)\right)$
17 14 eqeq1d ${⊢}{g}={h}\to \left({g}\left({y}\right)=\bigcup {F}\left({y}\right)↔{h}\left({y}\right)=\bigcup {F}\left({y}\right)\right)$
18 17 rexralbidv ${⊢}{g}={h}\to \left(\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)↔\exists {z}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {z}\right)\phantom{\rule{.4em}{0ex}}{h}\left({y}\right)=\bigcup {F}\left({y}\right)\right)$
19 difeq2 ${⊢}{z}={w}\to {A}\setminus {z}={A}\setminus {w}$
20 19 raleqdv ${⊢}{z}={w}\to \left(\forall {y}\in \left({A}\setminus {z}\right)\phantom{\rule{.4em}{0ex}}{h}\left({y}\right)=\bigcup {F}\left({y}\right)↔\forall {y}\in \left({A}\setminus {w}\right)\phantom{\rule{.4em}{0ex}}{h}\left({y}\right)=\bigcup {F}\left({y}\right)\right)$
21 20 cbvrexvw ${⊢}\exists {z}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\forall {y}\in \left({A}\setminus {z}\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}}{h}\left({y}\right)=\bigcup {F}\left({y}\right)$
22 18 21 syl6bb ${⊢}{g}={h}\to \left(\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)↔\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)$
23 13 16 22 3anbi123d ${⊢}{g}={h}\to \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)↔\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)\right)$
24 14 ixpeq2dv ${⊢}{g}={h}\to \underset{{y}\in {A}}{⨉}{g}\left({y}\right)=\underset{{y}\in {A}}{⨉}{h}\left({y}\right)$
25 24 eqeq2d ${⊢}{g}={h}\to \left({S}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)↔{S}=\underset{{y}\in {A}}{⨉}{h}\left({y}\right)\right)$
26 23 25 anbi12d ${⊢}{g}={h}\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 {S}=\underset{{y}\in {A}}{⨉}{g}\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 {S}=\underset{{y}\in {A}}{⨉}{h}\left({y}\right)\right)\right)$
27 26 cbvexvw ${⊢}\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 {S}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)↔\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 {S}=\underset{{y}\in {A}}{⨉}{h}\left({y}\right)\right)$
28 2 12 27 3bitri ${⊢}{S}\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 {S}=\underset{{y}\in {A}}{⨉}{h}\left({y}\right)\right)$