xpstopnlem1

Description: The function F used in xpsval is a homeomorphism from the binary product topology to the indexed product topology. (Contributed by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Hypotheses	xpstopnlem1.f	$⊢ F = (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})$
	xpstopnlem1.j	$⊢ φ \to J \in TopOn (X)$
	xpstopnlem1.k	$⊢ φ \to K \in TopOn (Y)$
Assertion	xpstopnlem1	$⊢ φ \to F \in ((J \times_{t} K) Homeo \prod_{𝑡} (\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\}))$

Proof

Step	Hyp	Ref	Expression
1		xpstopnlem1.f	$⊢ F = (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})$
2		xpstopnlem1.j	$⊢ φ \to J \in TopOn (X)$
3		xpstopnlem1.k	$⊢ φ \to K \in TopOn (Y)$
4		txtopon	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to J \times_{t} K \in TopOn (X \times Y)$
5	2 3 4	syl2anc	$⊢ φ \to J \times_{t} K \in TopOn (X \times Y)$
6		eqid	$⊢ \prod_{𝑡} (\{⟨\emptyset, J⟩\}) = \prod_{𝑡} (\{⟨\emptyset, J⟩\})$
7		0ex	$⊢ \emptyset \in V$
8	7	a1i	$⊢ φ \to \emptyset \in V$
9	6 8 2	pt1hmeo	$⊢ φ \to (z \in X ⟼ \{⟨\emptyset, z⟩\}) \in (J Homeo \prod_{𝑡} (\{⟨\emptyset, J⟩\}))$
10		hmeocn	$⊢ (z \in X ⟼ \{⟨\emptyset, z⟩\}) \in (J Homeo \prod_{𝑡} (\{⟨\emptyset, J⟩\})) \to (z \in X ⟼ \{⟨\emptyset, z⟩\}) \in (J Cn \prod_{𝑡} (\{⟨\emptyset, J⟩\}))$
11		cntop2	$⊢ (z \in X ⟼ \{⟨\emptyset, z⟩\}) \in (J Cn \prod_{𝑡} (\{⟨\emptyset, J⟩\})) \to \prod_{𝑡} (\{⟨\emptyset, J⟩\}) \in Top$
12	9 10 11	3syl	$⊢ φ \to \prod_{𝑡} (\{⟨\emptyset, J⟩\}) \in Top$
13		toptopon2	$⊢ \prod_{𝑡} (\{⟨\emptyset, J⟩\}) \in Top \leftrightarrow \prod_{𝑡} (\{⟨\emptyset, J⟩\}) \in TopOn (⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\}))$
14	12 13	sylib	$⊢ φ \to \prod_{𝑡} (\{⟨\emptyset, J⟩\}) \in TopOn (⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\}))$
15		eqid	$⊢ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}) = \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\})$
16		1on	$⊢ 1_{𝑜} \in On$
17	16	a1i	$⊢ φ \to 1_{𝑜} \in On$
18	15 17 3	pt1hmeo	$⊢ φ \to (z \in Y ⟼ \{⟨1_{𝑜}, z⟩\}) \in (K Homeo \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}))$
19		hmeocn	$⊢ (z \in Y ⟼ \{⟨1_{𝑜}, z⟩\}) \in (K Homeo \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\})) \to (z \in Y ⟼ \{⟨1_{𝑜}, z⟩\}) \in (K Cn \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}))$
20		cntop2	$⊢ (z \in Y ⟼ \{⟨1_{𝑜}, z⟩\}) \in (K Cn \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\})) \to \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}) \in Top$
21	18 19 20	3syl	$⊢ φ \to \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}) \in Top$
22		toptopon2	$⊢ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}) \in Top \leftrightarrow \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}) \in TopOn (⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}))$
23	21 22	sylib	$⊢ φ \to \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}) \in TopOn (⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}))$
24		txtopon	$⊢ (\prod_{𝑡} (\{⟨\emptyset, J⟩\}) \in TopOn (⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\})) \land \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}) \in TopOn (⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}))) \to \prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times_{t} \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}) \in TopOn (⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times ⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}))$
25	14 23 24	syl2anc	$⊢ φ \to \prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times_{t} \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}) \in TopOn (⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times ⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}))$
26		opeq2	$⊢ z = x \to ⟨\emptyset, z⟩ = ⟨\emptyset, x⟩$
27	26	sneqd	$⊢ z = x \to \{⟨\emptyset, z⟩\} = \{⟨\emptyset, x⟩\}$
28		eqid	$⊢ (z \in X ⟼ \{⟨\emptyset, z⟩\}) = (z \in X ⟼ \{⟨\emptyset, z⟩\})$
29		snex	$⊢ \{⟨\emptyset, x⟩\} \in V$
30	27 28 29	fvmpt	$⊢ x \in X \to (z \in X ⟼ \{⟨\emptyset, z⟩\}) (x) = \{⟨\emptyset, x⟩\}$
31		opeq2	$⊢ z = y \to ⟨1_{𝑜}, z⟩ = ⟨1_{𝑜}, y⟩$
32	31	sneqd	$⊢ z = y \to \{⟨1_{𝑜}, z⟩\} = \{⟨1_{𝑜}, y⟩\}$
33		eqid	$⊢ (z \in Y ⟼ \{⟨1_{𝑜}, z⟩\}) = (z \in Y ⟼ \{⟨1_{𝑜}, z⟩\})$
34		snex	$⊢ \{⟨1_{𝑜}, y⟩\} \in V$
35	32 33 34	fvmpt	$⊢ y \in Y \to (z \in Y ⟼ \{⟨1_{𝑜}, z⟩\}) (y) = \{⟨1_{𝑜}, y⟩\}$
36		opeq12	$⊢ ((z \in X ⟼ \{⟨\emptyset, z⟩\}) (x) = \{⟨\emptyset, x⟩\} \land (z \in Y ⟼ \{⟨1_{𝑜}, z⟩\}) (y) = \{⟨1_{𝑜}, y⟩\}) \to ⟨(z \in X ⟼ \{⟨\emptyset, z⟩\}) (x), (z \in Y ⟼ \{⟨1_{𝑜}, z⟩\}) (y)⟩ = ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩$
37	30 35 36	syl2an	$⊢ (x \in X \land y \in Y) \to ⟨(z \in X ⟼ \{⟨\emptyset, z⟩\}) (x), (z \in Y ⟼ \{⟨1_{𝑜}, z⟩\}) (y)⟩ = ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩$
38	37	mpoeq3ia	$⊢ (x \in X, y \in Y ⟼ ⟨(z \in X ⟼ \{⟨\emptyset, z⟩\}) (x), (z \in Y ⟼ \{⟨1_{𝑜}, z⟩\}) (y)⟩) = (x \in X, y \in Y ⟼ ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩)$
39		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
40	2 39	syl	$⊢ φ \to X = ⋃ J$
41		toponuni	$⊢ K \in TopOn (Y) \to Y = ⋃ K$
42	3 41	syl	$⊢ φ \to Y = ⋃ K$
43		mpoeq12	$⊢ (X = ⋃ J \land Y = ⋃ K) \to (x \in X, y \in Y ⟼ ⟨(z \in X ⟼ \{⟨\emptyset, z⟩\}) (x), (z \in Y ⟼ \{⟨1_{𝑜}, z⟩\}) (y)⟩) = (x \in ⋃ J, y \in ⋃ K ⟼ ⟨(z \in X ⟼ \{⟨\emptyset, z⟩\}) (x), (z \in Y ⟼ \{⟨1_{𝑜}, z⟩\}) (y)⟩)$
44	40 42 43	syl2anc	$⊢ φ \to (x \in X, y \in Y ⟼ ⟨(z \in X ⟼ \{⟨\emptyset, z⟩\}) (x), (z \in Y ⟼ \{⟨1_{𝑜}, z⟩\}) (y)⟩) = (x \in ⋃ J, y \in ⋃ K ⟼ ⟨(z \in X ⟼ \{⟨\emptyset, z⟩\}) (x), (z \in Y ⟼ \{⟨1_{𝑜}, z⟩\}) (y)⟩)$
45	38 44	eqtr3id	$⊢ φ \to (x \in X, y \in Y ⟼ ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩) = (x \in ⋃ J, y \in ⋃ K ⟼ ⟨(z \in X ⟼ \{⟨\emptyset, z⟩\}) (x), (z \in Y ⟼ \{⟨1_{𝑜}, z⟩\}) (y)⟩)$
46		eqid	$⊢ ⋃ J = ⋃ J$
47		eqid	$⊢ ⋃ K = ⋃ K$
48	46 47 9 18	txhmeo	$⊢ φ \to (x \in ⋃ J, y \in ⋃ K ⟼ ⟨(z \in X ⟼ \{⟨\emptyset, z⟩\}) (x), (z \in Y ⟼ \{⟨1_{𝑜}, z⟩\}) (y)⟩) \in ((J \times_{t} K) Homeo (\prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times_{t} \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\})))$
49	45 48	eqeltrd	$⊢ φ \to (x \in X, y \in Y ⟼ ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩) \in ((J \times_{t} K) Homeo (\prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times_{t} \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\})))$
50		hmeocn	$⊢ (x \in X, y \in Y ⟼ ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩) \in ((J \times_{t} K) Homeo (\prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times_{t} \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}))) \to (x \in X, y \in Y ⟼ ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩) \in ((J \times_{t} K) Cn (\prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times_{t} \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\})))$
51	49 50	syl	$⊢ φ \to (x \in X, y \in Y ⟼ ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩) \in ((J \times_{t} K) Cn (\prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times_{t} \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\})))$
52		cnf2	$⊢ (J \times_{t} K \in TopOn (X \times Y) \land \prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times_{t} \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}) \in TopOn (⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times ⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\})) \land (x \in X, y \in Y ⟼ ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩) \in ((J \times_{t} K) Cn (\prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times_{t} \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\})))) \to (x \in X, y \in Y ⟼ ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩) : X \times Y ⟶ ⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times ⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\})$
53	5 25 51 52	syl3anc	$⊢ φ \to (x \in X, y \in Y ⟼ ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩) : X \times Y ⟶ ⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times ⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\})$
54		eqid	$⊢ (x \in X, y \in Y ⟼ ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩) = (x \in X, y \in Y ⟼ ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩)$
55	54	fmpo	$⊢ \forall x \in X \forall y \in Y ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩ \in (⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times ⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\})) \leftrightarrow (x \in X, y \in Y ⟼ ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩) : X \times Y ⟶ ⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times ⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\})$
56	53 55	sylibr	$⊢ φ \to \forall x \in X \forall y \in Y ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩ \in (⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times ⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}))$
57	56	r19.21bi	$⊢ (φ \land x \in X) \to \forall y \in Y ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩ \in (⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times ⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}))$
58	57	r19.21bi	$⊢ ((φ \land x \in X) \land y \in Y) \to ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩ \in (⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times ⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}))$
59	58	anasss	$⊢ (φ \land (x \in X \land y \in Y)) \to ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩ \in (⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times ⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}))$
60		eqidd	$⊢ φ \to (x \in X, y \in Y ⟼ ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩) = (x \in X, y \in Y ⟼ ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩)$
61		vex	$⊢ x \in V$
62		vex	$⊢ y \in V$
63	61 62	op1std	$⊢ z = ⟨x, y⟩ \to 1^{st} (z) = x$
64	61 62	op2ndd	$⊢ z = ⟨x, y⟩ \to 2^{nd} (z) = y$
65	63 64	uneq12d	$⊢ z = ⟨x, y⟩ \to 1^{st} (z) \cup 2^{nd} (z) = x \cup y$
66	65	mpompt	$⊢ (z \in (⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times ⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\})) ⟼ 1^{st} (z) \cup 2^{nd} (z)) = (x \in ⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\}), y \in ⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}) ⟼ x \cup y)$
67	66	eqcomi	$⊢ (x \in ⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\}), y \in ⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}) ⟼ x \cup y) = (z \in (⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times ⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\})) ⟼ 1^{st} (z) \cup 2^{nd} (z))$
68	67	a1i	$⊢ φ \to (x \in ⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\}), y \in ⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}) ⟼ x \cup y) = (z \in (⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times ⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\})) ⟼ 1^{st} (z) \cup 2^{nd} (z))$
69	29 34	op1std	$⊢ z = ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩ \to 1^{st} (z) = \{⟨\emptyset, x⟩\}$
70	29 34	op2ndd	$⊢ z = ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩ \to 2^{nd} (z) = \{⟨1_{𝑜}, y⟩\}$
71	69 70	uneq12d	$⊢ z = ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩ \to 1^{st} (z) \cup 2^{nd} (z) = \{⟨\emptyset, x⟩\} \cup \{⟨1_{𝑜}, y⟩\}$
72		df-pr	$⊢ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\} = \{⟨\emptyset, x⟩\} \cup \{⟨1_{𝑜}, y⟩\}$
73	71 72	eqtr4di	$⊢ z = ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩ \to 1^{st} (z) \cup 2^{nd} (z) = \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}$
74	59 60 68 73	fmpoco	$⊢ φ \to (x \in ⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\}), y \in ⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}) ⟼ x \cup y) \circ (x \in X, y \in Y ⟼ ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩) = (x \in X, y \in Y ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})$
75	1 74	eqtr4id	$⊢ φ \to F = (x \in ⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\}), y \in ⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}) ⟼ x \cup y) \circ (x \in X, y \in Y ⟼ ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩)$
76		eqid	$⊢ ⋃ \prod_{𝑡} ({\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{\emptyset\}}) = ⋃ \prod_{𝑡} ({\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{\emptyset\}})$
77		eqid	$⊢ ⋃ \prod_{𝑡} ({\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{1_{𝑜}\}}) = ⋃ \prod_{𝑡} ({\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{1_{𝑜}\}})$
78		eqid	$⊢ \prod_{𝑡} (\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\}) = \prod_{𝑡} (\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\})$
79		eqid	$⊢ \prod_{𝑡} ({\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{\emptyset\}}) = \prod_{𝑡} ({\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{\emptyset\}})$
80		eqid	$⊢ \prod_{𝑡} ({\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{1_{𝑜}\}}) = \prod_{𝑡} ({\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{1_{𝑜}\}})$
81		eqid	$⊢ (x \in ⋃ \prod_{𝑡} ({\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{\emptyset\}}), y \in ⋃ \prod_{𝑡} ({\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{1_{𝑜}\}}) ⟼ x \cup y) = (x \in ⋃ \prod_{𝑡} ({\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{\emptyset\}}), y \in ⋃ \prod_{𝑡} ({\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{1_{𝑜}\}}) ⟼ x \cup y)$
82		2on	$⊢ 2_{𝑜} \in On$
83	82	a1i	$⊢ φ \to 2_{𝑜} \in On$
84		topontop	$⊢ J \in TopOn (X) \to J \in Top$
85	2 84	syl	$⊢ φ \to J \in Top$
86		topontop	$⊢ K \in TopOn (Y) \to K \in Top$
87	3 86	syl	$⊢ φ \to K \in Top$
88		xpscf	$⊢ \{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} : 2_{𝑜} ⟶ Top \leftrightarrow (J \in Top \land K \in Top)$
89	85 87 88	sylanbrc	$⊢ φ \to \{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} : 2_{𝑜} ⟶ Top$
90		df2o3	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$
91		df-pr	$⊢ \{\emptyset, 1_{𝑜}\} = \{\emptyset\} \cup \{1_{𝑜}\}$
92	90 91	eqtri	$⊢ 2_{𝑜} = \{\emptyset\} \cup \{1_{𝑜}\}$
93	92	a1i	$⊢ φ \to 2_{𝑜} = \{\emptyset\} \cup \{1_{𝑜}\}$
94		1n0	$⊢ 1_{𝑜} \neq \emptyset$
95	94	necomi	$⊢ \emptyset \neq 1_{𝑜}$
96		disjsn2	$⊢ \emptyset \neq 1_{𝑜} \to \{\emptyset\} \cap \{1_{𝑜}\} = \emptyset$
97	95 96	mp1i	$⊢ φ \to \{\emptyset\} \cap \{1_{𝑜}\} = \emptyset$
98	76 77 78 79 80 81 83 89 93 97	ptunhmeo	$⊢ φ \to (x \in ⋃ \prod_{𝑡} ({\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{\emptyset\}}), y \in ⋃ \prod_{𝑡} ({\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{1_{𝑜}\}}) ⟼ x \cup y) \in ((\prod_{𝑡} ({\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{\emptyset\}}) \times_{t} \prod_{𝑡} ({\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{1_{𝑜}\}})) Homeo \prod_{𝑡} (\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\}))$
99		fnpr2o	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to \{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} Fn 2_{𝑜}$
100	2 3 99	syl2anc	$⊢ φ \to \{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} Fn 2_{𝑜}$
101	7	prid1	$⊢ \emptyset \in \{\emptyset, 1_{𝑜}\}$
102	101 90	eleqtrri	$⊢ \emptyset \in 2_{𝑜}$
103		fnressn	$⊢ (\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} Fn 2_{𝑜} \land \emptyset \in 2_{𝑜}) \to {\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{\emptyset\}} = \{⟨\emptyset, \{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} (\emptyset)⟩\}$
104	100 102 103	sylancl	$⊢ φ \to {\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{\emptyset\}} = \{⟨\emptyset, \{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} (\emptyset)⟩\}$
105		fvpr0o	$⊢ J \in TopOn (X) \to \{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} (\emptyset) = J$
106	2 105	syl	$⊢ φ \to \{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} (\emptyset) = J$
107	106	opeq2d	$⊢ φ \to ⟨\emptyset, \{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} (\emptyset)⟩ = ⟨\emptyset, J⟩$
108	107	sneqd	$⊢ φ \to \{⟨\emptyset, \{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} (\emptyset)⟩\} = \{⟨\emptyset, J⟩\}$
109	104 108	eqtrd	$⊢ φ \to {\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{\emptyset\}} = \{⟨\emptyset, J⟩\}$
110	109	fveq2d	$⊢ φ \to \prod_{𝑡} ({\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{\emptyset\}}) = \prod_{𝑡} (\{⟨\emptyset, J⟩\})$
111	110	unieqd	$⊢ φ \to ⋃ \prod_{𝑡} ({\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{\emptyset\}}) = ⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\})$
112		1oelpr	$⊢ 1_{𝑜} \in \{\emptyset, 1_{𝑜}\}$
113	112 90	eleqtrri	$⊢ 1_{𝑜} \in 2_{𝑜}$
114		fnressn	$⊢ (\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} Fn 2_{𝑜} \land 1_{𝑜} \in 2_{𝑜}) \to {\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{1_{𝑜}\}} = \{⟨1_{𝑜}, \{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} (1_{𝑜})⟩\}$
115	100 113 114	sylancl	$⊢ φ \to {\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{1_{𝑜}\}} = \{⟨1_{𝑜}, \{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} (1_{𝑜})⟩\}$
116		fvpr1o	$⊢ K \in TopOn (Y) \to \{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} (1_{𝑜}) = K$
117	3 116	syl	$⊢ φ \to \{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} (1_{𝑜}) = K$
118	117	opeq2d	$⊢ φ \to ⟨1_{𝑜}, \{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} (1_{𝑜})⟩ = ⟨1_{𝑜}, K⟩$
119	118	sneqd	$⊢ φ \to \{⟨1_{𝑜}, \{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} (1_{𝑜})⟩\} = \{⟨1_{𝑜}, K⟩\}$
120	115 119	eqtrd	$⊢ φ \to {\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{1_{𝑜}\}} = \{⟨1_{𝑜}, K⟩\}$
121	120	fveq2d	$⊢ φ \to \prod_{𝑡} ({\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{1_{𝑜}\}}) = \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\})$
122	121	unieqd	$⊢ φ \to ⋃ \prod_{𝑡} ({\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{1_{𝑜}\}}) = ⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\})$
123		eqidd	$⊢ φ \to x \cup y = x \cup y$
124	111 122 123	mpoeq123dv	$⊢ φ \to (x \in ⋃ \prod_{𝑡} ({\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{\emptyset\}}), y \in ⋃ \prod_{𝑡} ({\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{1_{𝑜}\}}) ⟼ x \cup y) = (x \in ⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\}), y \in ⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}) ⟼ x \cup y)$
125	110 121	oveq12d	$⊢ φ \to \prod_{𝑡} ({\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{\emptyset\}}) \times_{t} \prod_{𝑡} ({\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{1_{𝑜}\}}) = \prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times_{t} \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\})$
126	125	oveq1d	$⊢ φ \to (\prod_{𝑡} ({\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{\emptyset\}}) \times_{t} \prod_{𝑡} ({\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\} ↾}_{\{1_{𝑜}\}})) Homeo \prod_{𝑡} (\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\}) = (\prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times_{t} \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\})) Homeo \prod_{𝑡} (\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\})$
127	98 124 126	3eltr3d	$⊢ φ \to (x \in ⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\}), y \in ⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}) ⟼ x \cup y) \in ((\prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times_{t} \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\})) Homeo \prod_{𝑡} (\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\}))$
128		hmeoco	$⊢ ((x \in X, y \in Y ⟼ ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩) \in ((J \times_{t} K) Homeo (\prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times_{t} \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}))) \land (x \in ⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\}), y \in ⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}) ⟼ x \cup y) \in ((\prod_{𝑡} (\{⟨\emptyset, J⟩\}) \times_{t} \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\})) Homeo \prod_{𝑡} (\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\}))) \to (x \in ⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\}), y \in ⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}) ⟼ x \cup y) \circ (x \in X, y \in Y ⟼ ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩) \in ((J \times_{t} K) Homeo \prod_{𝑡} (\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\}))$
129	49 127 128	syl2anc	$⊢ φ \to (x \in ⋃ \prod_{𝑡} (\{⟨\emptyset, J⟩\}), y \in ⋃ \prod_{𝑡} (\{⟨1_{𝑜}, K⟩\}) ⟼ x \cup y) \circ (x \in X, y \in Y ⟼ ⟨\{⟨\emptyset, x⟩\}, \{⟨1_{𝑜}, y⟩\}⟩) \in ((J \times_{t} K) Homeo \prod_{𝑡} (\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\}))$
130	75 129	eqeltrd	$⊢ φ \to F \in ((J \times_{t} K) Homeo \prod_{𝑡} (\{⟨\emptyset, J⟩, ⟨1_{𝑜}, K⟩\}))$

Metamath Proof Explorer

Theorem xpstopnlem1

Proof