Theorem 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	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
	xpstopnlem1.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	xpstopnlem1.k	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
Assertion	xpstopnlem1	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐽 ×t 𝐾 ) Homeo ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ) ) )

Proof

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