ptclsg

Description: The closure of a box in the product topology is the box formed from the closures of the factors. The proof uses the axiom of choice; the last hypothesis is the choice assumption. (Contributed by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Hypotheses	ptcls.2	$⊢ J = \prod_{𝑡} ((k \in A ⟼ R))$
	ptcls.a	$⊢ φ \to A \in V$
	ptcls.j	$⊢ (φ \land k \in A) \to R \in TopOn (X)$
	ptcls.c	$⊢ (φ \land k \in A) \to S \subseteq X$
	ptclsg.1	$⊢ φ \to ⋃_{k \in A} S \in \underline{AC} A$
Assertion	ptclsg	$⊢ φ \to cls (J) (\underset{k \in A}{⨉} S) = \underset{k \in A}{⨉} cls (R) (S)$

Proof

Step	Hyp	Ref	Expression
1		ptcls.2	$⊢ J = \prod_{𝑡} ((k \in A ⟼ R))$
2		ptcls.a	$⊢ φ \to A \in V$
3		ptcls.j	$⊢ (φ \land k \in A) \to R \in TopOn (X)$
4		ptcls.c	$⊢ (φ \land k \in A) \to S \subseteq X$
5		ptclsg.1	$⊢ φ \to ⋃_{k \in A} S \in \underline{AC} A$
6		topontop	$⊢ R \in TopOn (X) \to R \in Top$
7	3 6	syl	$⊢ (φ \land k \in A) \to R \in Top$
8		toponuni	$⊢ R \in TopOn (X) \to X = ⋃ R$
9	3 8	syl	$⊢ (φ \land k \in A) \to X = ⋃ R$
10	4 9	sseqtrd	$⊢ (φ \land k \in A) \to S \subseteq ⋃ R$
11		eqid	$⊢ ⋃ R = ⋃ R$
12	11	clscld	$⊢ (R \in Top \land S \subseteq ⋃ R) \to cls (R) (S) \in Clsd (R)$
13	7 10 12	syl2anc	$⊢ (φ \land k \in A) \to cls (R) (S) \in Clsd (R)$
14	2 7 13	ptcldmpt	$⊢ φ \to \underset{k \in A}{⨉} cls (R) (S) \in Clsd (\prod_{𝑡} ((k \in A ⟼ R)))$
15	1	fveq2i	$⊢ Clsd (J) = Clsd (\prod_{𝑡} ((k \in A ⟼ R)))$
16	14 15	eleqtrrdi	$⊢ φ \to \underset{k \in A}{⨉} cls (R) (S) \in Clsd (J)$
17	11	sscls	$⊢ (R \in Top \land S \subseteq ⋃ R) \to S \subseteq cls (R) (S)$
18	7 10 17	syl2anc	$⊢ (φ \land k \in A) \to S \subseteq cls (R) (S)$
19	18	ralrimiva	$⊢ φ \to \forall k \in A S \subseteq cls (R) (S)$
20		ss2ixp	$⊢ \forall k \in A S \subseteq cls (R) (S) \to \underset{k \in A}{⨉} S \subseteq \underset{k \in A}{⨉} cls (R) (S)$
21	19 20	syl	$⊢ φ \to \underset{k \in A}{⨉} S \subseteq \underset{k \in A}{⨉} cls (R) (S)$
22		eqid	$⊢ ⋃ J = ⋃ J$
23	22	clsss2	$⊢ (\underset{k \in A}{⨉} cls (R) (S) \in Clsd (J) \land \underset{k \in A}{⨉} S \subseteq \underset{k \in A}{⨉} cls (R) (S)) \to cls (J) (\underset{k \in A}{⨉} S) \subseteq \underset{k \in A}{⨉} cls (R) (S)$
24	16 21 23	syl2anc	$⊢ φ \to cls (J) (\underset{k \in A}{⨉} S) \subseteq \underset{k \in A}{⨉} cls (R) (S)$
25		vex	$⊢ u \in V$
26		eqeq1	$⊢ x = u \to (x = \underset{y \in A}{⨉} g (y) \leftrightarrow u = \underset{y \in A}{⨉} g (y))$
27	26	anbi2d	$⊢ x = u \to (((g Fn A \land \forall y \in A g (y) \in (k \in A ⟼ R) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (k \in A ⟼ R) (y)) \land x = \underset{y \in A}{⨉} g (y)) \leftrightarrow ((g Fn A \land \forall y \in A g (y) \in (k \in A ⟼ R) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (k \in A ⟼ R) (y)) \land u = \underset{y \in A}{⨉} g (y)))$
28	27	exbidv	$⊢ x = u \to (\exists g ((g Fn A \land \forall y \in A g (y) \in (k \in A ⟼ R) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (k \in A ⟼ R) (y)) \land x = \underset{y \in A}{⨉} g (y)) \leftrightarrow \exists g ((g Fn A \land \forall y \in A g (y) \in (k \in A ⟼ R) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (k \in A ⟼ R) (y)) \land u = \underset{y \in A}{⨉} g (y)))$
29	25 28	elab	$⊢ u \in \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in (k \in A ⟼ R) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (k \in A ⟼ R) (y)) \land x = \underset{y \in A}{⨉} g (y))\} \leftrightarrow \exists g ((g Fn A \land \forall y \in A g (y) \in (k \in A ⟼ R) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (k \in A ⟼ R) (y)) \land u = \underset{y \in A}{⨉} g (y))$
30		nffvmpt1	$⊢ \underline{Ⅎ} k (k \in A ⟼ R) (y)$
31	30	nfel2	$⊢ Ⅎ k g (y) \in (k \in A ⟼ R) (y)$
32		nfv	$⊢ Ⅎ y g (k) \in (k \in A ⟼ R) (k)$
33		fveq2	$⊢ y = k \to g (y) = g (k)$
34		fveq2	$⊢ y = k \to (k \in A ⟼ R) (y) = (k \in A ⟼ R) (k)$
35	33 34	eleq12d	$⊢ y = k \to (g (y) \in (k \in A ⟼ R) (y) \leftrightarrow g (k) \in (k \in A ⟼ R) (k))$
36	31 32 35	cbvralw	$⊢ \forall y \in A g (y) \in (k \in A ⟼ R) (y) \leftrightarrow \forall k \in A g (k) \in (k \in A ⟼ R) (k)$
37		simpr	$⊢ (φ \land k \in A) \to k \in A$
38		eqid	$⊢ (k \in A ⟼ R) = (k \in A ⟼ R)$
39	38	fvmpt2	$⊢ (k \in A \land R \in TopOn (X)) \to (k \in A ⟼ R) (k) = R$
40	37 3 39	syl2anc	$⊢ (φ \land k \in A) \to (k \in A ⟼ R) (k) = R$
41	40	eleq2d	$⊢ (φ \land k \in A) \to (g (k) \in (k \in A ⟼ R) (k) \leftrightarrow g (k) \in R)$
42	41	ralbidva	$⊢ φ \to (\forall k \in A g (k) \in (k \in A ⟼ R) (k) \leftrightarrow \forall k \in A g (k) \in R)$
43	36 42	syl5bb	$⊢ φ \to (\forall y \in A g (y) \in (k \in A ⟼ R) (y) \leftrightarrow \forall k \in A g (k) \in R)$
44	43	anbi2d	$⊢ φ \to ((g Fn A \land \forall y \in A g (y) \in (k \in A ⟼ R) (y)) \leftrightarrow (g Fn A \land \forall k \in A g (k) \in R))$
45	44	adantr	$⊢ (φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \to ((g Fn A \land \forall y \in A g (y) \in (k \in A ⟼ R) (y)) \leftrightarrow (g Fn A \land \forall k \in A g (k) \in R))$
46	45	biimpa	$⊢ ((φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \land (g Fn A \land \forall y \in A g (y) \in (k \in A ⟼ R) (y))) \to (g Fn A \land \forall k \in A g (k) \in R)$
47	5	ad2antrr	$⊢ ((φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \land ((g Fn A \land \forall k \in A g (k) \in R) \land f \in \underset{y \in A}{⨉} g (y))) \to ⋃_{k \in A} S \in \underline{AC} A$
48		simpll	$⊢ ((φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \land ((g Fn A \land \forall k \in A g (k) \in R) \land f \in \underset{y \in A}{⨉} g (y))) \to φ$
49		vex	$⊢ f \in V$
50	49	elixp	$⊢ f \in \underset{k \in A}{⨉} cls (R) (S) \leftrightarrow (f Fn A \land \forall k \in A f (k) \in cls (R) (S))$
51	50	simprbi	$⊢ f \in \underset{k \in A}{⨉} cls (R) (S) \to \forall k \in A f (k) \in cls (R) (S)$
52	51	ad2antlr	$⊢ ((φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \land ((g Fn A \land \forall k \in A g (k) \in R) \land f \in \underset{y \in A}{⨉} g (y))) \to \forall k \in A f (k) \in cls (R) (S)$
53	11	clsndisj	$⊢ ((R \in Top \land S \subseteq ⋃ R \land f (k) \in cls (R) (S)) \land (g (k) \in R \land f (k) \in g (k))) \to g (k) \cap S \neq \emptyset$
54	53	ex	$⊢ (R \in Top \land S \subseteq ⋃ R \land f (k) \in cls (R) (S)) \to ((g (k) \in R \land f (k) \in g (k)) \to g (k) \cap S \neq \emptyset)$
55	54	3expia	$⊢ (R \in Top \land S \subseteq ⋃ R) \to (f (k) \in cls (R) (S) \to ((g (k) \in R \land f (k) \in g (k)) \to g (k) \cap S \neq \emptyset))$
56	7 10 55	syl2anc	$⊢ (φ \land k \in A) \to (f (k) \in cls (R) (S) \to ((g (k) \in R \land f (k) \in g (k)) \to g (k) \cap S \neq \emptyset))$
57	56	ralimdva	$⊢ φ \to (\forall k \in A f (k) \in cls (R) (S) \to \forall k \in A ((g (k) \in R \land f (k) \in g (k)) \to g (k) \cap S \neq \emptyset))$
58	48 52 57	sylc	$⊢ ((φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \land ((g Fn A \land \forall k \in A g (k) \in R) \land f \in \underset{y \in A}{⨉} g (y))) \to \forall k \in A ((g (k) \in R \land f (k) \in g (k)) \to g (k) \cap S \neq \emptyset)$
59		simprlr	$⊢ ((φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \land ((g Fn A \land \forall k \in A g (k) \in R) \land f \in \underset{y \in A}{⨉} g (y))) \to \forall k \in A g (k) \in R$
60		simprr	$⊢ ((φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \land ((g Fn A \land \forall k \in A g (k) \in R) \land f \in \underset{y \in A}{⨉} g (y))) \to f \in \underset{y \in A}{⨉} g (y)$
61	33	cbvixpv	$⊢ \underset{y \in A}{⨉} g (y) = \underset{k \in A}{⨉} g (k)$
62	60 61	eleqtrdi	$⊢ ((φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \land ((g Fn A \land \forall k \in A g (k) \in R) \land f \in \underset{y \in A}{⨉} g (y))) \to f \in \underset{k \in A}{⨉} g (k)$
63	49	elixp	$⊢ f \in \underset{k \in A}{⨉} g (k) \leftrightarrow (f Fn A \land \forall k \in A f (k) \in g (k))$
64	63	simprbi	$⊢ f \in \underset{k \in A}{⨉} g (k) \to \forall k \in A f (k) \in g (k)$
65	62 64	syl	$⊢ ((φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \land ((g Fn A \land \forall k \in A g (k) \in R) \land f \in \underset{y \in A}{⨉} g (y))) \to \forall k \in A f (k) \in g (k)$
66		r19.26	$⊢ \forall k \in A (g (k) \in R \land f (k) \in g (k)) \leftrightarrow (\forall k \in A g (k) \in R \land \forall k \in A f (k) \in g (k))$
67	59 65 66	sylanbrc	$⊢ ((φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \land ((g Fn A \land \forall k \in A g (k) \in R) \land f \in \underset{y \in A}{⨉} g (y))) \to \forall k \in A (g (k) \in R \land f (k) \in g (k))$
68		ralim	$⊢ \forall k \in A ((g (k) \in R \land f (k) \in g (k)) \to g (k) \cap S \neq \emptyset) \to (\forall k \in A (g (k) \in R \land f (k) \in g (k)) \to \forall k \in A g (k) \cap S \neq \emptyset)$
69	58 67 68	sylc	$⊢ ((φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \land ((g Fn A \land \forall k \in A g (k) \in R) \land f \in \underset{y \in A}{⨉} g (y))) \to \forall k \in A g (k) \cap S \neq \emptyset$
70		rabn0	$⊢ \{z \in ⋃_{k \in A} S \| z \in (g (k) \cap S)\} \neq \emptyset \leftrightarrow \exists z \in ⋃_{k \in A} S z \in (g (k) \cap S)$
71		dfin5	$⊢ ⋃_{k \in A} S \cap (g (k) \cap S) = \{z \in ⋃_{k \in A} S \| z \in (g (k) \cap S)\}$
72		inss2	$⊢ g (k) \cap S \subseteq S$
73		ssiun2	$⊢ k \in A \to S \subseteq ⋃_{k \in A} S$
74	72 73	sstrid	$⊢ k \in A \to g (k) \cap S \subseteq ⋃_{k \in A} S$
75		sseqin2	$⊢ g (k) \cap S \subseteq ⋃_{k \in A} S \leftrightarrow ⋃_{k \in A} S \cap (g (k) \cap S) = g (k) \cap S$
76	74 75	sylib	$⊢ k \in A \to ⋃_{k \in A} S \cap (g (k) \cap S) = g (k) \cap S$
77	71 76	syl5eqr	$⊢ k \in A \to \{z \in ⋃_{k \in A} S \| z \in (g (k) \cap S)\} = g (k) \cap S$
78	77	neeq1d	$⊢ k \in A \to (\{z \in ⋃_{k \in A} S \| z \in (g (k) \cap S)\} \neq \emptyset \leftrightarrow g (k) \cap S \neq \emptyset)$
79	70 78	bitr3id	$⊢ k \in A \to (\exists z \in ⋃_{k \in A} S z \in (g (k) \cap S) \leftrightarrow g (k) \cap S \neq \emptyset)$
80	79	ralbiia	$⊢ \forall k \in A \exists z \in ⋃_{k \in A} S z \in (g (k) \cap S) \leftrightarrow \forall k \in A g (k) \cap S \neq \emptyset$
81	69 80	sylibr	$⊢ ((φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \land ((g Fn A \land \forall k \in A g (k) \in R) \land f \in \underset{y \in A}{⨉} g (y))) \to \forall k \in A \exists z \in ⋃_{k \in A} S z \in (g (k) \cap S)$
82		nfv	$⊢ Ⅎ y \exists z \in ⋃_{k \in A} S z \in (g (k) \cap S)$
83		nfiu1	$⊢ \underline{Ⅎ} k ⋃_{k \in A} S$
84		nfcv	$⊢ \underline{Ⅎ} k g (y)$
85		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ y / k ⦌ S$
86	84 85	nfin	$⊢ \underline{Ⅎ} k (g (y) \cap ⦋ y / k ⦌ S)$
87	86	nfel2	$⊢ Ⅎ k z \in (g (y) \cap ⦋ y / k ⦌ S)$
88	83 87	nfrex	$⊢ Ⅎ k \exists z \in ⋃_{k \in A} S z \in (g (y) \cap ⦋ y / k ⦌ S)$
89		fveq2	$⊢ k = y \to g (k) = g (y)$
90		csbeq1a	$⊢ k = y \to S = ⦋ y / k ⦌ S$
91	89 90	ineq12d	$⊢ k = y \to g (k) \cap S = g (y) \cap ⦋ y / k ⦌ S$
92	91	eleq2d	$⊢ k = y \to (z \in (g (k) \cap S) \leftrightarrow z \in (g (y) \cap ⦋ y / k ⦌ S))$
93	92	rexbidv	$⊢ k = y \to (\exists z \in ⋃_{k \in A} S z \in (g (k) \cap S) \leftrightarrow \exists z \in ⋃_{k \in A} S z \in (g (y) \cap ⦋ y / k ⦌ S))$
94	82 88 93	cbvralw	$⊢ \forall k \in A \exists z \in ⋃_{k \in A} S z \in (g (k) \cap S) \leftrightarrow \forall y \in A \exists z \in ⋃_{k \in A} S z \in (g (y) \cap ⦋ y / k ⦌ S)$
95	81 94	sylib	$⊢ ((φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \land ((g Fn A \land \forall k \in A g (k) \in R) \land f \in \underset{y \in A}{⨉} g (y))) \to \forall y \in A \exists z \in ⋃_{k \in A} S z \in (g (y) \cap ⦋ y / k ⦌ S)$
96		eleq1	$⊢ z = h (y) \to (z \in (g (y) \cap ⦋ y / k ⦌ S) \leftrightarrow h (y) \in (g (y) \cap ⦋ y / k ⦌ S))$
97	96	acni3	$⊢ (⋃_{k \in A} S \in \underline{AC} A \land \forall y \in A \exists z \in ⋃_{k \in A} S z \in (g (y) \cap ⦋ y / k ⦌ S)) \to \exists h (h : A ⟶ ⋃_{k \in A} S \land \forall y \in A h (y) \in (g (y) \cap ⦋ y / k ⦌ S))$
98	47 95 97	syl2anc	$⊢ ((φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \land ((g Fn A \land \forall k \in A g (k) \in R) \land f \in \underset{y \in A}{⨉} g (y))) \to \exists h (h : A ⟶ ⋃_{k \in A} S \land \forall y \in A h (y) \in (g (y) \cap ⦋ y / k ⦌ S))$
99		ffn	$⊢ h : A ⟶ ⋃_{k \in A} S \to h Fn A$
100		nfv	$⊢ Ⅎ y h (k) \in (g (k) \cap S)$
101	86	nfel2	$⊢ Ⅎ k h (y) \in (g (y) \cap ⦋ y / k ⦌ S)$
102		fveq2	$⊢ k = y \to h (k) = h (y)$
103	102 91	eleq12d	$⊢ k = y \to (h (k) \in (g (k) \cap S) \leftrightarrow h (y) \in (g (y) \cap ⦋ y / k ⦌ S))$
104	100 101 103	cbvralw	$⊢ \forall k \in A h (k) \in (g (k) \cap S) \leftrightarrow \forall y \in A h (y) \in (g (y) \cap ⦋ y / k ⦌ S)$
105		ne0i	$⊢ h \in \underset{k \in A}{⨉} (g (k) \cap S) \to \underset{k \in A}{⨉} (g (k) \cap S) \neq \emptyset$
106		vex	$⊢ h \in V$
107	106	elixp	$⊢ h \in \underset{k \in A}{⨉} (g (k) \cap S) \leftrightarrow (h Fn A \land \forall k \in A h (k) \in (g (k) \cap S))$
108		ixpin	$⊢ \underset{k \in A}{⨉} (g (k) \cap S) = \underset{k \in A}{⨉} g (k) \cap \underset{k \in A}{⨉} S$
109	61	ineq1i	$⊢ \underset{y \in A}{⨉} g (y) \cap \underset{k \in A}{⨉} S = \underset{k \in A}{⨉} g (k) \cap \underset{k \in A}{⨉} S$
110	108 109	eqtr4i	$⊢ \underset{k \in A}{⨉} (g (k) \cap S) = \underset{y \in A}{⨉} g (y) \cap \underset{k \in A}{⨉} S$
111	110	neeq1i	$⊢ \underset{k \in A}{⨉} (g (k) \cap S) \neq \emptyset \leftrightarrow \underset{y \in A}{⨉} g (y) \cap \underset{k \in A}{⨉} S \neq \emptyset$
112	105 107 111	3imtr3i	$⊢ (h Fn A \land \forall k \in A h (k) \in (g (k) \cap S)) \to \underset{y \in A}{⨉} g (y) \cap \underset{k \in A}{⨉} S \neq \emptyset$
113	104 112	sylan2br	$⊢ (h Fn A \land \forall y \in A h (y) \in (g (y) \cap ⦋ y / k ⦌ S)) \to \underset{y \in A}{⨉} g (y) \cap \underset{k \in A}{⨉} S \neq \emptyset$
114	99 113	sylan	$⊢ (h : A ⟶ ⋃_{k \in A} S \land \forall y \in A h (y) \in (g (y) \cap ⦋ y / k ⦌ S)) \to \underset{y \in A}{⨉} g (y) \cap \underset{k \in A}{⨉} S \neq \emptyset$
115	114	exlimiv	$⊢ \exists h (h : A ⟶ ⋃_{k \in A} S \land \forall y \in A h (y) \in (g (y) \cap ⦋ y / k ⦌ S)) \to \underset{y \in A}{⨉} g (y) \cap \underset{k \in A}{⨉} S \neq \emptyset$
116	98 115	syl	$⊢ ((φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \land ((g Fn A \land \forall k \in A g (k) \in R) \land f \in \underset{y \in A}{⨉} g (y))) \to \underset{y \in A}{⨉} g (y) \cap \underset{k \in A}{⨉} S \neq \emptyset$
117	116	expr	$⊢ ((φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \land (g Fn A \land \forall k \in A g (k) \in R)) \to (f \in \underset{y \in A}{⨉} g (y) \to \underset{y \in A}{⨉} g (y) \cap \underset{k \in A}{⨉} S \neq \emptyset)$
118	46 117	syldan	$⊢ ((φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \land (g Fn A \land \forall y \in A g (y) \in (k \in A ⟼ R) (y))) \to (f \in \underset{y \in A}{⨉} g (y) \to \underset{y \in A}{⨉} g (y) \cap \underset{k \in A}{⨉} S \neq \emptyset)$
119	118	3adantr3	$⊢ ((φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \land (g Fn A \land \forall y \in A g (y) \in (k \in A ⟼ R) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (k \in A ⟼ R) (y))) \to (f \in \underset{y \in A}{⨉} g (y) \to \underset{y \in A}{⨉} g (y) \cap \underset{k \in A}{⨉} S \neq \emptyset)$
120		eleq2	$⊢ u = \underset{y \in A}{⨉} g (y) \to (f \in u \leftrightarrow f \in \underset{y \in A}{⨉} g (y))$
121		ineq1	$⊢ u = \underset{y \in A}{⨉} g (y) \to u \cap \underset{k \in A}{⨉} S = \underset{y \in A}{⨉} g (y) \cap \underset{k \in A}{⨉} S$
122	121	neeq1d	$⊢ u = \underset{y \in A}{⨉} g (y) \to (u \cap \underset{k \in A}{⨉} S \neq \emptyset \leftrightarrow \underset{y \in A}{⨉} g (y) \cap \underset{k \in A}{⨉} S \neq \emptyset)$
123	120 122	imbi12d	$⊢ u = \underset{y \in A}{⨉} g (y) \to ((f \in u \to u \cap \underset{k \in A}{⨉} S \neq \emptyset) \leftrightarrow (f \in \underset{y \in A}{⨉} g (y) \to \underset{y \in A}{⨉} g (y) \cap \underset{k \in A}{⨉} S \neq \emptyset))$
124	119 123	syl5ibrcom	$⊢ ((φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \land (g Fn A \land \forall y \in A g (y) \in (k \in A ⟼ R) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (k \in A ⟼ R) (y))) \to (u = \underset{y \in A}{⨉} g (y) \to (f \in u \to u \cap \underset{k \in A}{⨉} S \neq \emptyset))$
125	124	expimpd	$⊢ (φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \to (((g Fn A \land \forall y \in A g (y) \in (k \in A ⟼ R) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (k \in A ⟼ R) (y)) \land u = \underset{y \in A}{⨉} g (y)) \to (f \in u \to u \cap \underset{k \in A}{⨉} S \neq \emptyset))$
126	125	exlimdv	$⊢ (φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \to (\exists g ((g Fn A \land \forall y \in A g (y) \in (k \in A ⟼ R) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (k \in A ⟼ R) (y)) \land u = \underset{y \in A}{⨉} g (y)) \to (f \in u \to u \cap \underset{k \in A}{⨉} S \neq \emptyset))$
127	29 126	syl5bi	$⊢ (φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \to (u \in \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in (k \in A ⟼ R) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (k \in A ⟼ R) (y)) \land x = \underset{y \in A}{⨉} g (y))\} \to (f \in u \to u \cap \underset{k \in A}{⨉} S \neq \emptyset))$
128	127	ralrimiv	$⊢ (φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \to \forall u \in \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in (k \in A ⟼ R) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (k \in A ⟼ R) (y)) \land x = \underset{y \in A}{⨉} g (y))\} (f \in u \to u \cap \underset{k \in A}{⨉} S \neq \emptyset)$
129	7	fmpttd	$⊢ φ \to (k \in A ⟼ R) : A ⟶ Top$
130	129	ffnd	$⊢ φ \to (k \in A ⟼ R) Fn A$
131		eqid	$⊢ \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in (k \in A ⟼ R) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (k \in A ⟼ R) (y)) \land x = \underset{y \in A}{⨉} g (y))\} = \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in (k \in A ⟼ R) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (k \in A ⟼ R) (y)) \land x = \underset{y \in A}{⨉} g (y))\}$
132	131	ptval	$⊢ (A \in V \land (k \in A ⟼ R) Fn A) \to \prod_{𝑡} ((k \in A ⟼ R)) = topGen (\{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in (k \in A ⟼ R) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (k \in A ⟼ R) (y)) \land x = \underset{y \in A}{⨉} g (y))\})$
133	2 130 132	syl2anc	$⊢ φ \to \prod_{𝑡} ((k \in A ⟼ R)) = topGen (\{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in (k \in A ⟼ R) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (k \in A ⟼ R) (y)) \land x = \underset{y \in A}{⨉} g (y))\})$
134	1 133	syl5eq	$⊢ φ \to J = topGen (\{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in (k \in A ⟼ R) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (k \in A ⟼ R) (y)) \land x = \underset{y \in A}{⨉} g (y))\})$
135	134	adantr	$⊢ (φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \to J = topGen (\{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in (k \in A ⟼ R) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (k \in A ⟼ R) (y)) \land x = \underset{y \in A}{⨉} g (y))\})$
136	3	ralrimiva	$⊢ φ \to \forall k \in A R \in TopOn (X)$
137	1	pttopon	$⊢ (A \in V \land \forall k \in A R \in TopOn (X)) \to J \in TopOn (\underset{k \in A}{⨉} X)$
138	2 136 137	syl2anc	$⊢ φ \to J \in TopOn (\underset{k \in A}{⨉} X)$
139		toponuni	$⊢ J \in TopOn (\underset{k \in A}{⨉} X) \to \underset{k \in A}{⨉} X = ⋃ J$
140	138 139	syl	$⊢ φ \to \underset{k \in A}{⨉} X = ⋃ J$
141	140	adantr	$⊢ (φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \to \underset{k \in A}{⨉} X = ⋃ J$
142	131	ptbas	$⊢ (A \in V \land (k \in A ⟼ R) : A ⟶ Top) \to \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in (k \in A ⟼ R) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (k \in A ⟼ R) (y)) \land x = \underset{y \in A}{⨉} g (y))\} \in TopBases$
143	2 129 142	syl2anc	$⊢ φ \to \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in (k \in A ⟼ R) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (k \in A ⟼ R) (y)) \land x = \underset{y \in A}{⨉} g (y))\} \in TopBases$
144	143	adantr	$⊢ (φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \to \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in (k \in A ⟼ R) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (k \in A ⟼ R) (y)) \land x = \underset{y \in A}{⨉} g (y))\} \in TopBases$
145	4	ralrimiva	$⊢ φ \to \forall k \in A S \subseteq X$
146		ss2ixp	$⊢ \forall k \in A S \subseteq X \to \underset{k \in A}{⨉} S \subseteq \underset{k \in A}{⨉} X$
147	145 146	syl	$⊢ φ \to \underset{k \in A}{⨉} S \subseteq \underset{k \in A}{⨉} X$
148	147	adantr	$⊢ (φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \to \underset{k \in A}{⨉} S \subseteq \underset{k \in A}{⨉} X$
149	11	clsss3	$⊢ (R \in Top \land S \subseteq ⋃ R) \to cls (R) (S) \subseteq ⋃ R$
150	7 10 149	syl2anc	$⊢ (φ \land k \in A) \to cls (R) (S) \subseteq ⋃ R$
151	150 9	sseqtrrd	$⊢ (φ \land k \in A) \to cls (R) (S) \subseteq X$
152	151	ralrimiva	$⊢ φ \to \forall k \in A cls (R) (S) \subseteq X$
153		ss2ixp	$⊢ \forall k \in A cls (R) (S) \subseteq X \to \underset{k \in A}{⨉} cls (R) (S) \subseteq \underset{k \in A}{⨉} X$
154	152 153	syl	$⊢ φ \to \underset{k \in A}{⨉} cls (R) (S) \subseteq \underset{k \in A}{⨉} X$
155	154	sselda	$⊢ (φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \to f \in \underset{k \in A}{⨉} X$
156	135 141 144 148 155	elcls3	$⊢ (φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \to (f \in cls (J) (\underset{k \in A}{⨉} S) \leftrightarrow \forall u \in \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in (k \in A ⟼ R) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (k \in A ⟼ R) (y)) \land x = \underset{y \in A}{⨉} g (y))\} (f \in u \to u \cap \underset{k \in A}{⨉} S \neq \emptyset))$
157	128 156	mpbird	$⊢ (φ \land f \in \underset{k \in A}{⨉} cls (R) (S)) \to f \in cls (J) (\underset{k \in A}{⨉} S)$
158	24 157	eqelssd	$⊢ φ \to cls (J) (\underset{k \in A}{⨉} S) = \underset{k \in A}{⨉} cls (R) (S)$

Metamath Proof Explorer

Theorem ptclsg

Proof