MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  txhmeo Structured version   Visualization version   GIF version
Theorem txhmeo 23307
Description: Lift a pair of homeomorphisms on the factors to a homeomorphism of product topologies. (Contributed by Mario Carneiro, 2-Sep-2015.)
Hypotheses
Ref Expression
txhmeo.1 𝑋 = βˆͺ 𝐽
txhmeo.2 π‘Œ = βˆͺ 𝐾
txhmeo.3 (πœ‘ β†’ 𝐹 ∈ (𝐽Homeo𝐿))
txhmeo.4 (πœ‘ β†’ 𝐺 ∈ (𝐾Homeo𝑀))
Assertion
Ref Expression
txhmeo (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) ∈ ((𝐽 Γ—t 𝐾)Homeo(𝐿 Γ—t 𝑀)))
Distinct variable groups:   π‘₯,𝑦,𝐹   π‘₯,𝐽,𝑦   π‘₯,𝐾,𝑦   πœ‘,π‘₯,𝑦   π‘₯,𝐺,𝑦   π‘₯,𝐿,𝑦   π‘₯,𝑋,𝑦   π‘₯,π‘Œ,𝑦   π‘₯,𝑀,𝑦
Proof of Theorem txhmeo
Dummy variables 𝑣 𝑒 𝑀 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 txhmeo.3 . . . . . 6 (πœ‘ β†’ 𝐹 ∈ (𝐽Homeo𝐿))
2 hmeocn 23264 . . . . . 6 (𝐹 ∈ (𝐽Homeo𝐿) β†’ 𝐹 ∈ (𝐽 Cn 𝐿))
31, 2syl 17 . . . . 5 (πœ‘ β†’ 𝐹 ∈ (𝐽 Cn 𝐿))
4 cntop1 22744 . . . . 5 (𝐹 ∈ (𝐽 Cn 𝐿) β†’ 𝐽 ∈ Top)
53, 4syl 17 . . . 4 (πœ‘ β†’ 𝐽 ∈ Top)
6 txhmeo.1 . . . . 5 𝑋 = βˆͺ 𝐽
76toptopon 22419 . . . 4 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOnβ€˜π‘‹))
85, 7sylib 217 . . 3 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
9 txhmeo.4 . . . . . 6 (πœ‘ β†’ 𝐺 ∈ (𝐾Homeo𝑀))
10 hmeocn 23264 . . . . . 6 (𝐺 ∈ (𝐾Homeo𝑀) β†’ 𝐺 ∈ (𝐾 Cn 𝑀))
119, 10syl 17 . . . . 5 (πœ‘ β†’ 𝐺 ∈ (𝐾 Cn 𝑀))
12 cntop1 22744 . . . . 5 (𝐺 ∈ (𝐾 Cn 𝑀) β†’ 𝐾 ∈ Top)
1311, 12syl 17 . . . 4 (πœ‘ β†’ 𝐾 ∈ Top)
14 txhmeo.2 . . . . 5 π‘Œ = βˆͺ 𝐾
1514toptopon 22419 . . . 4 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOnβ€˜π‘Œ))
1613, 15sylib 217 . . 3 (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜π‘Œ))
178, 16cnmpt1st 23172 . . . 4 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ π‘₯) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐽))
188, 16, 17, 3cnmpt21f 23176 . . 3 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ (πΉβ€˜π‘₯)) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿))
198, 16cnmpt2nd 23173 . . . 4 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ 𝑦) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐾))
208, 16, 19, 11cnmpt21f 23176 . . 3 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ (πΊβ€˜π‘¦)) ∈ ((𝐽 Γ—t 𝐾) Cn 𝑀))
218, 16, 18, 20cnmpt2t 23177 . 2 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) ∈ ((𝐽 Γ—t 𝐾) Cn (𝐿 Γ—t 𝑀)))
22 vex 3479 . . . . . . . . . . 11 π‘₯ ∈ V
23 vex 3479 . . . . . . . . . . 11 𝑦 ∈ V
2422, 23op1std 7985 . . . . . . . . . 10 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ (1st β€˜π‘’) = π‘₯)
2524fveq2d 6896 . . . . . . . . 9 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ (πΉβ€˜(1st β€˜π‘’)) = (πΉβ€˜π‘₯))
2622, 23op2ndd 7986 . . . . . . . . . 10 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ (2nd β€˜π‘’) = 𝑦)
2726fveq2d 6896 . . . . . . . . 9 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ (πΊβ€˜(2nd β€˜π‘’)) = (πΊβ€˜π‘¦))
2825, 27opeq12d 4882 . . . . . . . 8 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩ = ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩)
2928mpompt 7522 . . . . . . 7 (𝑒 ∈ (𝑋 Γ— π‘Œ) ↦ ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩) = (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩)
3029eqcomi 2742 . . . . . 6 (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) = (𝑒 ∈ (𝑋 Γ— π‘Œ) ↦ ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩)
31 eqid 2733 . . . . . . . . . 10 βˆͺ 𝐿 = βˆͺ 𝐿
326, 31cnf 22750 . . . . . . . . 9 (𝐹 ∈ (𝐽 Cn 𝐿) β†’ 𝐹:π‘‹βŸΆβˆͺ 𝐿)
333, 32syl 17 . . . . . . . 8 (πœ‘ β†’ 𝐹:π‘‹βŸΆβˆͺ 𝐿)
34 xp1st 8007 . . . . . . . 8 (𝑒 ∈ (𝑋 Γ— π‘Œ) β†’ (1st β€˜π‘’) ∈ 𝑋)
35 ffvelcdm 7084 . . . . . . . 8 ((𝐹:π‘‹βŸΆβˆͺ 𝐿 ∧ (1st β€˜π‘’) ∈ 𝑋) β†’ (πΉβ€˜(1st β€˜π‘’)) ∈ βˆͺ 𝐿)
3633, 34, 35syl2an 597 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ (𝑋 Γ— π‘Œ)) β†’ (πΉβ€˜(1st β€˜π‘’)) ∈ βˆͺ 𝐿)
37 eqid 2733 . . . . . . . . . 10 βˆͺ 𝑀 = βˆͺ 𝑀
3814, 37cnf 22750 . . . . . . . . 9 (𝐺 ∈ (𝐾 Cn 𝑀) β†’ 𝐺:π‘ŒβŸΆβˆͺ 𝑀)
3911, 38syl 17 . . . . . . . 8 (πœ‘ β†’ 𝐺:π‘ŒβŸΆβˆͺ 𝑀)
40 xp2nd 8008 . . . . . . . 8 (𝑒 ∈ (𝑋 Γ— π‘Œ) β†’ (2nd β€˜π‘’) ∈ π‘Œ)
41 ffvelcdm 7084 . . . . . . . 8 ((𝐺:π‘ŒβŸΆβˆͺ 𝑀 ∧ (2nd β€˜π‘’) ∈ π‘Œ) β†’ (πΊβ€˜(2nd β€˜π‘’)) ∈ βˆͺ 𝑀)
4239, 40, 41syl2an 597 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ (𝑋 Γ— π‘Œ)) β†’ (πΊβ€˜(2nd β€˜π‘’)) ∈ βˆͺ 𝑀)
4336, 42opelxpd 5716 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ (𝑋 Γ— π‘Œ)) β†’ ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩ ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))
446, 31hmeof1o 23268 . . . . . . . . . 10 (𝐹 ∈ (𝐽Homeo𝐿) β†’ 𝐹:𝑋–1-1-ontoβ†’βˆͺ 𝐿)
451, 44syl 17 . . . . . . . . 9 (πœ‘ β†’ 𝐹:𝑋–1-1-ontoβ†’βˆͺ 𝐿)
46 f1ocnv 6846 . . . . . . . . 9 (𝐹:𝑋–1-1-ontoβ†’βˆͺ 𝐿 β†’ ◑𝐹:βˆͺ 𝐿–1-1-onto→𝑋)
47 f1of 6834 . . . . . . . . 9 (◑𝐹:βˆͺ 𝐿–1-1-onto→𝑋 β†’ ◑𝐹:βˆͺ πΏβŸΆπ‘‹)
4845, 46, 473syl 18 . . . . . . . 8 (πœ‘ β†’ ◑𝐹:βˆͺ πΏβŸΆπ‘‹)
49 xp1st 8007 . . . . . . . 8 (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) β†’ (1st β€˜π‘£) ∈ βˆͺ 𝐿)
50 ffvelcdm 7084 . . . . . . . 8 ((◑𝐹:βˆͺ πΏβŸΆπ‘‹ ∧ (1st β€˜π‘£) ∈ βˆͺ 𝐿) β†’ (β—‘πΉβ€˜(1st β€˜π‘£)) ∈ 𝑋)
5148, 49, 50syl2an 597 . . . . . . 7 ((πœ‘ ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀)) β†’ (β—‘πΉβ€˜(1st β€˜π‘£)) ∈ 𝑋)
5214, 37hmeof1o 23268 . . . . . . . . . 10 (𝐺 ∈ (𝐾Homeo𝑀) β†’ 𝐺:π‘Œβ€“1-1-ontoβ†’βˆͺ 𝑀)
539, 52syl 17 . . . . . . . . 9 (πœ‘ β†’ 𝐺:π‘Œβ€“1-1-ontoβ†’βˆͺ 𝑀)
54 f1ocnv 6846 . . . . . . . . 9 (𝐺:π‘Œβ€“1-1-ontoβ†’βˆͺ 𝑀 β†’ ◑𝐺:βˆͺ 𝑀–1-1-ontoβ†’π‘Œ)
55 f1of 6834 . . . . . . . . 9 (◑𝐺:βˆͺ 𝑀–1-1-ontoβ†’π‘Œ β†’ ◑𝐺:βˆͺ π‘€βŸΆπ‘Œ)
5653, 54, 553syl 18 . . . . . . . 8 (πœ‘ β†’ ◑𝐺:βˆͺ π‘€βŸΆπ‘Œ)
57 xp2nd 8008 . . . . . . . 8 (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) β†’ (2nd β€˜π‘£) ∈ βˆͺ 𝑀)
58 ffvelcdm 7084 . . . . . . . 8 ((◑𝐺:βˆͺ π‘€βŸΆπ‘Œ ∧ (2nd β€˜π‘£) ∈ βˆͺ 𝑀) β†’ (β—‘πΊβ€˜(2nd β€˜π‘£)) ∈ π‘Œ)
5956, 57, 58syl2an 597 . . . . . . 7 ((πœ‘ ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀)) β†’ (β—‘πΊβ€˜(2nd β€˜π‘£)) ∈ π‘Œ)
6051, 59opelxpd 5716 . . . . . 6 ((πœ‘ ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀)) β†’ ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩ ∈ (𝑋 Γ— π‘Œ))
6145adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ 𝐹:𝑋–1-1-ontoβ†’βˆͺ 𝐿)
6234ad2antrl 727 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (1st β€˜π‘’) ∈ 𝑋)
6349ad2antll 728 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (1st β€˜π‘£) ∈ βˆͺ 𝐿)
64 f1ocnvfvb 7277 . . . . . . . . . 10 ((𝐹:𝑋–1-1-ontoβ†’βˆͺ 𝐿 ∧ (1st β€˜π‘’) ∈ 𝑋 ∧ (1st β€˜π‘£) ∈ βˆͺ 𝐿) β†’ ((πΉβ€˜(1st β€˜π‘’)) = (1st β€˜π‘£) ↔ (β—‘πΉβ€˜(1st β€˜π‘£)) = (1st β€˜π‘’)))
6561, 62, 63, 64syl3anc 1372 . . . . . . . . 9 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ ((πΉβ€˜(1st β€˜π‘’)) = (1st β€˜π‘£) ↔ (β—‘πΉβ€˜(1st β€˜π‘£)) = (1st β€˜π‘’)))
66 eqcom 2740 . . . . . . . . 9 ((1st β€˜π‘£) = (πΉβ€˜(1st β€˜π‘’)) ↔ (πΉβ€˜(1st β€˜π‘’)) = (1st β€˜π‘£))
67 eqcom 2740 . . . . . . . . 9 ((1st β€˜π‘’) = (β—‘πΉβ€˜(1st β€˜π‘£)) ↔ (β—‘πΉβ€˜(1st β€˜π‘£)) = (1st β€˜π‘’))
6865, 66, 673bitr4g 314 . . . . . . . 8 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ ((1st β€˜π‘£) = (πΉβ€˜(1st β€˜π‘’)) ↔ (1st β€˜π‘’) = (β—‘πΉβ€˜(1st β€˜π‘£))))
6953adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ 𝐺:π‘Œβ€“1-1-ontoβ†’βˆͺ 𝑀)
7040ad2antrl 727 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (2nd β€˜π‘’) ∈ π‘Œ)
7157ad2antll 728 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (2nd β€˜π‘£) ∈ βˆͺ 𝑀)
72 f1ocnvfvb 7277 . . . . . . . . . 10 ((𝐺:π‘Œβ€“1-1-ontoβ†’βˆͺ 𝑀 ∧ (2nd β€˜π‘’) ∈ π‘Œ ∧ (2nd β€˜π‘£) ∈ βˆͺ 𝑀) β†’ ((πΊβ€˜(2nd β€˜π‘’)) = (2nd β€˜π‘£) ↔ (β—‘πΊβ€˜(2nd β€˜π‘£)) = (2nd β€˜π‘’)))
7369, 70, 71, 72syl3anc 1372 . . . . . . . . 9 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ ((πΊβ€˜(2nd β€˜π‘’)) = (2nd β€˜π‘£) ↔ (β—‘πΊβ€˜(2nd β€˜π‘£)) = (2nd β€˜π‘’)))
74 eqcom 2740 . . . . . . . . 9 ((2nd β€˜π‘£) = (πΊβ€˜(2nd β€˜π‘’)) ↔ (πΊβ€˜(2nd β€˜π‘’)) = (2nd β€˜π‘£))
75 eqcom 2740 . . . . . . . . 9 ((2nd β€˜π‘’) = (β—‘πΊβ€˜(2nd β€˜π‘£)) ↔ (β—‘πΊβ€˜(2nd β€˜π‘£)) = (2nd β€˜π‘’))
7673, 74, 753bitr4g 314 . . . . . . . 8 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ ((2nd β€˜π‘£) = (πΊβ€˜(2nd β€˜π‘’)) ↔ (2nd β€˜π‘’) = (β—‘πΊβ€˜(2nd β€˜π‘£))))
7768, 76anbi12d 632 . . . . . . 7 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (((1st β€˜π‘£) = (πΉβ€˜(1st β€˜π‘’)) ∧ (2nd β€˜π‘£) = (πΊβ€˜(2nd β€˜π‘’))) ↔ ((1st β€˜π‘’) = (β—‘πΉβ€˜(1st β€˜π‘£)) ∧ (2nd β€˜π‘’) = (β—‘πΊβ€˜(2nd β€˜π‘£)))))
78 eqop 8017 . . . . . . . 8 (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) β†’ (𝑣 = ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩ ↔ ((1st β€˜π‘£) = (πΉβ€˜(1st β€˜π‘’)) ∧ (2nd β€˜π‘£) = (πΊβ€˜(2nd β€˜π‘’)))))
7978ad2antll 728 . . . . . . 7 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (𝑣 = ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩ ↔ ((1st β€˜π‘£) = (πΉβ€˜(1st β€˜π‘’)) ∧ (2nd β€˜π‘£) = (πΊβ€˜(2nd β€˜π‘’)))))
80 eqop 8017 . . . . . . . 8 (𝑒 ∈ (𝑋 Γ— π‘Œ) β†’ (𝑒 = ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩ ↔ ((1st β€˜π‘’) = (β—‘πΉβ€˜(1st β€˜π‘£)) ∧ (2nd β€˜π‘’) = (β—‘πΊβ€˜(2nd β€˜π‘£)))))
8180ad2antrl 727 . . . . . . 7 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (𝑒 = ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩ ↔ ((1st β€˜π‘’) = (β—‘πΉβ€˜(1st β€˜π‘£)) ∧ (2nd β€˜π‘’) = (β—‘πΊβ€˜(2nd β€˜π‘£)))))
8277, 79, 813bitr4rd 312 . . . . . 6 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (𝑒 = ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩ ↔ 𝑣 = ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩))
8330, 43, 60, 82f1ocnv2d 7659 . . . . 5 (πœ‘ β†’ ((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩):(𝑋 Γ— π‘Œ)–1-1-ontoβ†’(βˆͺ 𝐿 Γ— βˆͺ 𝑀) ∧ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) = (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) ↦ ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩)))
8483simprd 497 . . . 4 (πœ‘ β†’ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) = (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) ↦ ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩))
85 vex 3479 . . . . . . . 8 𝑧 ∈ V
86 vex 3479 . . . . . . . 8 𝑀 ∈ V
8785, 86op1std 7985 . . . . . . 7 (𝑣 = βŸ¨π‘§, π‘€βŸ© β†’ (1st β€˜π‘£) = 𝑧)
8887fveq2d 6896 . . . . . 6 (𝑣 = βŸ¨π‘§, π‘€βŸ© β†’ (β—‘πΉβ€˜(1st β€˜π‘£)) = (β—‘πΉβ€˜π‘§))
8985, 86op2ndd 7986 . . . . . . 7 (𝑣 = βŸ¨π‘§, π‘€βŸ© β†’ (2nd β€˜π‘£) = 𝑀)
9089fveq2d 6896 . . . . . 6 (𝑣 = βŸ¨π‘§, π‘€βŸ© β†’ (β—‘πΊβ€˜(2nd β€˜π‘£)) = (β—‘πΊβ€˜π‘€))
9188, 90opeq12d 4882 . . . . 5 (𝑣 = βŸ¨π‘§, π‘€βŸ© β†’ ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩ = ⟨(β—‘πΉβ€˜π‘§), (β—‘πΊβ€˜π‘€)⟩)
9291mpompt 7522 . . . 4 (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) ↦ ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩) = (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ ⟨(β—‘πΉβ€˜π‘§), (β—‘πΊβ€˜π‘€)⟩)
9384, 92eqtrdi 2789 . . 3 (πœ‘ β†’ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) = (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ ⟨(β—‘πΉβ€˜π‘§), (β—‘πΊβ€˜π‘€)⟩))
94 cntop2 22745 . . . . . 6 (𝐹 ∈ (𝐽 Cn 𝐿) β†’ 𝐿 ∈ Top)
953, 94syl 17 . . . . 5 (πœ‘ β†’ 𝐿 ∈ Top)
9631toptopon 22419 . . . . 5 (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿))
9795, 96sylib 217 . . . 4 (πœ‘ β†’ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿))
98 cntop2 22745 . . . . . 6 (𝐺 ∈ (𝐾 Cn 𝑀) β†’ 𝑀 ∈ Top)
9911, 98syl 17 . . . . 5 (πœ‘ β†’ 𝑀 ∈ Top)
10037toptopon 22419 . . . . 5 (𝑀 ∈ Top ↔ 𝑀 ∈ (TopOnβ€˜βˆͺ 𝑀))
10199, 100sylib 217 . . . 4 (πœ‘ β†’ 𝑀 ∈ (TopOnβ€˜βˆͺ 𝑀))
10297, 101cnmpt1st 23172 . . . . 5 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ 𝑧) ∈ ((𝐿 Γ—t 𝑀) Cn 𝐿))
103 hmeocnvcn 23265 . . . . . 6 (𝐹 ∈ (𝐽Homeo𝐿) β†’ ◑𝐹 ∈ (𝐿 Cn 𝐽))
1041, 103syl 17 . . . . 5 (πœ‘ β†’ ◑𝐹 ∈ (𝐿 Cn 𝐽))
10597, 101, 102, 104cnmpt21f 23176 . . . 4 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ (β—‘πΉβ€˜π‘§)) ∈ ((𝐿 Γ—t 𝑀) Cn 𝐽))
10697, 101cnmpt2nd 23173 . . . . 5 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ 𝑀) ∈ ((𝐿 Γ—t 𝑀) Cn 𝑀))
107 hmeocnvcn 23265 . . . . . 6 (𝐺 ∈ (𝐾Homeo𝑀) β†’ ◑𝐺 ∈ (𝑀 Cn 𝐾))
1089, 107syl 17 . . . . 5 (πœ‘ β†’ ◑𝐺 ∈ (𝑀 Cn 𝐾))
10997, 101, 106, 108cnmpt21f 23176 . . . 4 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ (β—‘πΊβ€˜π‘€)) ∈ ((𝐿 Γ—t 𝑀) Cn 𝐾))
11097, 101, 105, 109cnmpt2t 23177 . . 3 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ ⟨(β—‘πΉβ€˜π‘§), (β—‘πΊβ€˜π‘€)⟩) ∈ ((𝐿 Γ—t 𝑀) Cn (𝐽 Γ—t 𝐾)))
11193, 110eqeltrd 2834 . 2 (πœ‘ β†’ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) ∈ ((𝐿 Γ—t 𝑀) Cn (𝐽 Γ—t 𝐾)))
112 ishmeo 23263 . 2 ((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) ∈ ((𝐽 Γ—t 𝐾)Homeo(𝐿 Γ—t 𝑀)) ↔ ((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) ∈ ((𝐽 Γ—t 𝐾) Cn (𝐿 Γ—t 𝑀)) ∧ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) ∈ ((𝐿 Γ—t 𝑀) Cn (𝐽 Γ—t 𝐾))))
11321, 111, 112sylanbrc 584 1 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) ∈ ((𝐽 Γ—t 𝐾)Homeo(𝐿 Γ—t 𝑀)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  βŸ¨cop 4635  βˆͺ cuni 4909   ↦ cmpt 5232   Γ— cxp 5675  β—‘ccnv 5676  βŸΆwf 6540  β€“1-1-ontoβ†’wf1o 6543  β€˜cfv 6544  (class class class)co 7409   ∈ cmpo 7411  1st c1st 7973  2nd c2nd 7974  Topctop 22395  TopOnctopon 22412   Cn ccn 22728   Γ—t ctx 23064  Homeochmeo 23257
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-1st 7975  df-2nd 7976  df-map 8822  df-topgen 17389  df-top 22396  df-topon 22413  df-bases 22449  df-cn 22731  df-tx 23066  df-hmeo 23259
This theorem is referenced by:  xpstopnlem1  23313
  Copyright terms: Public domain W3C validator