xpstopnlem2

	Ref	Expression
Hypotheses	xpstps.t	$⊢ T = R \times_{𝑠} S$
	xpstopn.j	$⊢ J = TopOpen (R)$
	xpstopn.k	$⊢ K = TopOpen (S)$
	xpstopn.o	$⊢ O = TopOpen (T)$
	xpstopnlem.x	$⊢ X = {Base}_{R}$
	xpstopnlem.y	$⊢ Y = {Base}_{S}$
	xpstopnlem.f	$⊢ F = (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})$
Assertion	xpstopnlem2	$⊢ (R \in TopSp \land S \in TopSp) \to O = J \times_{t} K$

Proof

Step	Hyp	Ref	Expression
1		xpstps.t	$⊢ T = R \times_{𝑠} S$
2		xpstopn.j	$⊢ J = TopOpen (R)$
3		xpstopn.k	$⊢ K = TopOpen (S)$
4		xpstopn.o	$⊢ O = TopOpen (T)$
5		xpstopnlem.x	$⊢ X = {Base}_{R}$
6		xpstopnlem.y	$⊢ Y = {Base}_{S}$
7		xpstopnlem.f	$⊢ F = (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})$
8		eqid	$⊢ Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} = Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}$
9		fvexd	$⊢ (R \in TopSp \land S \in TopSp) \to Scalar (R) \in V$
10		2on	$⊢ 2_{𝑜} \in On$
11	10	a1i	$⊢ (R \in TopSp \land S \in TopSp) \to 2_{𝑜} \in On$
12		fnpr2o	$⊢ (R \in TopSp \land S \in TopSp) \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} Fn 2_{𝑜}$
13		eqid	$⊢ TopOpen (Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) = TopOpen (Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})$
14	8 9 11 12 13	prdstopn	$⊢ (R \in TopSp \land S \in TopSp) \to TopOpen (Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) = \prod_{𝑡} (TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})$
15		topnfn	$⊢ TopOpen Fn V$
16		dffn2	$⊢ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} Fn 2_{𝑜} \leftrightarrow \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} : 2_{𝑜} ⟶ V$
17	12 16	sylib	$⊢ (R \in TopSp \land S \in TopSp) \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} : 2_{𝑜} ⟶ V$
18		fnfco	$⊢ (TopOpen Fn V \land \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} : 2_{𝑜} ⟶ V) \to (TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) Fn 2_{𝑜}$
19	15 17 18	sylancr	$⊢ (R \in TopSp \land S \in TopSp) \to (TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) Fn 2_{𝑜}$
20		xpsfeq	$⊢ (TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) Fn 2_{𝑜} \to \{⟨\emptyset, (TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) (\emptyset)⟩, ⟨1_{𝑜}, (TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) (1_{𝑜})⟩\} = TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}$
21	19 20	syl	$⊢ (R \in TopSp \land S \in TopSp) \to \{⟨\emptyset, (TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) (\emptyset)⟩, ⟨1_{𝑜}, (TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) (1_{𝑜})⟩\} = TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}$
22		0ex	$⊢ \emptyset \in V$
23	22	prid1	$⊢ \emptyset \in \{\emptyset, 1_{𝑜}\}$
24		df2o3	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$
25	23 24	eleqtrri	$⊢ \emptyset \in 2_{𝑜}$
26		fvco2	$⊢ (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} Fn 2_{𝑜} \land \emptyset \in 2_{𝑜}) \to (TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) (\emptyset) = TopOpen (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (\emptyset))$
27	12 25 26	sylancl	$⊢ (R \in TopSp \land S \in TopSp) \to (TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) (\emptyset) = TopOpen (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (\emptyset))$
28		fvpr0o	$⊢ R \in TopSp \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (\emptyset) = R$
29	28	adantr	$⊢ (R \in TopSp \land S \in TopSp) \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (\emptyset) = R$
30	29	fveq2d	$⊢ (R \in TopSp \land S \in TopSp) \to TopOpen (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (\emptyset)) = TopOpen (R)$
31	30 2	eqtr4di	$⊢ (R \in TopSp \land S \in TopSp) \to TopOpen (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (\emptyset)) = J$
32	27 31	eqtrd	$⊢ (R \in TopSp \land S \in TopSp) \to (TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) (\emptyset) = J$
33	32	opeq2d	$⊢ (R \in TopSp \land S \in TopSp) \to ⟨\emptyset, (TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) (\emptyset)⟩ = ⟨\emptyset, J⟩$
34		1oex	$⊢ 1_{𝑜} \in V$
35	34	prid2	$⊢ 1_{𝑜} \in \{\emptyset, 1_{𝑜}\}$
36	35 24	eleqtrri	$⊢ 1_{𝑜} \in 2_{𝑜}$
37		fvco2	$⊢ (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} Fn 2_{𝑜} \land 1_{𝑜} \in 2_{𝑜}) \to (TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) (1_{𝑜}) = TopOpen (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (1_{𝑜}))$
38	12 36 37	sylancl	$⊢ (R \in TopSp \land S \in TopSp) \to (TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) (1_{𝑜}) = TopOpen (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (1_{𝑜}))$
39		fvpr1o	$⊢ S \in TopSp \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (1_{𝑜}) = S$
40	39	adantl	$⊢ (R \in TopSp \land S \in TopSp) \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (1_{𝑜}) = S$
41	40	fveq2d	$⊢ (R \in TopSp \land S \in TopSp) \to TopOpen (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (1_{𝑜})) = TopOpen (S)$
42	41 3	eqtr4di	$⊢ (R \in TopSp \land S \in TopSp) \to TopOpen (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (1_{𝑜})) = K$
43	38 42	eqtrd	$⊢ (R \in TopSp \land S \in TopSp) \to (TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) (1_{𝑜}) = K$
44	43	opeq2d	$⊢ (R \in TopSp \land S \in TopSp) \to ⟨1_{𝑜}, (TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) (1_{𝑜})⟩ = ⟨1_{𝑜}, K⟩$
45	33 44	preq12d	$⊢ (R \in TopSp \land S \in TopSp) \to \{⟨\emptyset, (TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) (\emptyset)⟩, ⟨1_{𝑜}, (TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) (1_{𝑜})⟩\} = \{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\}$
46	21 45	eqtr3d	$⊢ (R \in TopSp \land S \in TopSp) \to TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} = \{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\}$
47	46	fveq2d	$⊢ (R \in TopSp \land S \in TopSp) \to \prod_{𝑡} (TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) = \prod_{𝑡} (\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\})$
48	14 47	eqtrd	$⊢ (R \in TopSp \land S \in TopSp) \to TopOpen (Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) = \prod_{𝑡} (\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\})$
49	48	oveq1d	$⊢ (R \in TopSp \land S \in TopSp) \to TopOpen (Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) qTop F^{-1} = \prod_{𝑡} (\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\}) qTop F^{-1}$
50		simpl	$⊢ (R \in TopSp \land S \in TopSp) \to R \in TopSp$
51		simpr	$⊢ (R \in TopSp \land S \in TopSp) \to S \in TopSp$
52		eqid	$⊢ Scalar (R) = Scalar (R)$
53	1 5 6 50 51 7 52 8	xpsval	$⊢ (R \in TopSp \land S \in TopSp) \to T = F^{-1} “_{𝑠} (Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})$
54	1 5 6 50 51 7 52 8	xpsrnbas	$⊢ (R \in TopSp \land S \in TopSp) \to ran F = {Base}_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})}$
55	7	xpsff1o2	$⊢ F : X \times Y \underset{1-1 onto}{⟶} ran F$
56		f1ocnv	$⊢ F : X \times Y \underset{1-1 onto}{⟶} ran F \to F^{-1} : ran F \underset{1-1 onto}{⟶} X \times Y$
57	55 56	mp1i	$⊢ (R \in TopSp \land S \in TopSp) \to F^{-1} : ran F \underset{1-1 onto}{⟶} X \times Y$
58		f1ofo	$⊢ F^{-1} : ran F \underset{1-1 onto}{⟶} X \times Y \to F^{-1} : ran F \underset{onto}{⟶} X \times Y$
59	57 58	syl	$⊢ (R \in TopSp \land S \in TopSp) \to F^{-1} : ran F \underset{onto}{⟶} X \times Y$
60		ovexd	$⊢ (R \in TopSp \land S \in TopSp) \to Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} \in V$
61	53 54 59 60 13 4	imastopn	$⊢ (R \in TopSp \land S \in TopSp) \to O = TopOpen (Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) qTop F^{-1}$
62	5 2	istps	$⊢ R \in TopSp \leftrightarrow J \in TopOn (X)$
63	50 62	sylib	$⊢ (R \in TopSp \land S \in TopSp) \to J \in TopOn (X)$
64	6 3	istps	$⊢ S \in TopSp \leftrightarrow K \in TopOn (Y)$
65	51 64	sylib	$⊢ (R \in TopSp \land S \in TopSp) \to K \in TopOn (Y)$
66	7 63 65	xpstopnlem1	$⊢ (R \in TopSp \land S \in TopSp) \to F \in ((J \times_{t} K) Homeo \prod_{𝑡} (\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\}))$
67		hmeocnv	$⊢ F \in ((J \times_{t} K) Homeo \prod_{𝑡} (\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\})) \to F^{-1} \in (\prod_{𝑡} (\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\}) Homeo (J \times_{t} K))$
68		hmeoqtop	$⊢ F^{-1} \in (\prod_{𝑡} (\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\}) Homeo (J \times_{t} K)) \to J \times_{t} K = \prod_{𝑡} (\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\}) qTop F^{-1}$
69	66 67 68	3syl	$⊢ (R \in TopSp \land S \in TopSp) \to J \times_{t} K = \prod_{𝑡} (\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\}) qTop F^{-1}$
70	49 61 69	3eqtr4d	$⊢ (R \in TopSp \land S \in TopSp) \to O = J \times_{t} K$

Metamath Proof Explorer

Theorem xpstopnlem2

Proof