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 , 𝐾 ⟩ } ) ) )