Metamath Proof Explorer


Theorem ptunhmeo

Description: Define a homeomorphism from a binary product of indexed product topologies to an indexed product topology on the union of the index sets. This is the topological analogue of ( A ^ B ) x. ( A ^ C ) = A ^ ( B + C ) . (Contributed by Mario Carneiro, 8-Feb-2015) (Proof shortened by Mario Carneiro, 23-Aug-2015)

Ref Expression
Hypotheses ptunhmeo.x 𝑋 = 𝐾
ptunhmeo.y 𝑌 = 𝐿
ptunhmeo.j 𝐽 = ( ∏t𝐹 )
ptunhmeo.k 𝐾 = ( ∏t ‘ ( 𝐹𝐴 ) )
ptunhmeo.l 𝐿 = ( ∏t ‘ ( 𝐹𝐵 ) )
ptunhmeo.g 𝐺 = ( 𝑥𝑋 , 𝑦𝑌 ↦ ( 𝑥𝑦 ) )
ptunhmeo.c ( 𝜑𝐶𝑉 )
ptunhmeo.f ( 𝜑𝐹 : 𝐶 ⟶ Top )
ptunhmeo.u ( 𝜑𝐶 = ( 𝐴𝐵 ) )
ptunhmeo.i ( 𝜑 → ( 𝐴𝐵 ) = ∅ )
Assertion ptunhmeo ( 𝜑𝐺 ∈ ( ( 𝐾 ×t 𝐿 ) Homeo 𝐽 ) )

Proof

Step Hyp Ref Expression
1 ptunhmeo.x 𝑋 = 𝐾
2 ptunhmeo.y 𝑌 = 𝐿
3 ptunhmeo.j 𝐽 = ( ∏t𝐹 )
4 ptunhmeo.k 𝐾 = ( ∏t ‘ ( 𝐹𝐴 ) )
5 ptunhmeo.l 𝐿 = ( ∏t ‘ ( 𝐹𝐵 ) )
6 ptunhmeo.g 𝐺 = ( 𝑥𝑋 , 𝑦𝑌 ↦ ( 𝑥𝑦 ) )
7 ptunhmeo.c ( 𝜑𝐶𝑉 )
8 ptunhmeo.f ( 𝜑𝐹 : 𝐶 ⟶ Top )
9 ptunhmeo.u ( 𝜑𝐶 = ( 𝐴𝐵 ) )
10 ptunhmeo.i ( 𝜑 → ( 𝐴𝐵 ) = ∅ )
11 vex 𝑥 ∈ V
12 vex 𝑦 ∈ V
13 11 12 op1std ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1st𝑧 ) = 𝑥 )
14 11 12 op2ndd ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2nd𝑧 ) = 𝑦 )
15 13 14 uneq12d ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) = ( 𝑥𝑦 ) )
16 15 mpompt ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) ) = ( 𝑥𝑋 , 𝑦𝑌 ↦ ( 𝑥𝑦 ) )
17 6 16 eqtr4i 𝐺 = ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) )
18 xp1st ( 𝑧 ∈ ( 𝑋 × 𝑌 ) → ( 1st𝑧 ) ∈ 𝑋 )
19 18 adantl ( ( 𝜑𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( 1st𝑧 ) ∈ 𝑋 )
20 ixpeq2 ( ∀ 𝑛𝐴 ( ( 𝐹𝐴 ) ‘ 𝑛 ) = ( 𝐹𝑛 ) → X 𝑛𝐴 ( ( 𝐹𝐴 ) ‘ 𝑛 ) = X 𝑛𝐴 ( 𝐹𝑛 ) )
21 fvres ( 𝑛𝐴 → ( ( 𝐹𝐴 ) ‘ 𝑛 ) = ( 𝐹𝑛 ) )
22 21 unieqd ( 𝑛𝐴 ( ( 𝐹𝐴 ) ‘ 𝑛 ) = ( 𝐹𝑛 ) )
23 20 22 mprg X 𝑛𝐴 ( ( 𝐹𝐴 ) ‘ 𝑛 ) = X 𝑛𝐴 ( 𝐹𝑛 )
24 ssun1 𝐴 ⊆ ( 𝐴𝐵 )
25 24 9 sseqtrrid ( 𝜑𝐴𝐶 )
26 7 25 ssexd ( 𝜑𝐴 ∈ V )
27 8 25 fssresd ( 𝜑 → ( 𝐹𝐴 ) : 𝐴 ⟶ Top )
28 4 ptuni ( ( 𝐴 ∈ V ∧ ( 𝐹𝐴 ) : 𝐴 ⟶ Top ) → X 𝑛𝐴 ( ( 𝐹𝐴 ) ‘ 𝑛 ) = 𝐾 )
29 26 27 28 syl2anc ( 𝜑X 𝑛𝐴 ( ( 𝐹𝐴 ) ‘ 𝑛 ) = 𝐾 )
30 23 29 eqtr3id ( 𝜑X 𝑛𝐴 ( 𝐹𝑛 ) = 𝐾 )
31 30 1 eqtr4di ( 𝜑X 𝑛𝐴 ( 𝐹𝑛 ) = 𝑋 )
32 31 adantr ( ( 𝜑𝑧 ∈ ( 𝑋 × 𝑌 ) ) → X 𝑛𝐴 ( 𝐹𝑛 ) = 𝑋 )
33 19 32 eleqtrrd ( ( 𝜑𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( 1st𝑧 ) ∈ X 𝑛𝐴 ( 𝐹𝑛 ) )
34 xp2nd ( 𝑧 ∈ ( 𝑋 × 𝑌 ) → ( 2nd𝑧 ) ∈ 𝑌 )
35 34 adantl ( ( 𝜑𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( 2nd𝑧 ) ∈ 𝑌 )
36 9 eqcomd ( 𝜑 → ( 𝐴𝐵 ) = 𝐶 )
37 uneqdifeq ( ( 𝐴𝐶 ∧ ( 𝐴𝐵 ) = ∅ ) → ( ( 𝐴𝐵 ) = 𝐶 ↔ ( 𝐶𝐴 ) = 𝐵 ) )
38 25 10 37 syl2anc ( 𝜑 → ( ( 𝐴𝐵 ) = 𝐶 ↔ ( 𝐶𝐴 ) = 𝐵 ) )
39 36 38 mpbid ( 𝜑 → ( 𝐶𝐴 ) = 𝐵 )
40 39 ixpeq1d ( 𝜑X 𝑛 ∈ ( 𝐶𝐴 ) ( 𝐹𝑛 ) = X 𝑛𝐵 ( 𝐹𝑛 ) )
41 ixpeq2 ( ∀ 𝑛𝐵 ( ( 𝐹𝐵 ) ‘ 𝑛 ) = ( 𝐹𝑛 ) → X 𝑛𝐵 ( ( 𝐹𝐵 ) ‘ 𝑛 ) = X 𝑛𝐵 ( 𝐹𝑛 ) )
42 fvres ( 𝑛𝐵 → ( ( 𝐹𝐵 ) ‘ 𝑛 ) = ( 𝐹𝑛 ) )
43 42 unieqd ( 𝑛𝐵 ( ( 𝐹𝐵 ) ‘ 𝑛 ) = ( 𝐹𝑛 ) )
44 41 43 mprg X 𝑛𝐵 ( ( 𝐹𝐵 ) ‘ 𝑛 ) = X 𝑛𝐵 ( 𝐹𝑛 )
45 ssun2 𝐵 ⊆ ( 𝐴𝐵 )
46 45 9 sseqtrrid ( 𝜑𝐵𝐶 )
47 7 46 ssexd ( 𝜑𝐵 ∈ V )
48 8 46 fssresd ( 𝜑 → ( 𝐹𝐵 ) : 𝐵 ⟶ Top )
49 5 ptuni ( ( 𝐵 ∈ V ∧ ( 𝐹𝐵 ) : 𝐵 ⟶ Top ) → X 𝑛𝐵 ( ( 𝐹𝐵 ) ‘ 𝑛 ) = 𝐿 )
50 47 48 49 syl2anc ( 𝜑X 𝑛𝐵 ( ( 𝐹𝐵 ) ‘ 𝑛 ) = 𝐿 )
51 44 50 eqtr3id ( 𝜑X 𝑛𝐵 ( 𝐹𝑛 ) = 𝐿 )
52 51 2 eqtr4di ( 𝜑X 𝑛𝐵 ( 𝐹𝑛 ) = 𝑌 )
53 40 52 eqtrd ( 𝜑X 𝑛 ∈ ( 𝐶𝐴 ) ( 𝐹𝑛 ) = 𝑌 )
54 53 adantr ( ( 𝜑𝑧 ∈ ( 𝑋 × 𝑌 ) ) → X 𝑛 ∈ ( 𝐶𝐴 ) ( 𝐹𝑛 ) = 𝑌 )
55 35 54 eleqtrrd ( ( 𝜑𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( 2nd𝑧 ) ∈ X 𝑛 ∈ ( 𝐶𝐴 ) ( 𝐹𝑛 ) )
56 25 adantr ( ( 𝜑𝑧 ∈ ( 𝑋 × 𝑌 ) ) → 𝐴𝐶 )
57 undifixp ( ( ( 1st𝑧 ) ∈ X 𝑛𝐴 ( 𝐹𝑛 ) ∧ ( 2nd𝑧 ) ∈ X 𝑛 ∈ ( 𝐶𝐴 ) ( 𝐹𝑛 ) ∧ 𝐴𝐶 ) → ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) ∈ X 𝑛𝐶 ( 𝐹𝑛 ) )
58 33 55 56 57 syl3anc ( ( 𝜑𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) ∈ X 𝑛𝐶 ( 𝐹𝑛 ) )
59 ixpfn ( ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) ∈ X 𝑛𝐶 ( 𝐹𝑛 ) → ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) Fn 𝐶 )
60 58 59 syl ( ( 𝜑𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) Fn 𝐶 )
61 dffn5 ( ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) Fn 𝐶 ↔ ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) = ( 𝑘𝐶 ↦ ( ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) ‘ 𝑘 ) ) )
62 60 61 sylib ( ( 𝜑𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) = ( 𝑘𝐶 ↦ ( ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) ‘ 𝑘 ) ) )
63 62 mpteq2dva ( 𝜑 → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) ) = ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 𝑘𝐶 ↦ ( ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) ‘ 𝑘 ) ) ) )
64 17 63 syl5eq ( 𝜑𝐺 = ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 𝑘𝐶 ↦ ( ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) ‘ 𝑘 ) ) ) )
65 pttop ( ( 𝐴 ∈ V ∧ ( 𝐹𝐴 ) : 𝐴 ⟶ Top ) → ( ∏t ‘ ( 𝐹𝐴 ) ) ∈ Top )
66 26 27 65 syl2anc ( 𝜑 → ( ∏t ‘ ( 𝐹𝐴 ) ) ∈ Top )
67 4 66 eqeltrid ( 𝜑𝐾 ∈ Top )
68 1 toptopon ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
69 67 68 sylib ( 𝜑𝐾 ∈ ( TopOn ‘ 𝑋 ) )
70 pttop ( ( 𝐵 ∈ V ∧ ( 𝐹𝐵 ) : 𝐵 ⟶ Top ) → ( ∏t ‘ ( 𝐹𝐵 ) ) ∈ Top )
71 47 48 70 syl2anc ( 𝜑 → ( ∏t ‘ ( 𝐹𝐵 ) ) ∈ Top )
72 5 71 eqeltrid ( 𝜑𝐿 ∈ Top )
73 2 toptopon ( 𝐿 ∈ Top ↔ 𝐿 ∈ ( TopOn ‘ 𝑌 ) )
74 72 73 sylib ( 𝜑𝐿 ∈ ( TopOn ‘ 𝑌 ) )
75 txtopon ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
76 69 74 75 syl2anc ( 𝜑 → ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
77 9 eleq2d ( 𝜑 → ( 𝑘𝐶𝑘 ∈ ( 𝐴𝐵 ) ) )
78 77 biimpa ( ( 𝜑𝑘𝐶 ) → 𝑘 ∈ ( 𝐴𝐵 ) )
79 elun ( 𝑘 ∈ ( 𝐴𝐵 ) ↔ ( 𝑘𝐴𝑘𝐵 ) )
80 78 79 sylib ( ( 𝜑𝑘𝐶 ) → ( 𝑘𝐴𝑘𝐵 ) )
81 ixpfn ( ( 1st𝑧 ) ∈ X 𝑛𝐴 ( 𝐹𝑛 ) → ( 1st𝑧 ) Fn 𝐴 )
82 33 81 syl ( ( 𝜑𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( 1st𝑧 ) Fn 𝐴 )
83 82 adantlr ( ( ( 𝜑𝑘𝐴 ) ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( 1st𝑧 ) Fn 𝐴 )
84 52 adantr ( ( 𝜑𝑧 ∈ ( 𝑋 × 𝑌 ) ) → X 𝑛𝐵 ( 𝐹𝑛 ) = 𝑌 )
85 35 84 eleqtrrd ( ( 𝜑𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( 2nd𝑧 ) ∈ X 𝑛𝐵 ( 𝐹𝑛 ) )
86 ixpfn ( ( 2nd𝑧 ) ∈ X 𝑛𝐵 ( 𝐹𝑛 ) → ( 2nd𝑧 ) Fn 𝐵 )
87 85 86 syl ( ( 𝜑𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( 2nd𝑧 ) Fn 𝐵 )
88 87 adantlr ( ( ( 𝜑𝑘𝐴 ) ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( 2nd𝑧 ) Fn 𝐵 )
89 10 ad2antrr ( ( ( 𝜑𝑘𝐴 ) ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( 𝐴𝐵 ) = ∅ )
90 simplr ( ( ( 𝜑𝑘𝐴 ) ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → 𝑘𝐴 )
91 fvun1 ( ( ( 1st𝑧 ) Fn 𝐴 ∧ ( 2nd𝑧 ) Fn 𝐵 ∧ ( ( 𝐴𝐵 ) = ∅ ∧ 𝑘𝐴 ) ) → ( ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) ‘ 𝑘 ) = ( ( 1st𝑧 ) ‘ 𝑘 ) )
92 83 88 89 90 91 syl112anc ( ( ( 𝜑𝑘𝐴 ) ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) ‘ 𝑘 ) = ( ( 1st𝑧 ) ‘ 𝑘 ) )
93 92 mpteq2dva ( ( 𝜑𝑘𝐴 ) → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) ‘ 𝑘 ) ) = ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 1st𝑧 ) ‘ 𝑘 ) ) )
94 76 adantr ( ( 𝜑𝑘𝐴 ) → ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
95 13 mpompt ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 1st𝑧 ) ) = ( 𝑥𝑋 , 𝑦𝑌𝑥 )
96 69 adantr ( ( 𝜑𝑘𝐴 ) → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
97 74 adantr ( ( 𝜑𝑘𝐴 ) → 𝐿 ∈ ( TopOn ‘ 𝑌 ) )
98 96 97 cnmpt1st ( ( 𝜑𝑘𝐴 ) → ( 𝑥𝑋 , 𝑦𝑌𝑥 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐾 ) )
99 95 98 eqeltrid ( ( 𝜑𝑘𝐴 ) → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 1st𝑧 ) ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐾 ) )
100 26 adantr ( ( 𝜑𝑘𝐴 ) → 𝐴 ∈ V )
101 27 adantr ( ( 𝜑𝑘𝐴 ) → ( 𝐹𝐴 ) : 𝐴 ⟶ Top )
102 simpr ( ( 𝜑𝑘𝐴 ) → 𝑘𝐴 )
103 1 4 ptpjcn ( ( 𝐴 ∈ V ∧ ( 𝐹𝐴 ) : 𝐴 ⟶ Top ∧ 𝑘𝐴 ) → ( 𝑓𝑋 ↦ ( 𝑓𝑘 ) ) ∈ ( 𝐾 Cn ( ( 𝐹𝐴 ) ‘ 𝑘 ) ) )
104 100 101 102 103 syl3anc ( ( 𝜑𝑘𝐴 ) → ( 𝑓𝑋 ↦ ( 𝑓𝑘 ) ) ∈ ( 𝐾 Cn ( ( 𝐹𝐴 ) ‘ 𝑘 ) ) )
105 fvres ( 𝑘𝐴 → ( ( 𝐹𝐴 ) ‘ 𝑘 ) = ( 𝐹𝑘 ) )
106 105 adantl ( ( 𝜑𝑘𝐴 ) → ( ( 𝐹𝐴 ) ‘ 𝑘 ) = ( 𝐹𝑘 ) )
107 106 oveq2d ( ( 𝜑𝑘𝐴 ) → ( 𝐾 Cn ( ( 𝐹𝐴 ) ‘ 𝑘 ) ) = ( 𝐾 Cn ( 𝐹𝑘 ) ) )
108 104 107 eleqtrd ( ( 𝜑𝑘𝐴 ) → ( 𝑓𝑋 ↦ ( 𝑓𝑘 ) ) ∈ ( 𝐾 Cn ( 𝐹𝑘 ) ) )
109 fveq1 ( 𝑓 = ( 1st𝑧 ) → ( 𝑓𝑘 ) = ( ( 1st𝑧 ) ‘ 𝑘 ) )
110 94 99 96 108 109 cnmpt11 ( ( 𝜑𝑘𝐴 ) → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 1st𝑧 ) ‘ 𝑘 ) ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn ( 𝐹𝑘 ) ) )
111 93 110 eqeltrd ( ( 𝜑𝑘𝐴 ) → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) ‘ 𝑘 ) ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn ( 𝐹𝑘 ) ) )
112 82 adantlr ( ( ( 𝜑𝑘𝐵 ) ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( 1st𝑧 ) Fn 𝐴 )
113 87 adantlr ( ( ( 𝜑𝑘𝐵 ) ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( 2nd𝑧 ) Fn 𝐵 )
114 10 ad2antrr ( ( ( 𝜑𝑘𝐵 ) ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( 𝐴𝐵 ) = ∅ )
115 simplr ( ( ( 𝜑𝑘𝐵 ) ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → 𝑘𝐵 )
116 fvun2 ( ( ( 1st𝑧 ) Fn 𝐴 ∧ ( 2nd𝑧 ) Fn 𝐵 ∧ ( ( 𝐴𝐵 ) = ∅ ∧ 𝑘𝐵 ) ) → ( ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) ‘ 𝑘 ) = ( ( 2nd𝑧 ) ‘ 𝑘 ) )
117 112 113 114 115 116 syl112anc ( ( ( 𝜑𝑘𝐵 ) ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) ‘ 𝑘 ) = ( ( 2nd𝑧 ) ‘ 𝑘 ) )
118 117 mpteq2dva ( ( 𝜑𝑘𝐵 ) → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) ‘ 𝑘 ) ) = ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 2nd𝑧 ) ‘ 𝑘 ) ) )
119 76 adantr ( ( 𝜑𝑘𝐵 ) → ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
120 14 mpompt ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 2nd𝑧 ) ) = ( 𝑥𝑋 , 𝑦𝑌𝑦 )
121 69 adantr ( ( 𝜑𝑘𝐵 ) → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
122 74 adantr ( ( 𝜑𝑘𝐵 ) → 𝐿 ∈ ( TopOn ‘ 𝑌 ) )
123 121 122 cnmpt2nd ( ( 𝜑𝑘𝐵 ) → ( 𝑥𝑋 , 𝑦𝑌𝑦 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐿 ) )
124 120 123 eqeltrid ( ( 𝜑𝑘𝐵 ) → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 2nd𝑧 ) ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐿 ) )
125 47 adantr ( ( 𝜑𝑘𝐵 ) → 𝐵 ∈ V )
126 48 adantr ( ( 𝜑𝑘𝐵 ) → ( 𝐹𝐵 ) : 𝐵 ⟶ Top )
127 simpr ( ( 𝜑𝑘𝐵 ) → 𝑘𝐵 )
128 2 5 ptpjcn ( ( 𝐵 ∈ V ∧ ( 𝐹𝐵 ) : 𝐵 ⟶ Top ∧ 𝑘𝐵 ) → ( 𝑓𝑌 ↦ ( 𝑓𝑘 ) ) ∈ ( 𝐿 Cn ( ( 𝐹𝐵 ) ‘ 𝑘 ) ) )
129 125 126 127 128 syl3anc ( ( 𝜑𝑘𝐵 ) → ( 𝑓𝑌 ↦ ( 𝑓𝑘 ) ) ∈ ( 𝐿 Cn ( ( 𝐹𝐵 ) ‘ 𝑘 ) ) )
130 fvres ( 𝑘𝐵 → ( ( 𝐹𝐵 ) ‘ 𝑘 ) = ( 𝐹𝑘 ) )
131 130 adantl ( ( 𝜑𝑘𝐵 ) → ( ( 𝐹𝐵 ) ‘ 𝑘 ) = ( 𝐹𝑘 ) )
132 131 oveq2d ( ( 𝜑𝑘𝐵 ) → ( 𝐿 Cn ( ( 𝐹𝐵 ) ‘ 𝑘 ) ) = ( 𝐿 Cn ( 𝐹𝑘 ) ) )
133 129 132 eleqtrd ( ( 𝜑𝑘𝐵 ) → ( 𝑓𝑌 ↦ ( 𝑓𝑘 ) ) ∈ ( 𝐿 Cn ( 𝐹𝑘 ) ) )
134 fveq1 ( 𝑓 = ( 2nd𝑧 ) → ( 𝑓𝑘 ) = ( ( 2nd𝑧 ) ‘ 𝑘 ) )
135 119 124 122 133 134 cnmpt11 ( ( 𝜑𝑘𝐵 ) → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 2nd𝑧 ) ‘ 𝑘 ) ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn ( 𝐹𝑘 ) ) )
136 118 135 eqeltrd ( ( 𝜑𝑘𝐵 ) → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) ‘ 𝑘 ) ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn ( 𝐹𝑘 ) ) )
137 111 136 jaodan ( ( 𝜑 ∧ ( 𝑘𝐴𝑘𝐵 ) ) → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) ‘ 𝑘 ) ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn ( 𝐹𝑘 ) ) )
138 80 137 syldan ( ( 𝜑𝑘𝐶 ) → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) ‘ 𝑘 ) ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn ( 𝐹𝑘 ) ) )
139 3 76 7 8 138 ptcn ( 𝜑 → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 𝑘𝐶 ↦ ( ( ( 1st𝑧 ) ∪ ( 2nd𝑧 ) ) ‘ 𝑘 ) ) ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )
140 64 139 eqeltrd ( 𝜑𝐺 ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )
141 1 2 3 4 5 6 7 8 9 10 ptuncnv ( 𝜑 𝐺 = ( 𝑧 𝐽 ↦ ⟨ ( 𝑧𝐴 ) , ( 𝑧𝐵 ) ⟩ ) )
142 pttop ( ( 𝐶𝑉𝐹 : 𝐶 ⟶ Top ) → ( ∏t𝐹 ) ∈ Top )
143 7 8 142 syl2anc ( 𝜑 → ( ∏t𝐹 ) ∈ Top )
144 3 143 eqeltrid ( 𝜑𝐽 ∈ Top )
145 eqid 𝐽 = 𝐽
146 145 toptopon ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝐽 ) )
147 144 146 sylib ( 𝜑𝐽 ∈ ( TopOn ‘ 𝐽 ) )
148 145 3 4 ptrescn ( ( 𝐶𝑉𝐹 : 𝐶 ⟶ Top ∧ 𝐴𝐶 ) → ( 𝑧 𝐽 ↦ ( 𝑧𝐴 ) ) ∈ ( 𝐽 Cn 𝐾 ) )
149 7 8 25 148 syl3anc ( 𝜑 → ( 𝑧 𝐽 ↦ ( 𝑧𝐴 ) ) ∈ ( 𝐽 Cn 𝐾 ) )
150 145 3 5 ptrescn ( ( 𝐶𝑉𝐹 : 𝐶 ⟶ Top ∧ 𝐵𝐶 ) → ( 𝑧 𝐽 ↦ ( 𝑧𝐵 ) ) ∈ ( 𝐽 Cn 𝐿 ) )
151 7 8 46 150 syl3anc ( 𝜑 → ( 𝑧 𝐽 ↦ ( 𝑧𝐵 ) ) ∈ ( 𝐽 Cn 𝐿 ) )
152 147 149 151 cnmpt1t ( 𝜑 → ( 𝑧 𝐽 ↦ ⟨ ( 𝑧𝐴 ) , ( 𝑧𝐵 ) ⟩ ) ∈ ( 𝐽 Cn ( 𝐾 ×t 𝐿 ) ) )
153 141 152 eqeltrd ( 𝜑 𝐺 ∈ ( 𝐽 Cn ( 𝐾 ×t 𝐿 ) ) )
154 ishmeo ( 𝐺 ∈ ( ( 𝐾 ×t 𝐿 ) Homeo 𝐽 ) ↔ ( 𝐺 ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) ∧ 𝐺 ∈ ( 𝐽 Cn ( 𝐾 ×t 𝐿 ) ) ) )
155 140 153 154 sylanbrc ( 𝜑𝐺 ∈ ( ( 𝐾 ×t 𝐿 ) Homeo 𝐽 ) )