# Metamath Proof Explorer

## Theorem tmdgsum2

Description: For any neighborhood U of n X , there is a neighborhood u of X such that any sum of n elements in u sums to an element of U . (Contributed by Mario Carneiro, 19-Sep-2015)

Ref Expression
Hypotheses tmdgsum.j ${⊢}{J}=\mathrm{TopOpen}\left({G}\right)$
tmdgsum.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
tmdgsum2.t
tmdgsum2.1 ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
tmdgsum2.2 ${⊢}{\phi }\to {G}\in \mathrm{TopMnd}$
tmdgsum2.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
tmdgsum2.u ${⊢}{\phi }\to {U}\in {J}$
tmdgsum2.x ${⊢}{\phi }\to {X}\in {B}$
tmdgsum2.3
Assertion tmdgsum2 ${⊢}{\phi }\to \exists {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({X}\in {u}\wedge \forall {f}\in \left({{u}}^{{A}}\right)\phantom{\rule{.4em}{0ex}}{\sum }_{{G}}{f}\in {U}\right)$

### Proof

Step Hyp Ref Expression
1 tmdgsum.j ${⊢}{J}=\mathrm{TopOpen}\left({G}\right)$
2 tmdgsum.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
3 tmdgsum2.t
4 tmdgsum2.1 ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
5 tmdgsum2.2 ${⊢}{\phi }\to {G}\in \mathrm{TopMnd}$
6 tmdgsum2.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
7 tmdgsum2.u ${⊢}{\phi }\to {U}\in {J}$
8 tmdgsum2.x ${⊢}{\phi }\to {X}\in {B}$
9 tmdgsum2.3
10 eqid ${⊢}\left({f}\in \left({{B}}^{{A}}\right)⟼{\sum }_{{G}}{f}\right)=\left({f}\in \left({{B}}^{{A}}\right)⟼{\sum }_{{G}}{f}\right)$
11 10 mptpreima ${⊢}{\left({f}\in \left({{B}}^{{A}}\right)⟼{\sum }_{{G}}{f}\right)}^{-1}\left[{U}\right]=\left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}$
12 1 2 tmdgsum ${⊢}\left({G}\in \mathrm{CMnd}\wedge {G}\in \mathrm{TopMnd}\wedge {A}\in \mathrm{Fin}\right)\to \left({f}\in \left({{B}}^{{A}}\right)⟼{\sum }_{{G}}{f}\right)\in \left(\left({J}{^}_{\mathrm{ko}}𝒫{A}\right)\mathrm{Cn}{J}\right)$
13 4 5 6 12 syl3anc ${⊢}{\phi }\to \left({f}\in \left({{B}}^{{A}}\right)⟼{\sum }_{{G}}{f}\right)\in \left(\left({J}{^}_{\mathrm{ko}}𝒫{A}\right)\mathrm{Cn}{J}\right)$
14 cnima ${⊢}\left(\left({f}\in \left({{B}}^{{A}}\right)⟼{\sum }_{{G}}{f}\right)\in \left(\left({J}{^}_{\mathrm{ko}}𝒫{A}\right)\mathrm{Cn}{J}\right)\wedge {U}\in {J}\right)\to {\left({f}\in \left({{B}}^{{A}}\right)⟼{\sum }_{{G}}{f}\right)}^{-1}\left[{U}\right]\in \left({J}{^}_{\mathrm{ko}}𝒫{A}\right)$
15 13 7 14 syl2anc ${⊢}{\phi }\to {\left({f}\in \left({{B}}^{{A}}\right)⟼{\sum }_{{G}}{f}\right)}^{-1}\left[{U}\right]\in \left({J}{^}_{\mathrm{ko}}𝒫{A}\right)$
16 11 15 eqeltrrid ${⊢}{\phi }\to \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\in \left({J}{^}_{\mathrm{ko}}𝒫{A}\right)$
17 1 2 tmdtopon ${⊢}{G}\in \mathrm{TopMnd}\to {J}\in \mathrm{TopOn}\left({B}\right)$
18 topontop ${⊢}{J}\in \mathrm{TopOn}\left({B}\right)\to {J}\in \mathrm{Top}$
19 5 17 18 3syl ${⊢}{\phi }\to {J}\in \mathrm{Top}$
20 xkopt ${⊢}\left({J}\in \mathrm{Top}\wedge {A}\in \mathrm{Fin}\right)\to {J}{^}_{\mathrm{ko}}𝒫{A}={\prod }_{𝑡}\left({A}×\left\{{J}\right\}\right)$
21 19 6 20 syl2anc ${⊢}{\phi }\to {J}{^}_{\mathrm{ko}}𝒫{A}={\prod }_{𝑡}\left({A}×\left\{{J}\right\}\right)$
22 fnconstg ${⊢}{J}\in \mathrm{TopOn}\left({B}\right)\to \left({A}×\left\{{J}\right\}\right)Fn{A}$
23 5 17 22 3syl ${⊢}{\phi }\to \left({A}×\left\{{J}\right\}\right)Fn{A}$
24 eqid ${⊢}\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 \left({A}×\left\{{J}\right\}\right)\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 \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\wedge {x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)\right\}=\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 \left({A}×\left\{{J}\right\}\right)\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 \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\wedge {x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)\right\}$
25 24 ptval ${⊢}\left({A}\in \mathrm{Fin}\wedge \left({A}×\left\{{J}\right\}\right)Fn{A}\right)\to {\prod }_{𝑡}\left({A}×\left\{{J}\right\}\right)=\mathrm{topGen}\left(\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 \left({A}×\left\{{J}\right\}\right)\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 \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\wedge {x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)\right\}\right)$
26 6 23 25 syl2anc ${⊢}{\phi }\to {\prod }_{𝑡}\left({A}×\left\{{J}\right\}\right)=\mathrm{topGen}\left(\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 \left({A}×\left\{{J}\right\}\right)\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 \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\wedge {x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)\right\}\right)$
27 21 26 eqtrd ${⊢}{\phi }\to {J}{^}_{\mathrm{ko}}𝒫{A}=\mathrm{topGen}\left(\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 \left({A}×\left\{{J}\right\}\right)\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 \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\wedge {x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)\right\}\right)$
28 16 27 eleqtrd ${⊢}{\phi }\to \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\in \mathrm{topGen}\left(\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 \left({A}×\left\{{J}\right\}\right)\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 \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\wedge {x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)\right\}\right)$
29 oveq2 ${⊢}{f}={A}×\left\{{X}\right\}\to {\sum }_{{G}}{f}={\sum }_{{G}}\left({A}×\left\{{X}\right\}\right)$
30 29 eleq1d ${⊢}{f}={A}×\left\{{X}\right\}\to \left({\sum }_{{G}}{f}\in {U}↔{\sum }_{{G}}\left({A}×\left\{{X}\right\}\right)\in {U}\right)$
31 fconst6g ${⊢}{X}\in {B}\to \left({A}×\left\{{X}\right\}\right):{A}⟶{B}$
32 8 31 syl ${⊢}{\phi }\to \left({A}×\left\{{X}\right\}\right):{A}⟶{B}$
33 2 fvexi ${⊢}{B}\in \mathrm{V}$
34 elmapg ${⊢}\left({B}\in \mathrm{V}\wedge {A}\in \mathrm{Fin}\right)\to \left({A}×\left\{{X}\right\}\in \left({{B}}^{{A}}\right)↔\left({A}×\left\{{X}\right\}\right):{A}⟶{B}\right)$
35 33 6 34 sylancr ${⊢}{\phi }\to \left({A}×\left\{{X}\right\}\in \left({{B}}^{{A}}\right)↔\left({A}×\left\{{X}\right\}\right):{A}⟶{B}\right)$
36 32 35 mpbird ${⊢}{\phi }\to {A}×\left\{{X}\right\}\in \left({{B}}^{{A}}\right)$
37 fconstmpt ${⊢}{A}×\left\{{X}\right\}=\left({k}\in {A}⟼{X}\right)$
38 37 oveq2i ${⊢}{\sum }_{{G}}\left({A}×\left\{{X}\right\}\right)=\underset{{k}\in {A}}{{\sum }_{{G}}}{X}$
39 cmnmnd ${⊢}{G}\in \mathrm{CMnd}\to {G}\in \mathrm{Mnd}$
40 4 39 syl ${⊢}{\phi }\to {G}\in \mathrm{Mnd}$
41 2 3 gsumconst
42 40 6 8 41 syl3anc
43 38 42 syl5eq
44 43 9 eqeltrd ${⊢}{\phi }\to {\sum }_{{G}}\left({A}×\left\{{X}\right\}\right)\in {U}$
45 30 36 44 elrabd ${⊢}{\phi }\to {A}×\left\{{X}\right\}\in \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}$
46 tg2 ${⊢}\left(\left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\in \mathrm{topGen}\left(\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 \left({A}×\left\{{J}\right\}\right)\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 \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\wedge {x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)\right\}\right)\wedge {A}×\left\{{X}\right\}\in \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\to \exists {t}\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 \left({A}×\left\{{J}\right\}\right)\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 \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\wedge {x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\left({A}×\left\{{X}\right\}\in {t}\wedge {t}\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)$
47 28 45 46 syl2anc ${⊢}{\phi }\to \exists {t}\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 \left({A}×\left\{{J}\right\}\right)\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 \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\wedge {x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\left({A}×\left\{{X}\right\}\in {t}\wedge {t}\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)$
48 eleq2 ${⊢}{t}={x}\to \left({A}×\left\{{X}\right\}\in {t}↔{A}×\left\{{X}\right\}\in {x}\right)$
49 sseq1 ${⊢}{t}={x}\to \left({t}\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}↔{x}\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)$
50 48 49 anbi12d ${⊢}{t}={x}\to \left(\left({A}×\left\{{X}\right\}\in {t}\wedge {t}\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)↔\left({A}×\left\{{X}\right\}\in {x}\wedge {x}\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)$
51 50 rexab2 ${⊢}\exists {t}\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 \left({A}×\left\{{J}\right\}\right)\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 \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\wedge {x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}\left({A}×\left\{{X}\right\}\in {t}\wedge {t}\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\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 \left({A}×\left\{{J}\right\}\right)\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 \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\wedge {x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)\wedge \left({A}×\left\{{X}\right\}\in {x}\wedge {x}\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)$
52 47 51 sylib ${⊢}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}\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 \left({A}×\left\{{J}\right\}\right)\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 \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\wedge {x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)\wedge \left({A}×\left\{{X}\right\}\in {x}\wedge {x}\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)$
53 toponuni ${⊢}{J}\in \mathrm{TopOn}\left({B}\right)\to {B}=\bigcup {J}$
54 5 17 53 3syl ${⊢}{\phi }\to {B}=\bigcup {J}$
55 54 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to {B}=\bigcup {J}$
56 55 ineq1d ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to {B}\cap \bigcap \mathrm{ran}{g}=\bigcup {J}\cap \bigcap \mathrm{ran}{g}$
57 19 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to {J}\in \mathrm{Top}$
58 simplrl ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to {g}Fn{A}$
59 simplrr ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)$
60 fvconst2g ${⊢}\left({J}\in \mathrm{Top}\wedge {y}\in {A}\right)\to \left({A}×\left\{{J}\right\}\right)\left({y}\right)={J}$
61 60 eleq2d ${⊢}\left({J}\in \mathrm{Top}\wedge {y}\in {A}\right)\to \left({g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)↔{g}\left({y}\right)\in {J}\right)$
62 61 ralbidva ${⊢}{J}\in \mathrm{Top}\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in {J}\right)$
63 57 62 syl ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in {J}\right)$
64 59 63 mpbid ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in {J}$
65 ffnfv ${⊢}{g}:{A}⟶{J}↔\left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in {J}\right)$
66 58 64 65 sylanbrc ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to {g}:{A}⟶{J}$
67 66 frnd ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to \mathrm{ran}{g}\subseteq {J}$
68 6 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to {A}\in \mathrm{Fin}$
69 dffn4 ${⊢}{g}Fn{A}↔{g}:{A}\underset{onto}{⟶}\mathrm{ran}{g}$
70 58 69 sylib ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to {g}:{A}\underset{onto}{⟶}\mathrm{ran}{g}$
71 fofi ${⊢}\left({A}\in \mathrm{Fin}\wedge {g}:{A}\underset{onto}{⟶}\mathrm{ran}{g}\right)\to \mathrm{ran}{g}\in \mathrm{Fin}$
72 68 70 71 syl2anc ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to \mathrm{ran}{g}\in \mathrm{Fin}$
73 eqid ${⊢}\bigcup {J}=\bigcup {J}$
74 73 rintopn ${⊢}\left({J}\in \mathrm{Top}\wedge \mathrm{ran}{g}\subseteq {J}\wedge \mathrm{ran}{g}\in \mathrm{Fin}\right)\to \bigcup {J}\cap \bigcap \mathrm{ran}{g}\in {J}$
75 57 67 72 74 syl3anc ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to \bigcup {J}\cap \bigcap \mathrm{ran}{g}\in {J}$
76 56 75 eqeltrd ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to {B}\cap \bigcap \mathrm{ran}{g}\in {J}$
77 8 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to {X}\in {B}$
78 fconstmpt ${⊢}{A}×\left\{{X}\right\}=\left({y}\in {A}⟼{X}\right)$
79 simprl ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to {A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)$
80 78 79 eqeltrrid ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to \left({y}\in {A}⟼{X}\right)\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)$
81 mptelixpg ${⊢}{A}\in \mathrm{Fin}\to \left(\left({y}\in {A}⟼{X}\right)\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{X}\in {g}\left({y}\right)\right)$
82 68 81 syl ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to \left(\left({y}\in {A}⟼{X}\right)\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{X}\in {g}\left({y}\right)\right)$
83 80 82 mpbid ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{X}\in {g}\left({y}\right)$
84 eleq2 ${⊢}{z}={g}\left({y}\right)\to \left({X}\in {z}↔{X}\in {g}\left({y}\right)\right)$
85 84 ralrn ${⊢}{g}Fn{A}\to \left(\forall {z}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}{X}\in {z}↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{X}\in {g}\left({y}\right)\right)$
86 58 85 syl ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to \left(\forall {z}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}{X}\in {z}↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{X}\in {g}\left({y}\right)\right)$
87 83 86 mpbird ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to \forall {z}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}{X}\in {z}$
88 elrint ${⊢}{X}\in \left({B}\cap \bigcap \mathrm{ran}{g}\right)↔\left({X}\in {B}\wedge \forall {z}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}{X}\in {z}\right)$
89 77 87 88 sylanbrc ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to {X}\in \left({B}\cap \bigcap \mathrm{ran}{g}\right)$
90 33 inex1 ${⊢}{B}\cap \bigcap \mathrm{ran}{g}\in \mathrm{V}$
91 ixpconstg ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\cap \bigcap \mathrm{ran}{g}\in \mathrm{V}\right)\to \underset{{y}\in {A}}{⨉}\left({B}\cap \bigcap \mathrm{ran}{g}\right)={\left({B}\cap \bigcap \mathrm{ran}{g}\right)}^{{A}}$
92 68 90 91 sylancl ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to \underset{{y}\in {A}}{⨉}\left({B}\cap \bigcap \mathrm{ran}{g}\right)={\left({B}\cap \bigcap \mathrm{ran}{g}\right)}^{{A}}$
93 inss2 ${⊢}{B}\cap \bigcap \mathrm{ran}{g}\subseteq \bigcap \mathrm{ran}{g}$
94 fnfvelrn ${⊢}\left({g}Fn{A}\wedge {y}\in {A}\right)\to {g}\left({y}\right)\in \mathrm{ran}{g}$
95 intss1 ${⊢}{g}\left({y}\right)\in \mathrm{ran}{g}\to \bigcap \mathrm{ran}{g}\subseteq {g}\left({y}\right)$
96 94 95 syl ${⊢}\left({g}Fn{A}\wedge {y}\in {A}\right)\to \bigcap \mathrm{ran}{g}\subseteq {g}\left({y}\right)$
97 93 96 sstrid ${⊢}\left({g}Fn{A}\wedge {y}\in {A}\right)\to {B}\cap \bigcap \mathrm{ran}{g}\subseteq {g}\left({y}\right)$
98 97 ralrimiva ${⊢}{g}Fn{A}\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{B}\cap \bigcap \mathrm{ran}{g}\subseteq {g}\left({y}\right)$
99 ss2ixp ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{B}\cap \bigcap \mathrm{ran}{g}\subseteq {g}\left({y}\right)\to \underset{{y}\in {A}}{⨉}\left({B}\cap \bigcap \mathrm{ran}{g}\right)\subseteq \underset{{y}\in {A}}{⨉}{g}\left({y}\right)$
100 58 98 99 3syl ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to \underset{{y}\in {A}}{⨉}\left({B}\cap \bigcap \mathrm{ran}{g}\right)\subseteq \underset{{y}\in {A}}{⨉}{g}\left({y}\right)$
101 92 100 eqsstrrd ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to {\left({B}\cap \bigcap \mathrm{ran}{g}\right)}^{{A}}\subseteq \underset{{y}\in {A}}{⨉}{g}\left({y}\right)$
102 ssrab ${⊢}\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}↔\left(\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq {{B}}^{{A}}\wedge \forall {f}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\phantom{\rule{.4em}{0ex}}{\sum }_{{G}}{f}\in {U}\right)$
103 102 simprbi ${⊢}\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\to \forall {f}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\phantom{\rule{.4em}{0ex}}{\sum }_{{G}}{f}\in {U}$
104 103 ad2antll ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to \forall {f}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\phantom{\rule{.4em}{0ex}}{\sum }_{{G}}{f}\in {U}$
105 ssralv ${⊢}{\left({B}\cap \bigcap \mathrm{ran}{g}\right)}^{{A}}\subseteq \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\to \left(\forall {f}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\phantom{\rule{.4em}{0ex}}{\sum }_{{G}}{f}\in {U}\to \forall {f}\in \left({\left({B}\cap \bigcap \mathrm{ran}{g}\right)}^{{A}}\right)\phantom{\rule{.4em}{0ex}}{\sum }_{{G}}{f}\in {U}\right)$
106 101 104 105 sylc ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to \forall {f}\in \left({\left({B}\cap \bigcap \mathrm{ran}{g}\right)}^{{A}}\right)\phantom{\rule{.4em}{0ex}}{\sum }_{{G}}{f}\in {U}$
107 eleq2 ${⊢}{u}={B}\cap \bigcap \mathrm{ran}{g}\to \left({X}\in {u}↔{X}\in \left({B}\cap \bigcap \mathrm{ran}{g}\right)\right)$
108 oveq1 ${⊢}{u}={B}\cap \bigcap \mathrm{ran}{g}\to {{u}}^{{A}}={\left({B}\cap \bigcap \mathrm{ran}{g}\right)}^{{A}}$
109 108 raleqdv ${⊢}{u}={B}\cap \bigcap \mathrm{ran}{g}\to \left(\forall {f}\in \left({{u}}^{{A}}\right)\phantom{\rule{.4em}{0ex}}{\sum }_{{G}}{f}\in {U}↔\forall {f}\in \left({\left({B}\cap \bigcap \mathrm{ran}{g}\right)}^{{A}}\right)\phantom{\rule{.4em}{0ex}}{\sum }_{{G}}{f}\in {U}\right)$
110 107 109 anbi12d ${⊢}{u}={B}\cap \bigcap \mathrm{ran}{g}\to \left(\left({X}\in {u}\wedge \forall {f}\in \left({{u}}^{{A}}\right)\phantom{\rule{.4em}{0ex}}{\sum }_{{G}}{f}\in {U}\right)↔\left({X}\in \left({B}\cap \bigcap \mathrm{ran}{g}\right)\wedge \forall {f}\in \left({\left({B}\cap \bigcap \mathrm{ran}{g}\right)}^{{A}}\right)\phantom{\rule{.4em}{0ex}}{\sum }_{{G}}{f}\in {U}\right)\right)$
111 110 rspcev ${⊢}\left({B}\cap \bigcap \mathrm{ran}{g}\in {J}\wedge \left({X}\in \left({B}\cap \bigcap \mathrm{ran}{g}\right)\wedge \forall {f}\in \left({\left({B}\cap \bigcap \mathrm{ran}{g}\right)}^{{A}}\right)\phantom{\rule{.4em}{0ex}}{\sum }_{{G}}{f}\in {U}\right)\right)\to \exists {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({X}\in {u}\wedge \forall {f}\in \left({{u}}^{{A}}\right)\phantom{\rule{.4em}{0ex}}{\sum }_{{G}}{f}\in {U}\right)$
112 76 89 106 111 syl12anc ${⊢}\left(\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\wedge \left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to \exists {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({X}\in {u}\wedge \forall {f}\in \left({{u}}^{{A}}\right)\phantom{\rule{.4em}{0ex}}{\sum }_{{G}}{f}\in {U}\right)$
113 112 ex ${⊢}\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\to \left(\left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\to \exists {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({X}\in {u}\wedge \forall {f}\in \left({{u}}^{{A}}\right)\phantom{\rule{.4em}{0ex}}{\sum }_{{G}}{f}\in {U}\right)\right)$
114 113 3adantr3 ${⊢}\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\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 \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\to \left(\left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\to \exists {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({X}\in {u}\wedge \forall {f}\in \left({{u}}^{{A}}\right)\phantom{\rule{.4em}{0ex}}{\sum }_{{G}}{f}\in {U}\right)\right)$
115 eleq2 ${⊢}{x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\to \left({A}×\left\{{X}\right\}\in {x}↔{A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)$
116 sseq1 ${⊢}{x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\to \left({x}\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}↔\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)$
117 115 116 anbi12d ${⊢}{x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\to \left(\left({A}×\left\{{X}\right\}\in {x}\wedge {x}\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)↔\left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)$
118 117 imbi1d ${⊢}{x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\to \left(\left(\left({A}×\left\{{X}\right\}\in {x}\wedge {x}\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\to \exists {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({X}\in {u}\wedge \forall {f}\in \left({{u}}^{{A}}\right)\phantom{\rule{.4em}{0ex}}{\sum }_{{G}}{f}\in {U}\right)\right)↔\left(\left({A}×\left\{{X}\right\}\in \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\wedge \underset{{y}\in {A}}{⨉}{g}\left({y}\right)\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\to \exists {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({X}\in {u}\wedge \forall {f}\in \left({{u}}^{{A}}\right)\phantom{\rule{.4em}{0ex}}{\sum }_{{G}}{f}\in {U}\right)\right)\right)$
119 114 118 syl5ibrcom ${⊢}\left({\phi }\wedge \left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\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 \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\right)\to \left({x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\to \left(\left({A}×\left\{{X}\right\}\in {x}\wedge {x}\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\to \exists {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({X}\in {u}\wedge \forall {f}\in \left({{u}}^{{A}}\right)\phantom{\rule{.4em}{0ex}}{\sum }_{{G}}{f}\in {U}\right)\right)\right)$
120 119 expimpd ${⊢}{\phi }\to \left(\left(\left({g}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({y}\right)\in \left({A}×\left\{{J}\right\}\right)\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 \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\wedge {x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)\to \left(\left({A}×\left\{{X}\right\}\in {x}\wedge {x}\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\to \exists {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({X}\in {u}\wedge \forall {f}\in \left({{u}}^{{A}}\right)\phantom{\rule{.4em}{0ex}}{\sum }_{{G}}{f}\in {U}\right)\right)\right)$
121 120 exlimdv ${⊢}{\phi }\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 \left({A}×\left\{{J}\right\}\right)\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 \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\wedge {x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)\to \left(\left({A}×\left\{{X}\right\}\in {x}\wedge {x}\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\to \exists {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({X}\in {u}\wedge \forall {f}\in \left({{u}}^{{A}}\right)\phantom{\rule{.4em}{0ex}}{\sum }_{{G}}{f}\in {U}\right)\right)\right)$
122 121 impd ${⊢}{\phi }\to \left(\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 \left({A}×\left\{{J}\right\}\right)\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 \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\wedge {x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)\wedge \left({A}×\left\{{X}\right\}\in {x}\wedge {x}\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to \exists {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({X}\in {u}\wedge \forall {f}\in \left({{u}}^{{A}}\right)\phantom{\rule{.4em}{0ex}}{\sum }_{{G}}{f}\in {U}\right)\right)$
123 122 exlimdv ${⊢}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\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 \left({A}×\left\{{J}\right\}\right)\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 \left({A}×\left\{{J}\right\}\right)\left({y}\right)\right)\wedge {x}=\underset{{y}\in {A}}{⨉}{g}\left({y}\right)\right)\wedge \left({A}×\left\{{X}\right\}\in {x}\wedge {x}\subseteq \left\{{f}\in \left({{B}}^{{A}}\right)|{\sum }_{{G}}{f}\in {U}\right\}\right)\right)\to \exists {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({X}\in {u}\wedge \forall {f}\in \left({{u}}^{{A}}\right)\phantom{\rule{.4em}{0ex}}{\sum }_{{G}}{f}\in {U}\right)\right)$
124 52 123 mpd ${⊢}{\phi }\to \exists {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({X}\in {u}\wedge \forall {f}\in \left({{u}}^{{A}}\right)\phantom{\rule{.4em}{0ex}}{\sum }_{{G}}{f}\in {U}\right)$