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

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 eqtrid ⊢ ( 𝜑 → 𝐺 = ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 𝑘 ∈ 𝐶 ↦ ( ( ( 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 𝐽 ) )