MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  txhmeo Structured version   Visualization version   GIF version

Theorem txhmeo 22995
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 22952 . . . . . 6 (𝐹 ∈ (𝐽Homeo𝐿) β†’ 𝐹 ∈ (𝐽 Cn 𝐿))
31, 2syl 17 . . . . 5 (πœ‘ β†’ 𝐹 ∈ (𝐽 Cn 𝐿))
4 cntop1 22432 . . . . 5 (𝐹 ∈ (𝐽 Cn 𝐿) β†’ 𝐽 ∈ Top)
53, 4syl 17 . . . 4 (πœ‘ β†’ 𝐽 ∈ Top)
6 txhmeo.1 . . . . 5 𝑋 = βˆͺ 𝐽
76toptopon 22107 . . . 4 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOnβ€˜π‘‹))
85, 7sylib 217 . . 3 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
9 txhmeo.4 . . . . . 6 (πœ‘ β†’ 𝐺 ∈ (𝐾Homeo𝑀))
10 hmeocn 22952 . . . . . 6 (𝐺 ∈ (𝐾Homeo𝑀) β†’ 𝐺 ∈ (𝐾 Cn 𝑀))
119, 10syl 17 . . . . 5 (πœ‘ β†’ 𝐺 ∈ (𝐾 Cn 𝑀))
12 cntop1 22432 . . . . 5 (𝐺 ∈ (𝐾 Cn 𝑀) β†’ 𝐾 ∈ Top)
1311, 12syl 17 . . . 4 (πœ‘ β†’ 𝐾 ∈ Top)
14 txhmeo.2 . . . . 5 π‘Œ = βˆͺ 𝐾
1514toptopon 22107 . . . 4 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOnβ€˜π‘Œ))
1613, 15sylib 217 . . 3 (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜π‘Œ))
178, 16cnmpt1st 22860 . . . 4 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ π‘₯) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐽))
188, 16, 17, 3cnmpt21f 22864 . . 3 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ (πΉβ€˜π‘₯)) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿))
198, 16cnmpt2nd 22861 . . . 4 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ 𝑦) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐾))
208, 16, 19, 11cnmpt21f 22864 . . 3 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ (πΊβ€˜π‘¦)) ∈ ((𝐽 Γ—t 𝐾) Cn 𝑀))
218, 16, 18, 20cnmpt2t 22865 . 2 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) ∈ ((𝐽 Γ—t 𝐾) Cn (𝐿 Γ—t 𝑀)))
22 vex 3441 . . . . . . . . . . 11 π‘₯ ∈ V
23 vex 3441 . . . . . . . . . . 11 𝑦 ∈ V
2422, 23op1std 7869 . . . . . . . . . 10 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ (1st β€˜π‘’) = π‘₯)
2524fveq2d 6804 . . . . . . . . 9 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ (πΉβ€˜(1st β€˜π‘’)) = (πΉβ€˜π‘₯))
2622, 23op2ndd 7870 . . . . . . . . . 10 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ (2nd β€˜π‘’) = 𝑦)
2726fveq2d 6804 . . . . . . . . 9 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ (πΊβ€˜(2nd β€˜π‘’)) = (πΊβ€˜π‘¦))
2825, 27opeq12d 4817 . . . . . . . 8 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩ = ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩)
2928mpompt 7416 . . . . . . 7 (𝑒 ∈ (𝑋 Γ— π‘Œ) ↦ ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩) = (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩)
3029eqcomi 2745 . . . . . 6 (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) = (𝑒 ∈ (𝑋 Γ— π‘Œ) ↦ ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩)
31 eqid 2736 . . . . . . . . . 10 βˆͺ 𝐿 = βˆͺ 𝐿
326, 31cnf 22438 . . . . . . . . 9 (𝐹 ∈ (𝐽 Cn 𝐿) β†’ 𝐹:π‘‹βŸΆβˆͺ 𝐿)
333, 32syl 17 . . . . . . . 8 (πœ‘ β†’ 𝐹:π‘‹βŸΆβˆͺ 𝐿)
34 xp1st 7891 . . . . . . . 8 (𝑒 ∈ (𝑋 Γ— π‘Œ) β†’ (1st β€˜π‘’) ∈ 𝑋)
35 ffvelcdm 6987 . . . . . . . 8 ((𝐹:π‘‹βŸΆβˆͺ 𝐿 ∧ (1st β€˜π‘’) ∈ 𝑋) β†’ (πΉβ€˜(1st β€˜π‘’)) ∈ βˆͺ 𝐿)
3633, 34, 35syl2an 597 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ (𝑋 Γ— π‘Œ)) β†’ (πΉβ€˜(1st β€˜π‘’)) ∈ βˆͺ 𝐿)
37 eqid 2736 . . . . . . . . . 10 βˆͺ 𝑀 = βˆͺ 𝑀
3814, 37cnf 22438 . . . . . . . . 9 (𝐺 ∈ (𝐾 Cn 𝑀) β†’ 𝐺:π‘ŒβŸΆβˆͺ 𝑀)
3911, 38syl 17 . . . . . . . 8 (πœ‘ β†’ 𝐺:π‘ŒβŸΆβˆͺ 𝑀)
40 xp2nd 7892 . . . . . . . 8 (𝑒 ∈ (𝑋 Γ— π‘Œ) β†’ (2nd β€˜π‘’) ∈ π‘Œ)
41 ffvelcdm 6987 . . . . . . . 8 ((𝐺:π‘ŒβŸΆβˆͺ 𝑀 ∧ (2nd β€˜π‘’) ∈ π‘Œ) β†’ (πΊβ€˜(2nd β€˜π‘’)) ∈ βˆͺ 𝑀)
4239, 40, 41syl2an 597 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ (𝑋 Γ— π‘Œ)) β†’ (πΊβ€˜(2nd β€˜π‘’)) ∈ βˆͺ 𝑀)
4336, 42opelxpd 5634 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ (𝑋 Γ— π‘Œ)) β†’ ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩ ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))
446, 31hmeof1o 22956 . . . . . . . . . 10 (𝐹 ∈ (𝐽Homeo𝐿) β†’ 𝐹:𝑋–1-1-ontoβ†’βˆͺ 𝐿)
451, 44syl 17 . . . . . . . . 9 (πœ‘ β†’ 𝐹:𝑋–1-1-ontoβ†’βˆͺ 𝐿)
46 f1ocnv 6754 . . . . . . . . 9 (𝐹:𝑋–1-1-ontoβ†’βˆͺ 𝐿 β†’ ◑𝐹:βˆͺ 𝐿–1-1-onto→𝑋)
47 f1of 6742 . . . . . . . . 9 (◑𝐹:βˆͺ 𝐿–1-1-onto→𝑋 β†’ ◑𝐹:βˆͺ πΏβŸΆπ‘‹)
4845, 46, 473syl 18 . . . . . . . 8 (πœ‘ β†’ ◑𝐹:βˆͺ πΏβŸΆπ‘‹)
49 xp1st 7891 . . . . . . . 8 (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) β†’ (1st β€˜π‘£) ∈ βˆͺ 𝐿)
50 ffvelcdm 6987 . . . . . . . 8 ((◑𝐹:βˆͺ πΏβŸΆπ‘‹ ∧ (1st β€˜π‘£) ∈ βˆͺ 𝐿) β†’ (β—‘πΉβ€˜(1st β€˜π‘£)) ∈ 𝑋)
5148, 49, 50syl2an 597 . . . . . . 7 ((πœ‘ ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀)) β†’ (β—‘πΉβ€˜(1st β€˜π‘£)) ∈ 𝑋)
5214, 37hmeof1o 22956 . . . . . . . . . 10 (𝐺 ∈ (𝐾Homeo𝑀) β†’ 𝐺:π‘Œβ€“1-1-ontoβ†’βˆͺ 𝑀)
539, 52syl 17 . . . . . . . . 9 (πœ‘ β†’ 𝐺:π‘Œβ€“1-1-ontoβ†’βˆͺ 𝑀)
54 f1ocnv 6754 . . . . . . . . 9 (𝐺:π‘Œβ€“1-1-ontoβ†’βˆͺ 𝑀 β†’ ◑𝐺:βˆͺ 𝑀–1-1-ontoβ†’π‘Œ)
55 f1of 6742 . . . . . . . . 9 (◑𝐺:βˆͺ 𝑀–1-1-ontoβ†’π‘Œ β†’ ◑𝐺:βˆͺ π‘€βŸΆπ‘Œ)
5653, 54, 553syl 18 . . . . . . . 8 (πœ‘ β†’ ◑𝐺:βˆͺ π‘€βŸΆπ‘Œ)
57 xp2nd 7892 . . . . . . . 8 (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) β†’ (2nd β€˜π‘£) ∈ βˆͺ 𝑀)
58 ffvelcdm 6987 . . . . . . . 8 ((◑𝐺:βˆͺ π‘€βŸΆπ‘Œ ∧ (2nd β€˜π‘£) ∈ βˆͺ 𝑀) β†’ (β—‘πΊβ€˜(2nd β€˜π‘£)) ∈ π‘Œ)
5956, 57, 58syl2an 597 . . . . . . 7 ((πœ‘ ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀)) β†’ (β—‘πΊβ€˜(2nd β€˜π‘£)) ∈ π‘Œ)
6051, 59opelxpd 5634 . . . . . 6 ((πœ‘ ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀)) β†’ ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩ ∈ (𝑋 Γ— π‘Œ))
6145adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ 𝐹:𝑋–1-1-ontoβ†’βˆͺ 𝐿)
6234ad2antrl 726 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (1st β€˜π‘’) ∈ 𝑋)
6349ad2antll 727 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (1st β€˜π‘£) ∈ βˆͺ 𝐿)
64 f1ocnvfvb 7179 . . . . . . . . . 10 ((𝐹:𝑋–1-1-ontoβ†’βˆͺ 𝐿 ∧ (1st β€˜π‘’) ∈ 𝑋 ∧ (1st β€˜π‘£) ∈ βˆͺ 𝐿) β†’ ((πΉβ€˜(1st β€˜π‘’)) = (1st β€˜π‘£) ↔ (β—‘πΉβ€˜(1st β€˜π‘£)) = (1st β€˜π‘’)))
6561, 62, 63, 64syl3anc 1371 . . . . . . . . 9 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ ((πΉβ€˜(1st β€˜π‘’)) = (1st β€˜π‘£) ↔ (β—‘πΉβ€˜(1st β€˜π‘£)) = (1st β€˜π‘’)))
66 eqcom 2743 . . . . . . . . 9 ((1st β€˜π‘£) = (πΉβ€˜(1st β€˜π‘’)) ↔ (πΉβ€˜(1st β€˜π‘’)) = (1st β€˜π‘£))
67 eqcom 2743 . . . . . . . . 9 ((1st β€˜π‘’) = (β—‘πΉβ€˜(1st β€˜π‘£)) ↔ (β—‘πΉβ€˜(1st β€˜π‘£)) = (1st β€˜π‘’))
6865, 66, 673bitr4g 315 . . . . . . . 8 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ ((1st β€˜π‘£) = (πΉβ€˜(1st β€˜π‘’)) ↔ (1st β€˜π‘’) = (β—‘πΉβ€˜(1st β€˜π‘£))))
6953adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ 𝐺:π‘Œβ€“1-1-ontoβ†’βˆͺ 𝑀)
7040ad2antrl 726 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (2nd β€˜π‘’) ∈ π‘Œ)
7157ad2antll 727 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (2nd β€˜π‘£) ∈ βˆͺ 𝑀)
72 f1ocnvfvb 7179 . . . . . . . . . 10 ((𝐺:π‘Œβ€“1-1-ontoβ†’βˆͺ 𝑀 ∧ (2nd β€˜π‘’) ∈ π‘Œ ∧ (2nd β€˜π‘£) ∈ βˆͺ 𝑀) β†’ ((πΊβ€˜(2nd β€˜π‘’)) = (2nd β€˜π‘£) ↔ (β—‘πΊβ€˜(2nd β€˜π‘£)) = (2nd β€˜π‘’)))
7369, 70, 71, 72syl3anc 1371 . . . . . . . . 9 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ ((πΊβ€˜(2nd β€˜π‘’)) = (2nd β€˜π‘£) ↔ (β—‘πΊβ€˜(2nd β€˜π‘£)) = (2nd β€˜π‘’)))
74 eqcom 2743 . . . . . . . . 9 ((2nd β€˜π‘£) = (πΊβ€˜(2nd β€˜π‘’)) ↔ (πΊβ€˜(2nd β€˜π‘’)) = (2nd β€˜π‘£))
75 eqcom 2743 . . . . . . . . 9 ((2nd β€˜π‘’) = (β—‘πΊβ€˜(2nd β€˜π‘£)) ↔ (β—‘πΊβ€˜(2nd β€˜π‘£)) = (2nd β€˜π‘’))
7673, 74, 753bitr4g 315 . . . . . . . 8 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ ((2nd β€˜π‘£) = (πΊβ€˜(2nd β€˜π‘’)) ↔ (2nd β€˜π‘’) = (β—‘πΊβ€˜(2nd β€˜π‘£))))
7768, 76anbi12d 632 . . . . . . 7 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (((1st β€˜π‘£) = (πΉβ€˜(1st β€˜π‘’)) ∧ (2nd β€˜π‘£) = (πΊβ€˜(2nd β€˜π‘’))) ↔ ((1st β€˜π‘’) = (β—‘πΉβ€˜(1st β€˜π‘£)) ∧ (2nd β€˜π‘’) = (β—‘πΊβ€˜(2nd β€˜π‘£)))))
78 eqop 7901 . . . . . . . 8 (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) β†’ (𝑣 = ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩ ↔ ((1st β€˜π‘£) = (πΉβ€˜(1st β€˜π‘’)) ∧ (2nd β€˜π‘£) = (πΊβ€˜(2nd β€˜π‘’)))))
7978ad2antll 727 . . . . . . 7 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (𝑣 = ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩ ↔ ((1st β€˜π‘£) = (πΉβ€˜(1st β€˜π‘’)) ∧ (2nd β€˜π‘£) = (πΊβ€˜(2nd β€˜π‘’)))))
80 eqop 7901 . . . . . . . 8 (𝑒 ∈ (𝑋 Γ— π‘Œ) β†’ (𝑒 = ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩ ↔ ((1st β€˜π‘’) = (β—‘πΉβ€˜(1st β€˜π‘£)) ∧ (2nd β€˜π‘’) = (β—‘πΊβ€˜(2nd β€˜π‘£)))))
8180ad2antrl 726 . . . . . . 7 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (𝑒 = ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩ ↔ ((1st β€˜π‘’) = (β—‘πΉβ€˜(1st β€˜π‘£)) ∧ (2nd β€˜π‘’) = (β—‘πΊβ€˜(2nd β€˜π‘£)))))
8277, 79, 813bitr4rd 313 . . . . . 6 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (𝑒 = ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩ ↔ 𝑣 = ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩))
8330, 43, 60, 82f1ocnv2d 7550 . . . . 5 (πœ‘ β†’ ((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩):(𝑋 Γ— π‘Œ)–1-1-ontoβ†’(βˆͺ 𝐿 Γ— βˆͺ 𝑀) ∧ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) = (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) ↦ ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩)))
8483simprd 497 . . . 4 (πœ‘ β†’ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) = (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) ↦ ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩))
85 vex 3441 . . . . . . . 8 𝑧 ∈ V
86 vex 3441 . . . . . . . 8 𝑀 ∈ V
8785, 86op1std 7869 . . . . . . 7 (𝑣 = βŸ¨π‘§, π‘€βŸ© β†’ (1st β€˜π‘£) = 𝑧)
8887fveq2d 6804 . . . . . 6 (𝑣 = βŸ¨π‘§, π‘€βŸ© β†’ (β—‘πΉβ€˜(1st β€˜π‘£)) = (β—‘πΉβ€˜π‘§))
8985, 86op2ndd 7870 . . . . . . 7 (𝑣 = βŸ¨π‘§, π‘€βŸ© β†’ (2nd β€˜π‘£) = 𝑀)
9089fveq2d 6804 . . . . . 6 (𝑣 = βŸ¨π‘§, π‘€βŸ© β†’ (β—‘πΊβ€˜(2nd β€˜π‘£)) = (β—‘πΊβ€˜π‘€))
9188, 90opeq12d 4817 . . . . 5 (𝑣 = βŸ¨π‘§, π‘€βŸ© β†’ ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩ = ⟨(β—‘πΉβ€˜π‘§), (β—‘πΊβ€˜π‘€)⟩)
9291mpompt 7416 . . . 4 (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) ↦ ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩) = (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ ⟨(β—‘πΉβ€˜π‘§), (β—‘πΊβ€˜π‘€)⟩)
9384, 92eqtrdi 2792 . . 3 (πœ‘ β†’ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) = (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ ⟨(β—‘πΉβ€˜π‘§), (β—‘πΊβ€˜π‘€)⟩))
94 cntop2 22433 . . . . . 6 (𝐹 ∈ (𝐽 Cn 𝐿) β†’ 𝐿 ∈ Top)
953, 94syl 17 . . . . 5 (πœ‘ β†’ 𝐿 ∈ Top)
9631toptopon 22107 . . . . 5 (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿))
9795, 96sylib 217 . . . 4 (πœ‘ β†’ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿))
98 cntop2 22433 . . . . . 6 (𝐺 ∈ (𝐾 Cn 𝑀) β†’ 𝑀 ∈ Top)
9911, 98syl 17 . . . . 5 (πœ‘ β†’ 𝑀 ∈ Top)
10037toptopon 22107 . . . . 5 (𝑀 ∈ Top ↔ 𝑀 ∈ (TopOnβ€˜βˆͺ 𝑀))
10199, 100sylib 217 . . . 4 (πœ‘ β†’ 𝑀 ∈ (TopOnβ€˜βˆͺ 𝑀))
10297, 101cnmpt1st 22860 . . . . 5 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ 𝑧) ∈ ((𝐿 Γ—t 𝑀) Cn 𝐿))
103 hmeocnvcn 22953 . . . . . 6 (𝐹 ∈ (𝐽Homeo𝐿) β†’ ◑𝐹 ∈ (𝐿 Cn 𝐽))
1041, 103syl 17 . . . . 5 (πœ‘ β†’ ◑𝐹 ∈ (𝐿 Cn 𝐽))
10597, 101, 102, 104cnmpt21f 22864 . . . 4 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ (β—‘πΉβ€˜π‘§)) ∈ ((𝐿 Γ—t 𝑀) Cn 𝐽))
10697, 101cnmpt2nd 22861 . . . . 5 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ 𝑀) ∈ ((𝐿 Γ—t 𝑀) Cn 𝑀))
107 hmeocnvcn 22953 . . . . . 6 (𝐺 ∈ (𝐾Homeo𝑀) β†’ ◑𝐺 ∈ (𝑀 Cn 𝐾))
1089, 107syl 17 . . . . 5 (πœ‘ β†’ ◑𝐺 ∈ (𝑀 Cn 𝐾))
10997, 101, 106, 108cnmpt21f 22864 . . . 4 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ (β—‘πΊβ€˜π‘€)) ∈ ((𝐿 Γ—t 𝑀) Cn 𝐾))
11097, 101, 105, 109cnmpt2t 22865 . . 3 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ ⟨(β—‘πΉβ€˜π‘§), (β—‘πΊβ€˜π‘€)⟩) ∈ ((𝐿 Γ—t 𝑀) Cn (𝐽 Γ—t 𝐾)))
11193, 110eqeltrd 2837 . 2 (πœ‘ β†’ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) ∈ ((𝐿 Γ—t 𝑀) Cn (𝐽 Γ—t 𝐾)))
112 ishmeo 22951 . 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 1539   ∈ wcel 2104  βŸ¨cop 4571  βˆͺ cuni 4844   ↦ cmpt 5164   Γ— cxp 5594  β—‘ccnv 5595  βŸΆwf 6450  β€“1-1-ontoβ†’wf1o 6453  β€˜cfv 6454  (class class class)co 7303   ∈ cmpo 7305  1st c1st 7857  2nd c2nd 7858  Topctop 22083  TopOnctopon 22100   Cn ccn 22416   Γ—t ctx 22752  Homeochmeo 22945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7616
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-id 5496  df-xp 5602  df-rel 5603  df-cnv 5604  df-co 5605  df-dm 5606  df-rn 5607  df-res 5608  df-ima 5609  df-iota 6406  df-fun 6456  df-fn 6457  df-f 6458  df-f1 6459  df-fo 6460  df-f1o 6461  df-fv 6462  df-ov 7306  df-oprab 7307  df-mpo 7308  df-1st 7859  df-2nd 7860  df-map 8644  df-topgen 17195  df-top 22084  df-topon 22101  df-bases 22137  df-cn 22419  df-tx 22754  df-hmeo 22947
This theorem is referenced by:  xpstopnlem1  23001
  Copyright terms: Public domain W3C validator