Theorem xpstopnlem1 22136

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

Hypotheses

Ref	Expression
xpstopnlem1.f	⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))
xpstopnlem1.j	⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
xpstopnlem1.k	⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))

Assertion

Ref	Expression
xpstopnlem1	⊢ (𝜑 → 𝐹 ∈ ((𝐽 ×t 𝐾)Homeo(∏t‘◡({𝐽} +𝑐 {𝐾}))))

Distinct variable groups:   𝑥,𝑦,𝐽   𝑥,𝐾,𝑦   𝜑,𝑥,𝑦   𝑥,𝑋,𝑦   𝑥,𝑌,𝑦

Allowed substitution hints:   𝐹(𝑥,𝑦)

Proof of Theorem xpstopnlem1

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		xpstopnlem1.j	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
2		xpstopnlem1.k	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))
3		txtopon 21918	. . . . . . . . . 10 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
4	1, 2, 3	syl2anc 576	. . . . . . . . 9 ⊢ (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
5		eqid 2771	. . . . . . . . . . . . 13 ⊢ (∏t‘{⟨∅, 𝐽⟩}) = (∏t‘{⟨∅, 𝐽⟩})
6		0ex 5064	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ V
7	6	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∅ ∈ V)
8	5, 7, 1	pt1hmeo 22133	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑧 ∈ 𝑋 ↦ {⟨∅, 𝑧⟩}) ∈ (𝐽Homeo(∏t‘{⟨∅, 𝐽⟩})))
9		hmeocn 22087	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ 𝑋 ↦ {⟨∅, 𝑧⟩}) ∈ (𝐽Homeo(∏t‘{⟨∅, 𝐽⟩})) → (𝑧 ∈ 𝑋 ↦ {⟨∅, 𝑧⟩}) ∈ (𝐽 Cn (∏t‘{⟨∅, 𝐽⟩})))
10		cntop2 21568	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ 𝑋 ↦ {⟨∅, 𝑧⟩}) ∈ (𝐽 Cn (∏t‘{⟨∅, 𝐽⟩})) → (∏t‘{⟨∅, 𝐽⟩}) ∈ Top)
11	8, 9, 10	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (∏t‘{⟨∅, 𝐽⟩}) ∈ Top)
12		toptopon2 21245	. . . . . . . . . . 11 ⊢ ((∏t‘{⟨∅, 𝐽⟩}) ∈ Top ↔ (∏t‘{⟨∅, 𝐽⟩}) ∈ (TopOn‘∪ (∏t‘{⟨∅, 𝐽⟩})))
13	11, 12	sylib 210	. . . . . . . . . 10 ⊢ (𝜑 → (∏t‘{⟨∅, 𝐽⟩}) ∈ (TopOn‘∪ (∏t‘{⟨∅, 𝐽⟩})))
14		eqid 2771	. . . . . . . . . . . . 13 ⊢ (∏t‘{⟨1o, 𝐾⟩}) = (∏t‘{⟨1o, 𝐾⟩})
15		1on 7910	. . . . . . . . . . . . . 14 ⊢ 1o ∈ On
16	15	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1o ∈ On)
17	14, 16, 2	pt1hmeo 22133	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑧 ∈ 𝑌 ↦ {⟨1o, 𝑧⟩}) ∈ (𝐾Homeo(∏t‘{⟨1o, 𝐾⟩})))
18		hmeocn 22087	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ 𝑌 ↦ {⟨1o, 𝑧⟩}) ∈ (𝐾Homeo(∏t‘{⟨1o, 𝐾⟩})) → (𝑧 ∈ 𝑌 ↦ {⟨1o, 𝑧⟩}) ∈ (𝐾 Cn (∏t‘{⟨1o, 𝐾⟩})))
19		cntop2 21568	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ 𝑌 ↦ {⟨1o, 𝑧⟩}) ∈ (𝐾 Cn (∏t‘{⟨1o, 𝐾⟩})) → (∏t‘{⟨1o, 𝐾⟩}) ∈ Top)
20	17, 18, 19	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (∏t‘{⟨1o, 𝐾⟩}) ∈ Top)
21		toptopon2 21245	. . . . . . . . . . 11 ⊢ ((∏t‘{⟨1o, 𝐾⟩}) ∈ Top ↔ (∏t‘{⟨1o, 𝐾⟩}) ∈ (TopOn‘∪ (∏t‘{⟨1o, 𝐾⟩})))
22	20, 21	sylib 210	. . . . . . . . . 10 ⊢ (𝜑 → (∏t‘{⟨1o, 𝐾⟩}) ∈ (TopOn‘∪ (∏t‘{⟨1o, 𝐾⟩})))
23		txtopon 21918	. . . . . . . . . 10 ⊢ (((∏t‘{⟨∅, 𝐽⟩}) ∈ (TopOn‘∪ (∏t‘{⟨∅, 𝐽⟩})) ∧ (∏t‘{⟨1o, 𝐾⟩}) ∈ (TopOn‘∪ (∏t‘{⟨1o, 𝐾⟩}))) → ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩})) ∈ (TopOn‘(∪ (∏t‘{⟨∅, 𝐽⟩}) × ∪ (∏t‘{⟨1o, 𝐾⟩}))))
24	13, 22, 23	syl2anc 576	. . . . . . . . 9 ⊢ (𝜑 → ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩})) ∈ (TopOn‘(∪ (∏t‘{⟨∅, 𝐽⟩}) × ∪ (∏t‘{⟨1o, 𝐾⟩}))))
25		opeq2 4674	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑥 → ⟨∅, 𝑧⟩ = ⟨∅, 𝑥⟩)
26	25	sneqd 4447	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑥 → {⟨∅, 𝑧⟩} = {⟨∅, 𝑥⟩})
27		eqid 2771	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑋 ↦ {⟨∅, 𝑧⟩}) = (𝑧 ∈ 𝑋 ↦ {⟨∅, 𝑧⟩})
28		snex 5184	. . . . . . . . . . . . . . 15 ⊢ {⟨∅, 𝑥⟩} ∈ V
29	26, 27, 28	fvmpt 6593	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝑋 → ((𝑧 ∈ 𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥) = {⟨∅, 𝑥⟩})
30		opeq2 4674	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑦 → ⟨1o, 𝑧⟩ = ⟨1o, 𝑦⟩)
31	30	sneqd 4447	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → {⟨1o, 𝑧⟩} = {⟨1o, 𝑦⟩})
32		eqid 2771	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑌 ↦ {⟨1o, 𝑧⟩}) = (𝑧 ∈ 𝑌 ↦ {⟨1o, 𝑧⟩})
33		snex 5184	. . . . . . . . . . . . . . 15 ⊢ {⟨1o, 𝑦⟩} ∈ V
34	31, 32, 33	fvmpt 6593	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝑌 → ((𝑧 ∈ 𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦) = {⟨1o, 𝑦⟩})
35		opeq12 4675	. . . . . . . . . . . . . 14 ⊢ ((((𝑧 ∈ 𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥) = {⟨∅, 𝑥⟩} ∧ ((𝑧 ∈ 𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦) = {⟨1o, 𝑦⟩}) → ⟨((𝑧 ∈ 𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩ = ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩)
36	29, 34, 35	syl2an 587	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → ⟨((𝑧 ∈ 𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩ = ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩)
37	36	mpoeq3ia 7048	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨((𝑧 ∈ 𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩)
38		toponuni 21241	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
39	1, 38	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
40		toponuni 21241	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝐾)
41	2, 40	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 = ∪ 𝐾)
42		mpoeq12 7043	. . . . . . . . . . . . 13 ⊢ ((𝑋 = ∪ 𝐽 ∧ 𝑌 = ∪ 𝐾) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨((𝑧 ∈ 𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩) = (𝑥 ∈ ∪ 𝐽, 𝑦 ∈ ∪ 𝐾 ↦ ⟨((𝑧 ∈ 𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩))
43	39, 41, 42	syl2anc 576	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨((𝑧 ∈ 𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩) = (𝑥 ∈ ∪ 𝐽, 𝑦 ∈ ∪ 𝐾 ↦ ⟨((𝑧 ∈ 𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩))
44	37, 43	syl5eqr 2821	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) = (𝑥 ∈ ∪ 𝐽, 𝑦 ∈ ∪ 𝐾 ↦ ⟨((𝑧 ∈ 𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩))
45		eqid 2771	. . . . . . . . . . . 12 ⊢ ∪ 𝐽 = ∪ 𝐽
46		eqid 2771	. . . . . . . . . . . 12 ⊢ ∪ 𝐾 = ∪ 𝐾
47	45, 46, 8, 17	txhmeo 22130	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ∪ 𝐽, 𝑦 ∈ ∪ 𝐾 ↦ ⟨((𝑧 ∈ 𝑋 ↦ {⟨∅, 𝑧⟩})‘𝑥), ((𝑧 ∈ 𝑌 ↦ {⟨1o, 𝑧⟩})‘𝑦)⟩) ∈ ((𝐽 ×t 𝐾)Homeo((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))))
48	44, 47	eqeltrd 2859	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) ∈ ((𝐽 ×t 𝐾)Homeo((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))))
49		hmeocn 22087	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) ∈ ((𝐽 ×t 𝐾)Homeo((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) ∈ ((𝐽 ×t 𝐾) Cn ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))))
50	48, 49	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) ∈ ((𝐽 ×t 𝐾) Cn ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))))
51		cnf2 21576	. . . . . . . . 9 ⊢ (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩})) ∈ (TopOn‘(∪ (∏t‘{⟨∅, 𝐽⟩}) × ∪ (∏t‘{⟨1o, 𝐾⟩}))) ∧ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) ∈ ((𝐽 ×t 𝐾) Cn ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩})))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩):(𝑋 × 𝑌)⟶(∪ (∏t‘{⟨∅, 𝐽⟩}) × ∪ (∏t‘{⟨1o, 𝐾⟩})))
52	4, 24, 50, 51	syl3anc 1352	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩):(𝑋 × 𝑌)⟶(∪ (∏t‘{⟨∅, 𝐽⟩}) × ∪ (∏t‘{⟨1o, 𝐾⟩})))
53		eqid 2771	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩)
54	53	fmpo 7572	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ ∈ (∪ (∏t‘{⟨∅, 𝐽⟩}) × ∪ (∏t‘{⟨1o, 𝐾⟩})) ↔ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩):(𝑋 × 𝑌)⟶(∪ (∏t‘{⟨∅, 𝐽⟩}) × ∪ (∏t‘{⟨1o, 𝐾⟩})))
55	52, 54	sylibr 226	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ ∈ (∪ (∏t‘{⟨∅, 𝐽⟩}) × ∪ (∏t‘{⟨1o, 𝐾⟩})))
56	55	r19.21bi 3151	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ ∈ (∪ (∏t‘{⟨∅, 𝐽⟩}) × ∪ (∏t‘{⟨1o, 𝐾⟩})))
57	56	r19.21bi 3151	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ ∈ (∪ (∏t‘{⟨∅, 𝐽⟩}) × ∪ (∏t‘{⟨1o, 𝐾⟩})))
58	57	anasss 459	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ ∈ (∪ (∏t‘{⟨∅, 𝐽⟩}) × ∪ (∏t‘{⟨1o, 𝐾⟩})))
59		eqidd 2772	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩))
60		vex 3411	. . . . . . . . 9 ⊢ 𝑥 ∈ V
61		vex 3411	. . . . . . . . 9 ⊢ 𝑦 ∈ V
62	60, 61	op1std 7509	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (1st ‘𝑧) = 𝑥)
63	60, 61	op2ndd 7510	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd ‘𝑧) = 𝑦)
64	62, 63	uneq12d 4022	. . . . . . 7 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) = (𝑥 ∪ 𝑦))
65	64	mpompt 7080	. . . . . 6 ⊢ (𝑧 ∈ (∪ (∏t‘{⟨∅, 𝐽⟩}) × ∪ (∏t‘{⟨1o, 𝐾⟩})) ↦ ((1st ‘𝑧) ∪ (2nd ‘𝑧))) = (𝑥 ∈ ∪ (∏t‘{⟨∅, 𝐽⟩}), 𝑦 ∈ ∪ (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥 ∪ 𝑦))
66	65	eqcomi 2780	. . . . 5 ⊢ (𝑥 ∈ ∪ (∏t‘{⟨∅, 𝐽⟩}), 𝑦 ∈ ∪ (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥 ∪ 𝑦)) = (𝑧 ∈ (∪ (∏t‘{⟨∅, 𝐽⟩}) × ∪ (∏t‘{⟨1o, 𝐾⟩})) ↦ ((1st ‘𝑧) ∪ (2nd ‘𝑧)))
67	66	a1i 11	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ∪ (∏t‘{⟨∅, 𝐽⟩}), 𝑦 ∈ ∪ (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥 ∪ 𝑦)) = (𝑧 ∈ (∪ (∏t‘{⟨∅, 𝐽⟩}) × ∪ (∏t‘{⟨1o, 𝐾⟩})) ↦ ((1st ‘𝑧) ∪ (2nd ‘𝑧))))
68	28, 33	op1std 7509	. . . . . 6 ⊢ (𝑧 = ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ → (1st ‘𝑧) = {⟨∅, 𝑥⟩})
69	28, 33	op2ndd 7510	. . . . . 6 ⊢ (𝑧 = ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ → (2nd ‘𝑧) = {⟨1o, 𝑦⟩})
70	68, 69	uneq12d 4022	. . . . 5 ⊢ (𝑧 = ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ({⟨∅, 𝑥⟩} ∪ {⟨1o, 𝑦⟩}))
71		xpscg 16685	. . . . . . 7 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → ◡({𝑥} +𝑐 {𝑦}) = {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
72	71	el2v 3415	. . . . . 6 ⊢ ◡({𝑥} +𝑐 {𝑦}) = {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}
73		df-pr 4438	. . . . . 6 ⊢ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩} = ({⟨∅, 𝑥⟩} ∪ {⟨1o, 𝑦⟩})
74	72, 73	eqtri 2795	. . . . 5 ⊢ ◡({𝑥} +𝑐 {𝑦}) = ({⟨∅, 𝑥⟩} ∪ {⟨1o, 𝑦⟩})
75	70, 74	syl6eqr 2825	. . . 4 ⊢ (𝑧 = ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩ → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ◡({𝑥} +𝑐 {𝑦}))
76	58, 59, 67, 75	fmpoco 7596	. . 3 ⊢ (𝜑 → ((𝑥 ∈ ∪ (∏t‘{⟨∅, 𝐽⟩}), 𝑦 ∈ ∪ (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥 ∪ 𝑦)) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))
77		xpstopnlem1.f	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))
78	76, 77	syl6reqr 2826	. 2 ⊢ (𝜑 → 𝐹 = ((𝑥 ∈ ∪ (∏t‘{⟨∅, 𝐽⟩}), 𝑦 ∈ ∪ (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥 ∪ 𝑦)) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩)))
79		eqid 2771	. . . . 5 ⊢ ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})) = ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅}))
80		eqid 2771	. . . . 5 ⊢ ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1o})) = ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1o}))
81		eqid 2771	. . . . 5 ⊢ (∏t‘◡({𝐽} +𝑐 {𝐾})) = (∏t‘◡({𝐽} +𝑐 {𝐾}))
82		eqid 2771	. . . . 5 ⊢ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})) = (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅}))
83		eqid 2771	. . . . 5 ⊢ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1o})) = (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1o}))
84		eqid 2771	. . . . 5 ⊢ (𝑥 ∈ ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})), 𝑦 ∈ ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1o})) ↦ (𝑥 ∪ 𝑦)) = (𝑥 ∈ ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})), 𝑦 ∈ ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1o})) ↦ (𝑥 ∪ 𝑦))
85		2on 7912	. . . . . 6 ⊢ 2o ∈ On
86	85	a1i 11	. . . . 5 ⊢ (𝜑 → 2o ∈ On)
87		topontop 21240	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
88	1, 87	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐽 ∈ Top)
89		topontop 21240	. . . . . . 7 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top)
90	2, 89	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ Top)
91		xpscfcda 16699	. . . . . 6 ⊢ (◡({𝐽} +𝑐 {𝐾}):2o⟶Top ↔ (𝐽 ∈ Top ∧ 𝐾 ∈ Top))
92	88, 90, 91	sylanbrc 575	. . . . 5 ⊢ (𝜑 → ◡({𝐽} +𝑐 {𝐾}):2o⟶Top)
93		df2o3 7917	. . . . . . 7 ⊢ 2o = {∅, 1o}
94		df-pr 4438	. . . . . . 7 ⊢ {∅, 1o} = ({∅} ∪ {1o})
95	93, 94	eqtri 2795	. . . . . 6 ⊢ 2o = ({∅} ∪ {1o})
96	95	a1i 11	. . . . 5 ⊢ (𝜑 → 2o = ({∅} ∪ {1o}))
97		1n0 7919	. . . . . . 7 ⊢ 1o ≠ ∅
98	97	necomi 3014	. . . . . 6 ⊢ ∅ ≠ 1o
99		disjsn2 4518	. . . . . 6 ⊢ (∅ ≠ 1o → ({∅} ∩ {1o}) = ∅)
100	98, 99	mp1i 13	. . . . 5 ⊢ (𝜑 → ({∅} ∩ {1o}) = ∅)
101	79, 80, 81, 82, 83, 84, 86, 92, 96, 100	ptunhmeo 22135	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})), 𝑦 ∈ ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1o})) ↦ (𝑥 ∪ 𝑦)) ∈ (((∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})) ×t (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1o})))Homeo(∏t‘◡({𝐽} +𝑐 {𝐾}))))
102		xpscfn 16686	. . . . . . . . . 10 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → ◡({𝐽} +𝑐 {𝐾}) Fn 2o)
103	1, 2, 102	syl2anc 576	. . . . . . . . 9 ⊢ (𝜑 → ◡({𝐽} +𝑐 {𝐾}) Fn 2o)
104	6	prid1 4568	. . . . . . . . . 10 ⊢ ∅ ∈ {∅, 1o}
105	104, 93	eleqtrri 2858	. . . . . . . . 9 ⊢ ∅ ∈ 2o
106		fnressn 6741	. . . . . . . . 9 ⊢ ((◡({𝐽} +𝑐 {𝐾}) Fn 2o ∧ ∅ ∈ 2o) → (◡({𝐽} +𝑐 {𝐾}) ↾ {∅}) = {⟨∅, (◡({𝐽} +𝑐 {𝐾})‘∅)⟩})
107	103, 105, 106	sylancl 578	. . . . . . . 8 ⊢ (𝜑 → (◡({𝐽} +𝑐 {𝐾}) ↾ {∅}) = {⟨∅, (◡({𝐽} +𝑐 {𝐾})‘∅)⟩})
108		xpsc0 16689	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (◡({𝐽} +𝑐 {𝐾})‘∅) = 𝐽)
109	1, 108	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (◡({𝐽} +𝑐 {𝐾})‘∅) = 𝐽)
110	109	opeq2d 4680	. . . . . . . . 9 ⊢ (𝜑 → ⟨∅, (◡({𝐽} +𝑐 {𝐾})‘∅)⟩ = ⟨∅, 𝐽⟩)
111	110	sneqd 4447	. . . . . . . 8 ⊢ (𝜑 → {⟨∅, (◡({𝐽} +𝑐 {𝐾})‘∅)⟩} = {⟨∅, 𝐽⟩})
112	107, 111	eqtrd 2807	. . . . . . 7 ⊢ (𝜑 → (◡({𝐽} +𝑐 {𝐾}) ↾ {∅}) = {⟨∅, 𝐽⟩})
113	112	fveq2d 6500	. . . . . 6 ⊢ (𝜑 → (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})) = (∏t‘{⟨∅, 𝐽⟩}))
114	113	unieqd 4718	. . . . 5 ⊢ (𝜑 → ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})) = ∪ (∏t‘{⟨∅, 𝐽⟩}))
115		1oex 7911	. . . . . . . . . . 11 ⊢ 1o ∈ V
116	115	prid2 4569	. . . . . . . . . 10 ⊢ 1o ∈ {∅, 1o}
117	116, 93	eleqtrri 2858	. . . . . . . . 9 ⊢ 1o ∈ 2o
118		fnressn 6741	. . . . . . . . 9 ⊢ ((◡({𝐽} +𝑐 {𝐾}) Fn 2o ∧ 1o ∈ 2o) → (◡({𝐽} +𝑐 {𝐾}) ↾ {1o}) = {⟨1o, (◡({𝐽} +𝑐 {𝐾})‘1o)⟩})
119	103, 117, 118	sylancl 578	. . . . . . . 8 ⊢ (𝜑 → (◡({𝐽} +𝑐 {𝐾}) ↾ {1o}) = {⟨1o, (◡({𝐽} +𝑐 {𝐾})‘1o)⟩})
120		xpsc1 16690	. . . . . . . . . . 11 ⊢ (𝐾 ∈ (TopOn‘𝑌) → (◡({𝐽} +𝑐 {𝐾})‘1o) = 𝐾)
121	2, 120	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (◡({𝐽} +𝑐 {𝐾})‘1o) = 𝐾)
122	121	opeq2d 4680	. . . . . . . . 9 ⊢ (𝜑 → ⟨1o, (◡({𝐽} +𝑐 {𝐾})‘1o)⟩ = ⟨1o, 𝐾⟩)
123	122	sneqd 4447	. . . . . . . 8 ⊢ (𝜑 → {⟨1o, (◡({𝐽} +𝑐 {𝐾})‘1o)⟩} = {⟨1o, 𝐾⟩})
124	119, 123	eqtrd 2807	. . . . . . 7 ⊢ (𝜑 → (◡({𝐽} +𝑐 {𝐾}) ↾ {1o}) = {⟨1o, 𝐾⟩})
125	124	fveq2d 6500	. . . . . 6 ⊢ (𝜑 → (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1o})) = (∏t‘{⟨1o, 𝐾⟩}))
126	125	unieqd 4718	. . . . 5 ⊢ (𝜑 → ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1o})) = ∪ (∏t‘{⟨1o, 𝐾⟩}))
127		eqidd 2772	. . . . 5 ⊢ (𝜑 → (𝑥 ∪ 𝑦) = (𝑥 ∪ 𝑦))
128	114, 126, 127	mpoeq123dv 7045	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})), 𝑦 ∈ ∪ (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1o})) ↦ (𝑥 ∪ 𝑦)) = (𝑥 ∈ ∪ (∏t‘{⟨∅, 𝐽⟩}), 𝑦 ∈ ∪ (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥 ∪ 𝑦)))
129	113, 125	oveq12d 6992	. . . . 5 ⊢ (𝜑 → ((∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})) ×t (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1o}))) = ((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩})))
130	129	oveq1d 6989	. . . 4 ⊢ (𝜑 → (((∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {∅})) ×t (∏t‘(◡({𝐽} +𝑐 {𝐾}) ↾ {1o})))Homeo(∏t‘◡({𝐽} +𝑐 {𝐾}))) = (((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))Homeo(∏t‘◡({𝐽} +𝑐 {𝐾}))))
131	101, 128, 130	3eltr3d 2873	. . 3 ⊢ (𝜑 → (𝑥 ∈ ∪ (∏t‘{⟨∅, 𝐽⟩}), 𝑦 ∈ ∪ (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥 ∪ 𝑦)) ∈ (((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))Homeo(∏t‘◡({𝐽} +𝑐 {𝐾}))))
132		hmeoco 22099	. . 3 ⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩) ∈ ((𝐽 ×t 𝐾)Homeo((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))) ∧ (𝑥 ∈ ∪ (∏t‘{⟨∅, 𝐽⟩}), 𝑦 ∈ ∪ (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥 ∪ 𝑦)) ∈ (((∏t‘{⟨∅, 𝐽⟩}) ×t (∏t‘{⟨1o, 𝐾⟩}))Homeo(∏t‘◡({𝐽} +𝑐 {𝐾})))) → ((𝑥 ∈ ∪ (∏t‘{⟨∅, 𝐽⟩}), 𝑦 ∈ ∪ (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥 ∪ 𝑦)) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩)) ∈ ((𝐽 ×t 𝐾)Homeo(∏t‘◡({𝐽} +𝑐 {𝐾}))))
133	48, 131, 132	syl2anc 576	. 2 ⊢ (𝜑 → ((𝑥 ∈ ∪ (∏t‘{⟨∅, 𝐽⟩}), 𝑦 ∈ ∪ (∏t‘{⟨1o, 𝐾⟩}) ↦ (𝑥 ∪ 𝑦)) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨{⟨∅, 𝑥⟩}, {⟨1o, 𝑦⟩}⟩)) ∈ ((𝐽 ×t 𝐾)Homeo(∏t‘◡({𝐽} +𝑐 {𝐾}))))
134	78, 133	eqeltrd 2859	1 ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ×t 𝐾)Homeo(∏t‘◡({𝐽} +𝑐 {𝐾}))))

Syntax hints:   → wi 4   ∧ wa 387   = wceq 1508   ∈ wcel 2051   ≠ wne 2960  ∀wral 3081  Vcvv 3408   ∪ cun 3820   ∩ cin 3821  ∅c0 4172  {csn 4435  {cpr 4437  ⟨cop 4441  ∪ cuni 4708   ↦ cmpt 5004   × cxp 5401  ^◡ccnv 5402   ↾ cres 5405   ∘ ccom 5407  Oncon0 6026   Fn wfn 6180  ⟶wf 6181  ‘cfv 6185  (class class class)co 6974   ∈ cmpo 6976  1^st c1st 7497  2^nd c2nd 7498  1_oc1o 7896  2_oc2o 7897   +_𝑐 ccda 9385  ∏_tcpt 16566  Topctop 21220  TopOnctopon 21237   Cn ccn 21551   ×_t ctx 21887  Homeochmeo 22080

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2743  ax-rep 5045  ax-sep 5056  ax-nul 5063  ax-pow 5115  ax-pr 5182  ax-un 7277

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-ne 2961  df-ral 3086  df-rex 3087  df-reu 3088  df-rab 3090  df-v 3410  df-sbc 3675  df-csb 3780  df-dif 3825  df-un 3827  df-in 3829  df-ss 3836  df-pss 3838  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4709  df-int 4746  df-iun 4790  df-iin 4791  df-br 4926  df-opab 4988  df-mpt 5005  df-tr 5027  df-id 5308  df-eprel 5313  df-po 5322  df-so 5323  df-fr 5362  df-we 5364  df-xp 5409  df-rel 5410  df-cnv 5411  df-co 5412  df-dm 5413  df-rn 5414  df-res 5415  df-ima 5416  df-pred 5983  df-ord 6029  df-on 6030  df-lim 6031  df-suc 6032  df-iota 6149  df-fun 6187  df-fn 6188  df-f 6189  df-f1 6190  df-fo 6191  df-f1o 6192  df-fv 6193  df-ov 6977  df-oprab 6978  df-mpo 6979  df-om 7395  df-1st 7499  df-2nd 7500  df-wrecs 7748  df-recs 7810  df-rdg 7848  df-1o 7903  df-2o 7904  df-oadd 7907  df-er 8087  df-map 8206  df-ixp 8258  df-en 8305  df-dom 8306  df-sdom 8307  df-fin 8308  df-fi 8668  df-cda 9386  df-topgen 16571  df-pt 16572  df-top 21221  df-topon 21238  df-bases 21273  df-cn 21554  df-cnp 21555  df-tx 21889  df-hmeo 22082

This theorem is referenced by:  xpstopnlem2  22138