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		1oelpr	$⊢ 1_{𝑜} \in \{\emptyset, 1_{𝑜}\}$
35	34 24	eleqtrri	$⊢ 1_{𝑜} \in 2_{𝑜}$
36		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_{𝑜}))$
37	12 35 36	sylancl	$⊢ (R \in TopSp \land S \in TopSp) \to (TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) (1_{𝑜}) = TopOpen (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (1_{𝑜}))$
38		fvpr1o	$⊢ S \in TopSp \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (1_{𝑜}) = S$
39	38	adantl	$⊢ (R \in TopSp \land S \in TopSp) \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (1_{𝑜}) = S$
40	39	fveq2d	$⊢ (R \in TopSp \land S \in TopSp) \to TopOpen (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (1_{𝑜})) = TopOpen (S)$
41	40 3	eqtr4di	$⊢ (R \in TopSp \land S \in TopSp) \to TopOpen (\{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} (1_{𝑜})) = K$
42	37 41	eqtrd	$⊢ (R \in TopSp \land S \in TopSp) \to (TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) (1_{𝑜}) = K$
43	42	opeq2d	$⊢ (R \in TopSp \land S \in TopSp) \to ⟨1_{𝑜}, (TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) (1_{𝑜})⟩ = ⟨1_{𝑜}, K⟩$
44	33 43	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⟩\}$
45	21 44	eqtr3d	$⊢ (R \in TopSp \land S \in TopSp) \to TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} = \{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\}$
46	45	fveq2d	$⊢ (R \in TopSp \land S \in TopSp) \to \prod_{𝑡} (TopOpen \circ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) = \prod_{𝑡} (\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\})$
47	14 46	eqtrd	$⊢ (R \in TopSp \land S \in TopSp) \to TopOpen (Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) = \prod_{𝑡} (\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\})$
48	47	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}$
49		simpl	$⊢ (R \in TopSp \land S \in TopSp) \to R \in TopSp$
50		simpr	$⊢ (R \in TopSp \land S \in TopSp) \to S \in TopSp$
51		eqid	$⊢ Scalar (R) = Scalar (R)$
52	1 5 6 49 50 7 51 8	xpsval	$⊢ (R \in TopSp \land S \in TopSp) \to T = F^{-1} “_{𝑠} (Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})$
53	1 5 6 49 50 7 51 8	xpsrnbas	$⊢ (R \in TopSp \land S \in TopSp) \to ran F = {Base}_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})}$
54	7	xpsff1o2	$⊢ F : X \times Y \underset{1-1 onto}{⟶} ran F$
55		f1ocnv	$⊢ F : X \times Y \underset{1-1 onto}{⟶} ran F \to F^{-1} : ran F \underset{1-1 onto}{⟶} X \times Y$
56	54 55	mp1i	$⊢ (R \in TopSp \land S \in TopSp) \to F^{-1} : ran F \underset{1-1 onto}{⟶} X \times Y$
57		f1ofo	$⊢ F^{-1} : ran F \underset{1-1 onto}{⟶} X \times Y \to F^{-1} : ran F \underset{onto}{⟶} X \times Y$
58	56 57	syl	$⊢ (R \in TopSp \land S \in TopSp) \to F^{-1} : ran F \underset{onto}{⟶} X \times Y$
59		ovexd	$⊢ (R \in TopSp \land S \in TopSp) \to Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} \in V$
60	52 53 58 59 13 4	imastopn	$⊢ (R \in TopSp \land S \in TopSp) \to O = TopOpen (Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}) qTop F^{-1}$
61	5 2	istps	$⊢ R \in TopSp \leftrightarrow J \in TopOn (X)$
62	49 61	sylib	$⊢ (R \in TopSp \land S \in TopSp) \to J \in TopOn (X)$
63	6 3	istps	$⊢ S \in TopSp \leftrightarrow K \in TopOn (Y)$
64	50 63	sylib	$⊢ (R \in TopSp \land S \in TopSp) \to K \in TopOn (Y)$
65	7 62 64	xpstopnlem1	$⊢ (R \in TopSp \land S \in TopSp) \to F \in ((J \times_{t} K) Homeo \prod_{𝑡} (\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\}))$
66		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))$
67		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}$
68	65 66 67	3syl	$⊢ (R \in TopSp \land S \in TopSp) \to J \times_{t} K = \prod_{𝑡} (\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\}) qTop F^{-1}$
69	48 60 68	3eqtr4d	$⊢ (R \in TopSp \land S \in TopSp) \to O = J \times_{t} K$

Metamath Proof Explorer

Theorem xpstopnlem2

Proof