prdstopn

Description: Topology of a structure product. (Contributed by Mario Carneiro, 27-Aug-2015)

	Ref	Expression
Hypotheses	prdstopn.y	$⊢ Y = S ⨉_{𝑠} R$
	prdstopn.s	$⊢ φ \to S \in V$
	prdstopn.i	$⊢ φ \to I \in W$
	prdstopn.r	$⊢ φ \to R Fn I$
	prdstopn.o	$⊢ O = TopOpen (Y)$
Assertion	prdstopn	$⊢ φ \to O = \prod_{𝑡} (TopOpen \circ R)$

Proof

Step	Hyp	Ref	Expression
1		prdstopn.y	$⊢ Y = S ⨉_{𝑠} R$
2		prdstopn.s	$⊢ φ \to S \in V$
3		prdstopn.i	$⊢ φ \to I \in W$
4		prdstopn.r	$⊢ φ \to R Fn I$
5		prdstopn.o	$⊢ O = TopOpen (Y)$
6		fnex	$⊢ (R Fn I \land I \in W) \to R \in V$
7	4 3 6	syl2anc	$⊢ φ \to R \in V$
8		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
9		eqidd	$⊢ φ \to dom R = dom R$
10		eqid	$⊢ TopSet (Y) = TopSet (Y)$
11	1 2 7 8 9 10	prdstset	$⊢ φ \to TopSet (Y) = \prod_{𝑡} (TopOpen \circ R)$
12		topnfn	$⊢ TopOpen Fn V$
13		dffn2	$⊢ R Fn I \leftrightarrow R : I ⟶ V$
14	4 13	sylib	$⊢ φ \to R : I ⟶ V$
15		fnfco	$⊢ (TopOpen Fn V \land R : I ⟶ V) \to (TopOpen \circ R) Fn I$
16	12 14 15	sylancr	$⊢ φ \to (TopOpen \circ R) Fn I$
17		eqid	$⊢ \{x \| \exists g ((g Fn I \land \forall y \in I g (y) \in (TopOpen \circ R) (y) \land \exists z \in Fin \forall y \in (I ∖ z) g (y) = ⋃ (TopOpen \circ R) (y)) \land x = \underset{y \in I}{⨉} g (y))\} = \{x \| \exists g ((g Fn I \land \forall y \in I g (y) \in (TopOpen \circ R) (y) \land \exists z \in Fin \forall y \in (I ∖ z) g (y) = ⋃ (TopOpen \circ R) (y)) \land x = \underset{y \in I}{⨉} g (y))\}$
18	17	ptval	$⊢ (I \in W \land (TopOpen \circ R) Fn I) \to \prod_{𝑡} (TopOpen \circ R) = topGen (\{x \| \exists g ((g Fn I \land \forall y \in I g (y) \in (TopOpen \circ R) (y) \land \exists z \in Fin \forall y \in (I ∖ z) g (y) = ⋃ (TopOpen \circ R) (y)) \land x = \underset{y \in I}{⨉} g (y))\})$
19	3 16 18	syl2anc	$⊢ φ \to \prod_{𝑡} (TopOpen \circ R) = topGen (\{x \| \exists g ((g Fn I \land \forall y \in I g (y) \in (TopOpen \circ R) (y) \land \exists z \in Fin \forall y \in (I ∖ z) g (y) = ⋃ (TopOpen \circ R) (y)) \land x = \underset{y \in I}{⨉} g (y))\})$
20	19	unieqd	$⊢ φ \to ⋃ \prod_{𝑡} (TopOpen \circ R) = ⋃ topGen (\{x \| \exists g ((g Fn I \land \forall y \in I g (y) \in (TopOpen \circ R) (y) \land \exists z \in Fin \forall y \in (I ∖ z) g (y) = ⋃ (TopOpen \circ R) (y)) \land x = \underset{y \in I}{⨉} g (y))\})$
21		fvco2	$⊢ (R Fn I \land y \in I) \to (TopOpen \circ R) (y) = TopOpen (R (y))$
22	4 21	sylan	$⊢ (φ \land y \in I) \to (TopOpen \circ R) (y) = TopOpen (R (y))$
23		eqid	$⊢ {Base}_{R (y)} = {Base}_{R (y)}$
24		eqid	$⊢ TopSet (R (y)) = TopSet (R (y))$
25	23 24	topnval	$⊢ TopSet (R (y)) ↾_{𝑡} {Base}_{R (y)} = TopOpen (R (y))$
26		restsspw	$⊢ TopSet (R (y)) ↾_{𝑡} {Base}_{R (y)} \subseteq 𝒫 {Base}_{R (y)}$
27	25 26	eqsstrri	$⊢ TopOpen (R (y)) \subseteq 𝒫 {Base}_{R (y)}$
28	22 27	eqsstrdi	$⊢ (φ \land y \in I) \to (TopOpen \circ R) (y) \subseteq 𝒫 {Base}_{R (y)}$
29	28	sseld	$⊢ (φ \land y \in I) \to (g (y) \in (TopOpen \circ R) (y) \to g (y) \in 𝒫 {Base}_{R (y)})$
30		fvex	$⊢ g (y) \in V$
31	30	elpw	$⊢ g (y) \in 𝒫 {Base}_{R (y)} \leftrightarrow g (y) \subseteq {Base}_{R (y)}$
32	29 31	imbitrdi	$⊢ (φ \land y \in I) \to (g (y) \in (TopOpen \circ R) (y) \to g (y) \subseteq {Base}_{R (y)})$
33	32	ralimdva	$⊢ φ \to (\forall y \in I g (y) \in (TopOpen \circ R) (y) \to \forall y \in I g (y) \subseteq {Base}_{R (y)})$
34		simpl2	$⊢ ((g Fn I \land \forall y \in I g (y) \in (TopOpen \circ R) (y) \land \exists z \in Fin \forall y \in (I ∖ z) g (y) = ⋃ (TopOpen \circ R) (y)) \land x = \underset{y \in I}{⨉} g (y)) \to \forall y \in I g (y) \in (TopOpen \circ R) (y)$
35	33 34	impel	$⊢ (φ \land ((g Fn I \land \forall y \in I g (y) \in (TopOpen \circ R) (y) \land \exists z \in Fin \forall y \in (I ∖ z) g (y) = ⋃ (TopOpen \circ R) (y)) \land x = \underset{y \in I}{⨉} g (y))) \to \forall y \in I g (y) \subseteq {Base}_{R (y)}$
36		ss2ixp	$⊢ \forall y \in I g (y) \subseteq {Base}_{R (y)} \to \underset{y \in I}{⨉} g (y) \subseteq \underset{y \in I}{⨉} {Base}_{R (y)}$
37	35 36	syl	$⊢ (φ \land ((g Fn I \land \forall y \in I g (y) \in (TopOpen \circ R) (y) \land \exists z \in Fin \forall y \in (I ∖ z) g (y) = ⋃ (TopOpen \circ R) (y)) \land x = \underset{y \in I}{⨉} g (y))) \to \underset{y \in I}{⨉} g (y) \subseteq \underset{y \in I}{⨉} {Base}_{R (y)}$
38		simprr	$⊢ (φ \land ((g Fn I \land \forall y \in I g (y) \in (TopOpen \circ R) (y) \land \exists z \in Fin \forall y \in (I ∖ z) g (y) = ⋃ (TopOpen \circ R) (y)) \land x = \underset{y \in I}{⨉} g (y))) \to x = \underset{y \in I}{⨉} g (y)$
39	1 8 2 3 4	prdsbas2	$⊢ φ \to {Base}_{Y} = \underset{y \in I}{⨉} {Base}_{R (y)}$
40	39	adantr	$⊢ (φ \land ((g Fn I \land \forall y \in I g (y) \in (TopOpen \circ R) (y) \land \exists z \in Fin \forall y \in (I ∖ z) g (y) = ⋃ (TopOpen \circ R) (y)) \land x = \underset{y \in I}{⨉} g (y))) \to {Base}_{Y} = \underset{y \in I}{⨉} {Base}_{R (y)}$
41	37 38 40	3sstr4d	$⊢ (φ \land ((g Fn I \land \forall y \in I g (y) \in (TopOpen \circ R) (y) \land \exists z \in Fin \forall y \in (I ∖ z) g (y) = ⋃ (TopOpen \circ R) (y)) \land x = \underset{y \in I}{⨉} g (y))) \to x \subseteq {Base}_{Y}$
42	41	ex	$⊢ φ \to (((g Fn I \land \forall y \in I g (y) \in (TopOpen \circ R) (y) \land \exists z \in Fin \forall y \in (I ∖ z) g (y) = ⋃ (TopOpen \circ R) (y)) \land x = \underset{y \in I}{⨉} g (y)) \to x \subseteq {Base}_{Y})$
43	42	exlimdv	$⊢ φ \to (\exists g ((g Fn I \land \forall y \in I g (y) \in (TopOpen \circ R) (y) \land \exists z \in Fin \forall y \in (I ∖ z) g (y) = ⋃ (TopOpen \circ R) (y)) \land x = \underset{y \in I}{⨉} g (y)) \to x \subseteq {Base}_{Y})$
44		velpw	$⊢ x \in 𝒫 {Base}_{Y} \leftrightarrow x \subseteq {Base}_{Y}$
45	43 44	imbitrrdi	$⊢ φ \to (\exists g ((g Fn I \land \forall y \in I g (y) \in (TopOpen \circ R) (y) \land \exists z \in Fin \forall y \in (I ∖ z) g (y) = ⋃ (TopOpen \circ R) (y)) \land x = \underset{y \in I}{⨉} g (y)) \to x \in 𝒫 {Base}_{Y})$
46	45	abssdv	$⊢ φ \to \{x \| \exists g ((g Fn I \land \forall y \in I g (y) \in (TopOpen \circ R) (y) \land \exists z \in Fin \forall y \in (I ∖ z) g (y) = ⋃ (TopOpen \circ R) (y)) \land x = \underset{y \in I}{⨉} g (y))\} \subseteq 𝒫 {Base}_{Y}$
47		fvex	$⊢ {Base}_{Y} \in V$
48	47	pwex	$⊢ 𝒫 {Base}_{Y} \in V$
49	48	ssex	$⊢ \{x \| \exists g ((g Fn I \land \forall y \in I g (y) \in (TopOpen \circ R) (y) \land \exists z \in Fin \forall y \in (I ∖ z) g (y) = ⋃ (TopOpen \circ R) (y)) \land x = \underset{y \in I}{⨉} g (y))\} \subseteq 𝒫 {Base}_{Y} \to \{x \| \exists g ((g Fn I \land \forall y \in I g (y) \in (TopOpen \circ R) (y) \land \exists z \in Fin \forall y \in (I ∖ z) g (y) = ⋃ (TopOpen \circ R) (y)) \land x = \underset{y \in I}{⨉} g (y))\} \in V$
50		unitg	$⊢ \{x \| \exists g ((g Fn I \land \forall y \in I g (y) \in (TopOpen \circ R) (y) \land \exists z \in Fin \forall y \in (I ∖ z) g (y) = ⋃ (TopOpen \circ R) (y)) \land x = \underset{y \in I}{⨉} g (y))\} \in V \to ⋃ topGen (\{x \| \exists g ((g Fn I \land \forall y \in I g (y) \in (TopOpen \circ R) (y) \land \exists z \in Fin \forall y \in (I ∖ z) g (y) = ⋃ (TopOpen \circ R) (y)) \land x = \underset{y \in I}{⨉} g (y))\}) = ⋃ \{x \| \exists g ((g Fn I \land \forall y \in I g (y) \in (TopOpen \circ R) (y) \land \exists z \in Fin \forall y \in (I ∖ z) g (y) = ⋃ (TopOpen \circ R) (y)) \land x = \underset{y \in I}{⨉} g (y))\}$
51	46 49 50	3syl	$⊢ φ \to ⋃ topGen (\{x \| \exists g ((g Fn I \land \forall y \in I g (y) \in (TopOpen \circ R) (y) \land \exists z \in Fin \forall y \in (I ∖ z) g (y) = ⋃ (TopOpen \circ R) (y)) \land x = \underset{y \in I}{⨉} g (y))\}) = ⋃ \{x \| \exists g ((g Fn I \land \forall y \in I g (y) \in (TopOpen \circ R) (y) \land \exists z \in Fin \forall y \in (I ∖ z) g (y) = ⋃ (TopOpen \circ R) (y)) \land x = \underset{y \in I}{⨉} g (y))\}$
52	20 51	eqtrd	$⊢ φ \to ⋃ \prod_{𝑡} (TopOpen \circ R) = ⋃ \{x \| \exists g ((g Fn I \land \forall y \in I g (y) \in (TopOpen \circ R) (y) \land \exists z \in Fin \forall y \in (I ∖ z) g (y) = ⋃ (TopOpen \circ R) (y)) \land x = \underset{y \in I}{⨉} g (y))\}$
53		sspwuni	$⊢ \{x \| \exists g ((g Fn I \land \forall y \in I g (y) \in (TopOpen \circ R) (y) \land \exists z \in Fin \forall y \in (I ∖ z) g (y) = ⋃ (TopOpen \circ R) (y)) \land x = \underset{y \in I}{⨉} g (y))\} \subseteq 𝒫 {Base}_{Y} \leftrightarrow ⋃ \{x \| \exists g ((g Fn I \land \forall y \in I g (y) \in (TopOpen \circ R) (y) \land \exists z \in Fin \forall y \in (I ∖ z) g (y) = ⋃ (TopOpen \circ R) (y)) \land x = \underset{y \in I}{⨉} g (y))\} \subseteq {Base}_{Y}$
54	46 53	sylib	$⊢ φ \to ⋃ \{x \| \exists g ((g Fn I \land \forall y \in I g (y) \in (TopOpen \circ R) (y) \land \exists z \in Fin \forall y \in (I ∖ z) g (y) = ⋃ (TopOpen \circ R) (y)) \land x = \underset{y \in I}{⨉} g (y))\} \subseteq {Base}_{Y}$
55	52 54	eqsstrd	$⊢ φ \to ⋃ \prod_{𝑡} (TopOpen \circ R) \subseteq {Base}_{Y}$
56		sspwuni	$⊢ \prod_{𝑡} (TopOpen \circ R) \subseteq 𝒫 {Base}_{Y} \leftrightarrow ⋃ \prod_{𝑡} (TopOpen \circ R) \subseteq {Base}_{Y}$
57	55 56	sylibr	$⊢ φ \to \prod_{𝑡} (TopOpen \circ R) \subseteq 𝒫 {Base}_{Y}$
58	11 57	eqsstrd	$⊢ φ \to TopSet (Y) \subseteq 𝒫 {Base}_{Y}$
59	8 10	topnid	$⊢ TopSet (Y) \subseteq 𝒫 {Base}_{Y} \to TopSet (Y) = TopOpen (Y)$
60	58 59	syl	$⊢ φ \to TopSet (Y) = TopOpen (Y)$
61	60 5	eqtr4di	$⊢ φ \to TopSet (Y) = O$
62	61 11	eqtr3d	$⊢ φ \to O = \prod_{𝑡} (TopOpen \circ R)$

Metamath Proof Explorer

Theorem prdstopn

Proof