Theorem ptcld

Description: A closed box in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015)

	Ref	Expression
Hypotheses	ptcld.a	$$⊢\phi \to A\in V$$
	ptcld.f	$$⊢\phi \to F:A⟶\mathrm{Top}$$
	ptcld.c	$$⊢\left(\phi \wedge k\in A\right)\to C\in \mathrm{Clsd}\left(F\left(k\right)\right)$$
Assertion	ptcld	$$⊢\phi \to \underset{k\in A}{⨉}C\in \mathrm{Clsd}\left({\prod }_{𝑡}\left(F\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ptcld.a	$$⊢\phi \to A\in V$$
2		ptcld.f	$$⊢\phi \to F:A⟶\mathrm{Top}$$
3		ptcld.c	$$⊢\left(\phi \wedge k\in A\right)\to C\in \mathrm{Clsd}\left(F\left(k\right)\right)$$
4		eqid	$$⊢\bigcup F\left(k\right)=\bigcup F\left(k\right)$$
5	4	cldss	$$⊢C\in \mathrm{Clsd}\left(F\left(k\right)\right)\to C\subseteq \bigcup F\left(k\right)$$
6	3 5	syl	$$⊢\left(\phi \wedge k\in A\right)\to C\subseteq \bigcup F\left(k\right)$$
7	6	ralrimiva	$$⊢\phi \to \forall k\in AC\subseteq \bigcup F\left(k\right)$$
8		boxriin	$$⊢\forall k\in AC\subseteq \bigcup F\left(k\right)\to \underset{k\in A}{⨉}C=\underset{k\in A}{⨉}\bigcup F\left(k\right)\cap \bigcap _{x\in A}\underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)$$
9	7 8	syl	$$⊢\phi \to \underset{k\in A}{⨉}C=\underset{k\in A}{⨉}\bigcup F\left(k\right)\cap \bigcap _{x\in A}\underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)$$
10		eqid	$$⊢{\prod }_{𝑡}\left(F\right)={\prod }_{𝑡}\left(F\right)$$
11	10	ptuni	$$⊢\left(A\in V\wedge F:A⟶\mathrm{Top}\right)\to \underset{k\in A}{⨉}\bigcup F\left(k\right)=\bigcup {\prod }_{𝑡}\left(F\right)$$
12	1 2 11	syl2anc	$$⊢\phi \to \underset{k\in A}{⨉}\bigcup F\left(k\right)=\bigcup {\prod }_{𝑡}\left(F\right)$$
13	12	ineq1d	$$⊢\phi \to \underset{k\in A}{⨉}\bigcup F\left(k\right)\cap \bigcap _{x\in A}\underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)=\bigcup {\prod }_{𝑡}\left(F\right)\cap \bigcap _{x\in A}\underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)$$
14		pttop	$$⊢\left(A\in V\wedge F:A⟶\mathrm{Top}\right)\to {\prod }_{𝑡}\left(F\right)\in \mathrm{Top}$$
15	1 2 14	syl2anc	$$⊢\phi \to {\prod }_{𝑡}\left(F\right)\in \mathrm{Top}$$
16		sseq1	$$⊢C=if\left(k=x,C,\bigcup F\left(k\right)\right)\to \left(C\subseteq \bigcup F\left(k\right)\leftrightarrow if\left(k=x,C,\bigcup F\left(k\right)\right)\subseteq \bigcup F\left(k\right)\right)$$
17		sseq1	$$⊢\bigcup F\left(k\right)=if\left(k=x,C,\bigcup F\left(k\right)\right)\to \left(\bigcup F\left(k\right)\subseteq \bigcup F\left(k\right)\leftrightarrow if\left(k=x,C,\bigcup F\left(k\right)\right)\subseteq \bigcup F\left(k\right)\right)$$
18		simpl	$$⊢\left(C\subseteq \bigcup F\left(k\right)\wedge k=x\right)\to C\subseteq \bigcup F\left(k\right)$$
19		ssidd	$$⊢\left(C\subseteq \bigcup F\left(k\right)\wedge \neg k=x\right)\to \bigcup F\left(k\right)\subseteq \bigcup F\left(k\right)$$
20	16 17 18 19	ifbothda	$$⊢C\subseteq \bigcup F\left(k\right)\to if\left(k=x,C,\bigcup F\left(k\right)\right)\subseteq \bigcup F\left(k\right)$$
21	20	ralimi	$$⊢\forall k\in AC\subseteq \bigcup F\left(k\right)\to \forall k\in Aif\left(k=x,C,\bigcup F\left(k\right)\right)\subseteq \bigcup F\left(k\right)$$
22		ss2ixp	$$⊢\forall k\in Aif\left(k=x,C,\bigcup F\left(k\right)\right)\subseteq \bigcup F\left(k\right)\to \underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)\subseteq \underset{k\in A}{⨉}\bigcup F\left(k\right)$$
23	7 21 22	3syl	$$⊢\phi \to \underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)\subseteq \underset{k\in A}{⨉}\bigcup F\left(k\right)$$
24	23	adantr	$$⊢\left(\phi \wedge x\in A\right)\to \underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)\subseteq \underset{k\in A}{⨉}\bigcup F\left(k\right)$$
25	12	adantr	$$⊢\left(\phi \wedge x\in A\right)\to \underset{k\in A}{⨉}\bigcup F\left(k\right)=\bigcup {\prod }_{𝑡}\left(F\right)$$
26	24 25	sseqtrd	$$⊢\left(\phi \wedge x\in A\right)\to \underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)\subseteq \bigcup {\prod }_{𝑡}\left(F\right)$$
27	12	eqcomd	$$⊢\phi \to \bigcup {\prod }_{𝑡}\left(F\right)=\underset{k\in A}{⨉}\bigcup F\left(k\right)$$
28	27	difeq1d	$$⊢\phi \to \bigcup {\prod }_{𝑡}\left(F\right)\setminus \underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)=\underset{k\in A}{⨉}\bigcup F\left(k\right)\setminus \underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)$$
29	28	adantr	$$⊢\left(\phi \wedge x\in A\right)\to \bigcup {\prod }_{𝑡}\left(F\right)\setminus \underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)=\underset{k\in A}{⨉}\bigcup F\left(k\right)\setminus \underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)$$
30		simpr	$$⊢\left(\phi \wedge x\in A\right)\to x\in A$$
31	7	adantr	$$⊢\left(\phi \wedge x\in A\right)\to \forall k\in AC\subseteq \bigcup F\left(k\right)$$
32		boxcutc	$$⊢\left(x\in A\wedge \forall k\in AC\subseteq \bigcup F\left(k\right)\right)\to \underset{k\in A}{⨉}\bigcup F\left(k\right)\setminus \underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)=\underset{k\in A}{⨉}if\left(k=x,\bigcup F\left(k\right)\setminus C,\bigcup F\left(k\right)\right)$$
33	30 31 32	syl2anc	$$⊢\left(\phi \wedge x\in A\right)\to \underset{k\in A}{⨉}\bigcup F\left(k\right)\setminus \underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)=\underset{k\in A}{⨉}if\left(k=x,\bigcup F\left(k\right)\setminus C,\bigcup F\left(k\right)\right)$$
34		ixpeq2	$$⊢\forall k\in Aif\left(k=x,\bigcup F\left(k\right)\setminus C,\bigcup F\left(k\right)\right)=if\left(k=x,\bigcup F\left(x\right)\setminus ⦋x/k⦌C,\bigcup F\left(k\right)\right)\to \underset{k\in A}{⨉}if\left(k=x,\bigcup F\left(k\right)\setminus C,\bigcup F\left(k\right)\right)=\underset{k\in A}{⨉}if\left(k=x,\bigcup F\left(x\right)\setminus ⦋x/k⦌C,\bigcup F\left(k\right)\right)$$
35		fveq2	$$⊢k=x\to F\left(k\right)=F\left(x\right)$$
36	35	unieqd	$$⊢k=x\to \bigcup F\left(k\right)=\bigcup F\left(x\right)$$
37		csbeq1a	$$⊢k=x\to C=⦋x/k⦌C$$
38	36 37	difeq12d	$$⊢k=x\to \bigcup F\left(k\right)\setminus C=\bigcup F\left(x\right)\setminus ⦋x/k⦌C$$
39	38	adantl	$$⊢\left(k\in A\wedge k=x\right)\to \bigcup F\left(k\right)\setminus C=\bigcup F\left(x\right)\setminus ⦋x/k⦌C$$
40	39	ifeq1da	$$⊢k\in A\to if\left(k=x,\bigcup F\left(k\right)\setminus C,\bigcup F\left(k\right)\right)=if\left(k=x,\bigcup F\left(x\right)\setminus ⦋x/k⦌C,\bigcup F\left(k\right)\right)$$
41	34 40	mprg	$$⊢\underset{k\in A}{⨉}if\left(k=x,\bigcup F\left(k\right)\setminus C,\bigcup F\left(k\right)\right)=\underset{k\in A}{⨉}if\left(k=x,\bigcup F\left(x\right)\setminus ⦋x/k⦌C,\bigcup F\left(k\right)\right)$$
42	41	a1i	$$⊢\left(\phi \wedge x\in A\right)\to \underset{k\in A}{⨉}if\left(k=x,\bigcup F\left(k\right)\setminus C,\bigcup F\left(k\right)\right)=\underset{k\in A}{⨉}if\left(k=x,\bigcup F\left(x\right)\setminus ⦋x/k⦌C,\bigcup F\left(k\right)\right)$$
43	29 33 42	3eqtrd	$$⊢\left(\phi \wedge x\in A\right)\to \bigcup {\prod }_{𝑡}\left(F\right)\setminus \underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)=\underset{k\in A}{⨉}if\left(k=x,\bigcup F\left(x\right)\setminus ⦋x/k⦌C,\bigcup F\left(k\right)\right)$$
44	1	adantr	$$⊢\left(\phi \wedge x\in A\right)\to A\in V$$
45	2	adantr	$$⊢\left(\phi \wedge x\in A\right)\to F:A⟶\mathrm{Top}$$
46	3	ralrimiva	$$⊢\phi \to \forall k\in AC\in \mathrm{Clsd}\left(F\left(k\right)\right)$$
47		nfv	$$⊢ℲxC\in \mathrm{Clsd}\left(F\left(k\right)\right)$$
48		nfcsb1v	$$⊢\underset{\_}{Ⅎ}k⦋x/k⦌C$$
49	48	nfel1	$$⊢Ⅎk⦋x/k⦌C\in \mathrm{Clsd}\left(F\left(x\right)\right)$$
50		2fveq3	$$⊢k=x\to \mathrm{Clsd}\left(F\left(k\right)\right)=\mathrm{Clsd}\left(F\left(x\right)\right)$$
51	37 50	eleq12d	$$⊢k=x\to \left(C\in \mathrm{Clsd}\left(F\left(k\right)\right)\leftrightarrow ⦋x/k⦌C\in \mathrm{Clsd}\left(F\left(x\right)\right)\right)$$
52	47 49 51	cbvralw	$$⊢\forall k\in AC\in \mathrm{Clsd}\left(F\left(k\right)\right)\leftrightarrow \forall x\in A⦋x/k⦌C\in \mathrm{Clsd}\left(F\left(x\right)\right)$$
53	46 52	sylib	$$⊢\phi \to \forall x\in A⦋x/k⦌C\in \mathrm{Clsd}\left(F\left(x\right)\right)$$
54	53	r19.21bi	$$⊢\left(\phi \wedge x\in A\right)\to ⦋x/k⦌C\in \mathrm{Clsd}\left(F\left(x\right)\right)$$
55		eqid	$$⊢\bigcup F\left(x\right)=\bigcup F\left(x\right)$$
56	55	cldopn	$$⊢⦋x/k⦌C\in \mathrm{Clsd}\left(F\left(x\right)\right)\to \bigcup F\left(x\right)\setminus ⦋x/k⦌C\in F\left(x\right)$$
57	54 56	syl	$$⊢\left(\phi \wedge x\in A\right)\to \bigcup F\left(x\right)\setminus ⦋x/k⦌C\in F\left(x\right)$$
58	44 45 57	ptopn2	$$⊢\left(\phi \wedge x\in A\right)\to \underset{k\in A}{⨉}if\left(k=x,\bigcup F\left(x\right)\setminus ⦋x/k⦌C,\bigcup F\left(k\right)\right)\in {\prod }_{𝑡}\left(F\right)$$
59	43 58	eqeltrd	$$⊢\left(\phi \wedge x\in A\right)\to \bigcup {\prod }_{𝑡}\left(F\right)\setminus \underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)\in {\prod }_{𝑡}\left(F\right)$$
60		eqid	$$⊢\bigcup {\prod }_{𝑡}\left(F\right)=\bigcup {\prod }_{𝑡}\left(F\right)$$
61	60	iscld	$$⊢{\prod }_{𝑡}\left(F\right)\in \mathrm{Top}\to \left(\underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)\in \mathrm{Clsd}\left({\prod }_{𝑡}\left(F\right)\right)\leftrightarrow \left(\underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)\subseteq \bigcup {\prod }_{𝑡}\left(F\right)\wedge \bigcup {\prod }_{𝑡}\left(F\right)\setminus \underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)\in {\prod }_{𝑡}\left(F\right)\right)\right)$$
62	15 61	syl	$$⊢\phi \to \left(\underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)\in \mathrm{Clsd}\left({\prod }_{𝑡}\left(F\right)\right)\leftrightarrow \left(\underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)\subseteq \bigcup {\prod }_{𝑡}\left(F\right)\wedge \bigcup {\prod }_{𝑡}\left(F\right)\setminus \underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)\in {\prod }_{𝑡}\left(F\right)\right)\right)$$
63	62	adantr	$$⊢\left(\phi \wedge x\in A\right)\to \left(\underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)\in \mathrm{Clsd}\left({\prod }_{𝑡}\left(F\right)\right)\leftrightarrow \left(\underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)\subseteq \bigcup {\prod }_{𝑡}\left(F\right)\wedge \bigcup {\prod }_{𝑡}\left(F\right)\setminus \underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)\in {\prod }_{𝑡}\left(F\right)\right)\right)$$
64	26 59 63	mpbir2and	$$⊢\left(\phi \wedge x\in A\right)\to \underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)\in \mathrm{Clsd}\left({\prod }_{𝑡}\left(F\right)\right)$$
65	64	ralrimiva	$$⊢\phi \to \forall x\in A\underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)\in \mathrm{Clsd}\left({\prod }_{𝑡}\left(F\right)\right)$$
66	60	riincld	$$⊢\left({\prod }_{𝑡}\left(F\right)\in \mathrm{Top}\wedge \forall x\in A\underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)\in \mathrm{Clsd}\left({\prod }_{𝑡}\left(F\right)\right)\right)\to \bigcup {\prod }_{𝑡}\left(F\right)\cap \bigcap _{x\in A}\underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)\in \mathrm{Clsd}\left({\prod }_{𝑡}\left(F\right)\right)$$
67	15 65 66	syl2anc	$$⊢\phi \to \bigcup {\prod }_{𝑡}\left(F\right)\cap \bigcap _{x\in A}\underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)\in \mathrm{Clsd}\left({\prod }_{𝑡}\left(F\right)\right)$$
68	13 67	eqeltrd	$$⊢\phi \to \underset{k\in A}{⨉}\bigcup F\left(k\right)\cap \bigcap _{x\in A}\underset{k\in A}{⨉}if\left(k=x,C,\bigcup F\left(k\right)\right)\in \mathrm{Clsd}\left({\prod }_{𝑡}\left(F\right)\right)$$
69	9 68	eqeltrd	$$⊢\phi \to \underset{k\in A}{⨉}C\in \mathrm{Clsd}\left({\prod }_{𝑡}\left(F\right)\right)$$