This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 1oex ⊢ 1o ∈ V
113 112 prid2 ⊢ 1o ∈ { ∅ , 1o }
114 113 90 eleqtrri ⊢ 1o ∈ 2o
115 fnressn ⊢ ( ( { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } Fn 2o ∧ 1o ∈ 2o ) → ( { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ↾ { 1o } ) = { ⟨ 1o , ( { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ‘ 1o ) ⟩ } )
116 100 114 115 sylancl ⊢ ( 𝜑 → ( { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ↾ { 1o } ) = { ⟨ 1o , ( { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ‘ 1o ) ⟩ } )
117 fvpr1o ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → ( { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ‘ 1o ) = 𝐾 )
118 3 117 syl ⊢ ( 𝜑 → ( { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ‘ 1o ) = 𝐾 )
119 118 opeq2d ⊢ ( 𝜑 → ⟨ 1o , ( { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ‘ 1o ) ⟩ = ⟨ 1o , 𝐾 ⟩ )
120 119 sneqd ⊢ ( 𝜑 → { ⟨ 1o , ( { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ‘ 1o ) ⟩ } = { ⟨ 1o , 𝐾 ⟩ } )
121 116 120 eqtrd ⊢ ( 𝜑 → ( { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ↾ { 1o } ) = { ⟨ 1o , 𝐾 ⟩ } )
122 121 fveq2d ⊢ ( 𝜑 → ( ∏t ‘ ( { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ↾ { 1o } ) ) = ( ∏t ‘ { ⟨ 1o , 𝐾 ⟩ } ) )
123 122 unieqd ⊢ ( 𝜑 → ∪ ( ∏t ‘ ( { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ↾ { 1o } ) ) = ∪ ( ∏t ‘ { ⟨ 1o , 𝐾 ⟩ } ) )
124 eqidd ⊢ ( 𝜑 → ( 𝑥 ∪ 𝑦 ) = ( 𝑥 ∪ 𝑦 ) )
125 111 123 124 mpoeq123dv ⊢ ( 𝜑 → ( 𝑥 ∈ ∪ ( ∏t ‘ ( { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ↾ { ∅ } ) ) , 𝑦 ∈ ∪ ( ∏t ‘ ( { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ↾ { 1o } ) ) ↦ ( 𝑥 ∪ 𝑦 ) ) = ( 𝑥 ∈ ∪ ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ } ) , 𝑦 ∈ ∪ ( ∏t ‘ { ⟨ 1o , 𝐾 ⟩ } ) ↦ ( 𝑥 ∪ 𝑦 ) ) )
126 110 122 oveq12d ⊢ ( 𝜑 → ( ( ∏t ‘ ( { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ↾ { ∅ } ) ) ×t ( ∏t ‘ ( { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ↾ { 1o } ) ) ) = ( ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ } ) ×t ( ∏t ‘ { ⟨ 1o , 𝐾 ⟩ } ) ) )
127 126 oveq1d ⊢ ( 𝜑 → ( ( ( ∏t ‘ ( { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ↾ { ∅ } ) ) ×t ( ∏t ‘ ( { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ↾ { 1o } ) ) ) Homeo ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ) ) = ( ( ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ } ) ×t ( ∏t ‘ { ⟨ 1o , 𝐾 ⟩ } ) ) Homeo ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ) ) )
128 98 125 127 3eltr3d ⊢ ( 𝜑 → ( 𝑥 ∈ ∪ ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ } ) , 𝑦 ∈ ∪ ( ∏t ‘ { ⟨ 1o , 𝐾 ⟩ } ) ↦ ( 𝑥 ∪ 𝑦 ) ) ∈ ( ( ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ } ) ×t ( ∏t ‘ { ⟨ 1o , 𝐾 ⟩ } ) ) Homeo ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ) ) )
129 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 , 𝐾 ⟩ } ) ) )
130 49 128 129 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ ∪ ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ } ) , 𝑦 ∈ ∪ ( ∏t ‘ { ⟨ 1o , 𝐾 ⟩ } ) ↦ ( 𝑥 ∪ 𝑦 ) ) ∘ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ { ⟨ ∅ , 𝑥 ⟩ } , { ⟨ 1o , 𝑦 ⟩ } ⟩ ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Homeo ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ) ) )
131 75 130 eqeltrd ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐽 ×t 𝐾 ) Homeo ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ) ) )