xkopt

Description: The compact-open topology on a discrete set coincides with the product topology where all the factors are the same. (Contributed by Mario Carneiro, 19-Mar-2015) (Revised by Mario Carneiro, 12-Sep-2015)

		Ref	Expression
	Assertion	xkopt	$⊢ (R \in Top \land A \in V) \to R^_{ko} 𝒫 A = \prod_{𝑡} (A \times \{R\})$

Proof

Step	Hyp	Ref	Expression
1		distop	$⊢ A \in V \to 𝒫 A \in Top$
2		simpl	$⊢ (R \in Top \land A \in V) \to R \in Top$
3		unipw	$⊢ ⋃ 𝒫 A = A$
4	3	eqcomi	$⊢ A = ⋃ 𝒫 A$
5		eqid	$⊢ \{x \in 𝒫 A \| 𝒫 A ↾_{𝑡} x \in Comp\} = \{x \in 𝒫 A \| 𝒫 A ↾_{𝑡} x \in Comp\}$
6		eqid	$⊢ (k \in \{x \in 𝒫 A \| 𝒫 A ↾_{𝑡} x \in Comp\}, v \in R ⟼ \{f \in (𝒫 A Cn R) \| f [k] \subseteq v\}) = (k \in \{x \in 𝒫 A \| 𝒫 A ↾_{𝑡} x \in Comp\}, v \in R ⟼ \{f \in (𝒫 A Cn R) \| f [k] \subseteq v\})$
7	4 5 6	xkoval	$⊢ (𝒫 A \in Top \land R \in Top) \to R^_{ko} 𝒫 A = topGen (fi (ran (k \in \{x \in 𝒫 A \| 𝒫 A ↾_{𝑡} x \in Comp\}, v \in R ⟼ \{f \in (𝒫 A Cn R) \| f [k] \subseteq v\})))$
8	1 2 7	syl2an2	$⊢ (R \in Top \land A \in V) \to R^_{ko} 𝒫 A = topGen (fi (ran (k \in \{x \in 𝒫 A \| 𝒫 A ↾_{𝑡} x \in Comp\}, v \in R ⟼ \{f \in (𝒫 A Cn R) \| f [k] \subseteq v\})))$
9		simpr	$⊢ (R \in Top \land A \in V) \to A \in V$
10		fconst6g	$⊢ R \in Top \to (A \times \{R\}) : A ⟶ Top$
11	10	adantr	$⊢ (R \in Top \land A \in V) \to (A \times \{R\}) : A ⟶ Top$
12		pttop	$⊢ (A \in V \land (A \times \{R\}) : A ⟶ Top) \to \prod_{𝑡} (A \times \{R\}) \in Top$
13	9 11 12	syl2anc	$⊢ (R \in Top \land A \in V) \to \prod_{𝑡} (A \times \{R\}) \in Top$
14		elpwi	$⊢ x \in 𝒫 A \to x \subseteq A$
15		restdis	$⊢ (A \in V \land x \subseteq A) \to 𝒫 A ↾_{𝑡} x = 𝒫 x$
16	14 15	sylan2	$⊢ (A \in V \land x \in 𝒫 A) \to 𝒫 A ↾_{𝑡} x = 𝒫 x$
17	16	adantll	$⊢ ((R \in Top \land A \in V) \land x \in 𝒫 A) \to 𝒫 A ↾_{𝑡} x = 𝒫 x$
18	17	eleq1d	$⊢ ((R \in Top \land A \in V) \land x \in 𝒫 A) \to (𝒫 A ↾_{𝑡} x \in Comp \leftrightarrow 𝒫 x \in Comp)$
19		discmp	$⊢ x \in Fin \leftrightarrow 𝒫 x \in Comp$
20	18 19	bitr4di	$⊢ ((R \in Top \land A \in V) \land x \in 𝒫 A) \to (𝒫 A ↾_{𝑡} x \in Comp \leftrightarrow x \in Fin)$
21	20	rabbidva	$⊢ (R \in Top \land A \in V) \to \{x \in 𝒫 A \| 𝒫 A ↾_{𝑡} x \in Comp\} = \{x \in 𝒫 A \| x \in Fin\}$
22		dfin5	$⊢ 𝒫 A \cap Fin = \{x \in 𝒫 A \| x \in Fin\}$
23	21 22	eqtr4di	$⊢ (R \in Top \land A \in V) \to \{x \in 𝒫 A \| 𝒫 A ↾_{𝑡} x \in Comp\} = 𝒫 A \cap Fin$
24		eqidd	$⊢ (R \in Top \land A \in V) \to R = R$
25		toptopon2	$⊢ R \in Top \leftrightarrow R \in TopOn (⋃ R)$
26		cndis	$⊢ (A \in V \land R \in TopOn (⋃ R)) \to 𝒫 A Cn R = {⋃ R}^{A}$
27	26	ancoms	$⊢ (R \in TopOn (⋃ R) \land A \in V) \to 𝒫 A Cn R = {⋃ R}^{A}$
28	25 27	sylanb	$⊢ (R \in Top \land A \in V) \to 𝒫 A Cn R = {⋃ R}^{A}$
29	28	rabeqdv	$⊢ (R \in Top \land A \in V) \to \{f \in (𝒫 A Cn R) \| f [k] \subseteq v\} = \{f \in ({⋃ R}^{A}) \| f [k] \subseteq v\}$
30	23 24 29	mpoeq123dv	$⊢ (R \in Top \land A \in V) \to (k \in \{x \in 𝒫 A \| 𝒫 A ↾_{𝑡} x \in Comp\}, v \in R ⟼ \{f \in (𝒫 A Cn R) \| f [k] \subseteq v\}) = (k \in (𝒫 A \cap Fin), v \in R ⟼ \{f \in ({⋃ R}^{A}) \| f [k] \subseteq v\})$
31	30	rneqd	$⊢ (R \in Top \land A \in V) \to ran (k \in \{x \in 𝒫 A \| 𝒫 A ↾_{𝑡} x \in Comp\}, v \in R ⟼ \{f \in (𝒫 A Cn R) \| f [k] \subseteq v\}) = ran (k \in (𝒫 A \cap Fin), v \in R ⟼ \{f \in ({⋃ R}^{A}) \| f [k] \subseteq v\})$
32		eqid	$⊢ (k \in (𝒫 A \cap Fin), v \in R ⟼ \{f \in ({⋃ R}^{A}) \| f [k] \subseteq v\}) = (k \in (𝒫 A \cap Fin), v \in R ⟼ \{f \in ({⋃ R}^{A}) \| f [k] \subseteq v\})$
33	32	rnmpo	$⊢ ran (k \in (𝒫 A \cap Fin), v \in R ⟼ \{f \in ({⋃ R}^{A}) \| f [k] \subseteq v\}) = \{x \| \exists k \in (𝒫 A \cap Fin) \exists v \in R x = \{f \in ({⋃ R}^{A}) \| f [k] \subseteq v\}\}$
34	31 33	eqtrdi	$⊢ (R \in Top \land A \in V) \to ran (k \in \{x \in 𝒫 A \| 𝒫 A ↾_{𝑡} x \in Comp\}, v \in R ⟼ \{f \in (𝒫 A Cn R) \| f [k] \subseteq v\}) = \{x \| \exists k \in (𝒫 A \cap Fin) \exists v \in R x = \{f \in ({⋃ R}^{A}) \| f [k] \subseteq v\}\}$
35		elmapi	$⊢ f \in ({⋃ R}^{A}) \to f : A ⟶ ⋃ R$
36		eleq2	$⊢ v = if (x \in k, v, ⋃ R) \to (f (x) \in v \leftrightarrow f (x) \in if (x \in k, v, ⋃ R))$
37	36	imbi2d	$⊢ v = if (x \in k, v, ⋃ R) \to ((x \in A \to f (x) \in v) \leftrightarrow (x \in A \to f (x) \in if (x \in k, v, ⋃ R)))$
38	37	bibi1d	$⊢ v = if (x \in k, v, ⋃ R) \to (((x \in A \to f (x) \in v) \leftrightarrow (x \in k \to f (x) \in v)) \leftrightarrow ((x \in A \to f (x) \in if (x \in k, v, ⋃ R)) \leftrightarrow (x \in k \to f (x) \in v)))$
39		eleq2	$⊢ ⋃ R = if (x \in k, v, ⋃ R) \to (f (x) \in ⋃ R \leftrightarrow f (x) \in if (x \in k, v, ⋃ R))$
40	39	imbi2d	$⊢ ⋃ R = if (x \in k, v, ⋃ R) \to ((x \in A \to f (x) \in ⋃ R) \leftrightarrow (x \in A \to f (x) \in if (x \in k, v, ⋃ R)))$
41	40	bibi1d	$⊢ ⋃ R = if (x \in k, v, ⋃ R) \to (((x \in A \to f (x) \in ⋃ R) \leftrightarrow (x \in k \to f (x) \in v)) \leftrightarrow ((x \in A \to f (x) \in if (x \in k, v, ⋃ R)) \leftrightarrow (x \in k \to f (x) \in v)))$
42		simprl	$⊢ ((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \to k \in (𝒫 A \cap Fin)$
43	42	elin1d	$⊢ ((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \to k \in 𝒫 A$
44	43	elpwid	$⊢ ((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \to k \subseteq A$
45	44	adantr	$⊢ (((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land f : A ⟶ ⋃ R) \to k \subseteq A$
46	45	sselda	$⊢ ((((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land f : A ⟶ ⋃ R) \land x \in k) \to x \in A$
47		simpr	$⊢ ((((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land f : A ⟶ ⋃ R) \land x \in k) \to x \in k$
48	46 47	2thd	$⊢ ((((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land f : A ⟶ ⋃ R) \land x \in k) \to (x \in A \leftrightarrow x \in k)$
49	48	imbi1d	$⊢ ((((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land f : A ⟶ ⋃ R) \land x \in k) \to ((x \in A \to f (x) \in v) \leftrightarrow (x \in k \to f (x) \in v))$
50		ffvelrn	$⊢ (f : A ⟶ ⋃ R \land x \in A) \to f (x) \in ⋃ R$
51	50	ex	$⊢ f : A ⟶ ⋃ R \to (x \in A \to f (x) \in ⋃ R)$
52	51	adantl	$⊢ (((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land f : A ⟶ ⋃ R) \to (x \in A \to f (x) \in ⋃ R)$
53	52	adantr	$⊢ ((((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land f : A ⟶ ⋃ R) \land \neg x \in k) \to (x \in A \to f (x) \in ⋃ R)$
54		pm2.21	$⊢ \neg x \in k \to (x \in k \to f (x) \in v)$
55	54	adantl	$⊢ ((((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land f : A ⟶ ⋃ R) \land \neg x \in k) \to (x \in k \to f (x) \in v)$
56	53 55	2thd	$⊢ ((((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land f : A ⟶ ⋃ R) \land \neg x \in k) \to ((x \in A \to f (x) \in ⋃ R) \leftrightarrow (x \in k \to f (x) \in v))$
57	38 41 49 56	ifbothda	$⊢ (((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land f : A ⟶ ⋃ R) \to ((x \in A \to f (x) \in if (x \in k, v, ⋃ R)) \leftrightarrow (x \in k \to f (x) \in v))$
58	57	ralbidv2	$⊢ (((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land f : A ⟶ ⋃ R) \to (\forall x \in A f (x) \in if (x \in k, v, ⋃ R) \leftrightarrow \forall x \in k f (x) \in v)$
59		ffn	$⊢ f : A ⟶ ⋃ R \to f Fn A$
60	59	adantl	$⊢ (((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land f : A ⟶ ⋃ R) \to f Fn A$
61		vex	$⊢ f \in V$
62	61	elixp	$⊢ f \in \underset{x \in A}{⨉} if (x \in k, v, ⋃ R) \leftrightarrow (f Fn A \land \forall x \in A f (x) \in if (x \in k, v, ⋃ R))$
63	62	baib	$⊢ f Fn A \to (f \in \underset{x \in A}{⨉} if (x \in k, v, ⋃ R) \leftrightarrow \forall x \in A f (x) \in if (x \in k, v, ⋃ R))$
64	60 63	syl	$⊢ (((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land f : A ⟶ ⋃ R) \to (f \in \underset{x \in A}{⨉} if (x \in k, v, ⋃ R) \leftrightarrow \forall x \in A f (x) \in if (x \in k, v, ⋃ R))$
65		ffun	$⊢ f : A ⟶ ⋃ R \to Fun f$
66		fdm	$⊢ f : A ⟶ ⋃ R \to dom f = A$
67	66	adantl	$⊢ (((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land f : A ⟶ ⋃ R) \to dom f = A$
68	45 67	sseqtrrd	$⊢ (((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land f : A ⟶ ⋃ R) \to k \subseteq dom f$
69		funimass4	$⊢ (Fun f \land k \subseteq dom f) \to (f [k] \subseteq v \leftrightarrow \forall x \in k f (x) \in v)$
70	65 68 69	syl2an2	$⊢ (((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land f : A ⟶ ⋃ R) \to (f [k] \subseteq v \leftrightarrow \forall x \in k f (x) \in v)$
71	58 64 70	3bitr4d	$⊢ (((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land f : A ⟶ ⋃ R) \to (f \in \underset{x \in A}{⨉} if (x \in k, v, ⋃ R) \leftrightarrow f [k] \subseteq v)$
72	35 71	sylan2	$⊢ (((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land f \in ({⋃ R}^{A})) \to (f \in \underset{x \in A}{⨉} if (x \in k, v, ⋃ R) \leftrightarrow f [k] \subseteq v)$
73	72	rabbi2dva	$⊢ ((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \to ({⋃ R}^{A}) \cap \underset{x \in A}{⨉} if (x \in k, v, ⋃ R) = \{f \in ({⋃ R}^{A}) \| f [k] \subseteq v\}$
74		elssuni	$⊢ v \in R \to v \subseteq ⋃ R$
75	74	ad2antll	$⊢ ((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \to v \subseteq ⋃ R$
76		ssid	$⊢ ⋃ R \subseteq ⋃ R$
77		sseq1	$⊢ v = if (x \in k, v, ⋃ R) \to (v \subseteq ⋃ R \leftrightarrow if (x \in k, v, ⋃ R) \subseteq ⋃ R)$
78		sseq1	$⊢ ⋃ R = if (x \in k, v, ⋃ R) \to (⋃ R \subseteq ⋃ R \leftrightarrow if (x \in k, v, ⋃ R) \subseteq ⋃ R)$
79	77 78	ifboth	$⊢ (v \subseteq ⋃ R \land ⋃ R \subseteq ⋃ R) \to if (x \in k, v, ⋃ R) \subseteq ⋃ R$
80	75 76 79	sylancl	$⊢ ((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \to if (x \in k, v, ⋃ R) \subseteq ⋃ R$
81	80	ralrimivw	$⊢ ((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \to \forall x \in A if (x \in k, v, ⋃ R) \subseteq ⋃ R$
82		ss2ixp	$⊢ \forall x \in A if (x \in k, v, ⋃ R) \subseteq ⋃ R \to \underset{x \in A}{⨉} if (x \in k, v, ⋃ R) \subseteq \underset{x \in A}{⨉} ⋃ R$
83	81 82	syl	$⊢ ((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \to \underset{x \in A}{⨉} if (x \in k, v, ⋃ R) \subseteq \underset{x \in A}{⨉} ⋃ R$
84		simplr	$⊢ ((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \to A \in V$
85		uniexg	$⊢ R \in Top \to ⋃ R \in V$
86	85	ad2antrr	$⊢ ((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \to ⋃ R \in V$
87		ixpconstg	$⊢ (A \in V \land ⋃ R \in V) \to \underset{x \in A}{⨉} ⋃ R = {⋃ R}^{A}$
88	84 86 87	syl2anc	$⊢ ((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \to \underset{x \in A}{⨉} ⋃ R = {⋃ R}^{A}$
89	83 88	sseqtrd	$⊢ ((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \to \underset{x \in A}{⨉} if (x \in k, v, ⋃ R) \subseteq {⋃ R}^{A}$
90		sseqin2	$⊢ \underset{x \in A}{⨉} if (x \in k, v, ⋃ R) \subseteq {⋃ R}^{A} \leftrightarrow ({⋃ R}^{A}) \cap \underset{x \in A}{⨉} if (x \in k, v, ⋃ R) = \underset{x \in A}{⨉} if (x \in k, v, ⋃ R)$
91	89 90	sylib	$⊢ ((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \to ({⋃ R}^{A}) \cap \underset{x \in A}{⨉} if (x \in k, v, ⋃ R) = \underset{x \in A}{⨉} if (x \in k, v, ⋃ R)$
92	73 91	eqtr3d	$⊢ ((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \to \{f \in ({⋃ R}^{A}) \| f [k] \subseteq v\} = \underset{x \in A}{⨉} if (x \in k, v, ⋃ R)$
93	10	ad2antrr	$⊢ ((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \to (A \times \{R\}) : A ⟶ Top$
94	42	elin2d	$⊢ ((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \to k \in Fin$
95		simplrr	$⊢ (((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land x \in A) \to v \in R$
96		eqid	$⊢ ⋃ R = ⋃ R$
97	96	topopn	$⊢ R \in Top \to ⋃ R \in R$
98	97	ad3antrrr	$⊢ (((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land x \in A) \to ⋃ R \in R$
99	95 98	ifcld	$⊢ (((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land x \in A) \to if (x \in k, v, ⋃ R) \in R$
100		fvconst2g	$⊢ (R \in Top \land x \in A) \to (A \times \{R\}) (x) = R$
101	100	ad4ant14	$⊢ (((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land x \in A) \to (A \times \{R\}) (x) = R$
102	99 101	eleqtrrd	$⊢ (((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land x \in A) \to if (x \in k, v, ⋃ R) \in (A \times \{R\}) (x)$
103		eldifn	$⊢ x \in (A ∖ k) \to \neg x \in k$
104	103	iffalsed	$⊢ x \in (A ∖ k) \to if (x \in k, v, ⋃ R) = ⋃ R$
105	104	adantl	$⊢ (((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land x \in (A ∖ k)) \to if (x \in k, v, ⋃ R) = ⋃ R$
106		eldifi	$⊢ x \in (A ∖ k) \to x \in A$
107	106 101	sylan2	$⊢ (((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land x \in (A ∖ k)) \to (A \times \{R\}) (x) = R$
108	107	unieqd	$⊢ (((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land x \in (A ∖ k)) \to ⋃ (A \times \{R\}) (x) = ⋃ R$
109	105 108	eqtr4d	$⊢ (((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \land x \in (A ∖ k)) \to if (x \in k, v, ⋃ R) = ⋃ (A \times \{R\}) (x)$
110	84 93 94 102 109	ptopn	$⊢ ((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \to \underset{x \in A}{⨉} if (x \in k, v, ⋃ R) \in \prod_{𝑡} (A \times \{R\})$
111	92 110	eqeltrd	$⊢ ((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \to \{f \in ({⋃ R}^{A}) \| f [k] \subseteq v\} \in \prod_{𝑡} (A \times \{R\})$
112		eleq1	$⊢ x = \{f \in ({⋃ R}^{A}) \| f [k] \subseteq v\} \to (x \in \prod_{𝑡} (A \times \{R\}) \leftrightarrow \{f \in ({⋃ R}^{A}) \| f [k] \subseteq v\} \in \prod_{𝑡} (A \times \{R\}))$
113	111 112	syl5ibrcom	$⊢ ((R \in Top \land A \in V) \land (k \in (𝒫 A \cap Fin) \land v \in R)) \to (x = \{f \in ({⋃ R}^{A}) \| f [k] \subseteq v\} \to x \in \prod_{𝑡} (A \times \{R\}))$
114	113	rexlimdvva	$⊢ (R \in Top \land A \in V) \to (\exists k \in (𝒫 A \cap Fin) \exists v \in R x = \{f \in ({⋃ R}^{A}) \| f [k] \subseteq v\} \to x \in \prod_{𝑡} (A \times \{R\}))$
115	114	abssdv	$⊢ (R \in Top \land A \in V) \to \{x \| \exists k \in (𝒫 A \cap Fin) \exists v \in R x = \{f \in ({⋃ R}^{A}) \| f [k] \subseteq v\}\} \subseteq \prod_{𝑡} (A \times \{R\})$
116	34 115	eqsstrd	$⊢ (R \in Top \land A \in V) \to ran (k \in \{x \in 𝒫 A \| 𝒫 A ↾_{𝑡} x \in Comp\}, v \in R ⟼ \{f \in (𝒫 A Cn R) \| f [k] \subseteq v\}) \subseteq \prod_{𝑡} (A \times \{R\})$
117		tgfiss	$⊢ (\prod_{𝑡} (A \times \{R\}) \in Top \land ran (k \in \{x \in 𝒫 A \| 𝒫 A ↾_{𝑡} x \in Comp\}, v \in R ⟼ \{f \in (𝒫 A Cn R) \| f [k] \subseteq v\}) \subseteq \prod_{𝑡} (A \times \{R\})) \to topGen (fi (ran (k \in \{x \in 𝒫 A \| 𝒫 A ↾_{𝑡} x \in Comp\}, v \in R ⟼ \{f \in (𝒫 A Cn R) \| f [k] \subseteq v\}))) \subseteq \prod_{𝑡} (A \times \{R\})$
118	13 116 117	syl2anc	$⊢ (R \in Top \land A \in V) \to topGen (fi (ran (k \in \{x \in 𝒫 A \| 𝒫 A ↾_{𝑡} x \in Comp\}, v \in R ⟼ \{f \in (𝒫 A Cn R) \| f [k] \subseteq v\}))) \subseteq \prod_{𝑡} (A \times \{R\})$
119	8 118	eqsstrd	$⊢ (R \in Top \land A \in V) \to R^_{ko} 𝒫 A \subseteq \prod_{𝑡} (A \times \{R\})$
120		eqid	$⊢ \prod_{𝑡} (A \times \{R\}) = \prod_{𝑡} (A \times \{R\})$
121	120 96	ptuniconst	$⊢ (A \in V \land R \in Top) \to {⋃ R}^{A} = ⋃ \prod_{𝑡} (A \times \{R\})$
122	121	ancoms	$⊢ (R \in Top \land A \in V) \to {⋃ R}^{A} = ⋃ \prod_{𝑡} (A \times \{R\})$
123	28 122	eqtrd	$⊢ (R \in Top \land A \in V) \to 𝒫 A Cn R = ⋃ \prod_{𝑡} (A \times \{R\})$
124	123	oveq2d	$⊢ (R \in Top \land A \in V) \to \prod_{𝑡} (A \times \{R\}) ↾_{𝑡} (𝒫 A Cn R) = \prod_{𝑡} (A \times \{R\}) ↾_{𝑡} ⋃ \prod_{𝑡} (A \times \{R\})$
125		eqid	$⊢ ⋃ \prod_{𝑡} (A \times \{R\}) = ⋃ \prod_{𝑡} (A \times \{R\})$
126	125	restid	$⊢ \prod_{𝑡} (A \times \{R\}) \in Top \to \prod_{𝑡} (A \times \{R\}) ↾_{𝑡} ⋃ \prod_{𝑡} (A \times \{R\}) = \prod_{𝑡} (A \times \{R\})$
127	13 126	syl	$⊢ (R \in Top \land A \in V) \to \prod_{𝑡} (A \times \{R\}) ↾_{𝑡} ⋃ \prod_{𝑡} (A \times \{R\}) = \prod_{𝑡} (A \times \{R\})$
128	124 127	eqtrd	$⊢ (R \in Top \land A \in V) \to \prod_{𝑡} (A \times \{R\}) ↾_{𝑡} (𝒫 A Cn R) = \prod_{𝑡} (A \times \{R\})$
129	4 120	xkoptsub	$⊢ (𝒫 A \in Top \land R \in Top) \to \prod_{𝑡} (A \times \{R\}) ↾_{𝑡} (𝒫 A Cn R) \subseteq R^_{ko} 𝒫 A$
130	1 2 129	syl2an2	$⊢ (R \in Top \land A \in V) \to \prod_{𝑡} (A \times \{R\}) ↾_{𝑡} (𝒫 A Cn R) \subseteq R^_{ko} 𝒫 A$
131	128 130	eqsstrrd	$⊢ (R \in Top \land A \in V) \to \prod_{𝑡} (A \times \{R\}) \subseteq R^_{ko} 𝒫 A$
132	119 131	eqssd	$⊢ (R \in Top \land A \in V) \to R^_{ko} 𝒫 A = \prod_{𝑡} (A \times \{R\})$

Metamath Proof Explorer

Theorem xkopt

Proof