ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  txhmeo GIF version
Theorem txhmeo 13789
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 13775 . . . . . 6 (𝐹 ∈ (𝐽Homeo𝐿) β†’ 𝐹 ∈ (𝐽 Cn 𝐿))
31, 2syl 14 . . . . 5 (πœ‘ β†’ 𝐹 ∈ (𝐽 Cn 𝐿))
4 cntop1 13671 . . . . 5 (𝐹 ∈ (𝐽 Cn 𝐿) β†’ 𝐽 ∈ Top)
53, 4syl 14 . . . 4 (πœ‘ β†’ 𝐽 ∈ Top)
6 txhmeo.1 . . . . 5 𝑋 = βˆͺ 𝐽
76toptopon 13488 . . . 4 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOnβ€˜π‘‹))
85, 7sylib 122 . . 3 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
9 txhmeo.4 . . . . . 6 (πœ‘ β†’ 𝐺 ∈ (𝐾Homeo𝑀))
10 hmeocn 13775 . . . . . 6 (𝐺 ∈ (𝐾Homeo𝑀) β†’ 𝐺 ∈ (𝐾 Cn 𝑀))
119, 10syl 14 . . . . 5 (πœ‘ β†’ 𝐺 ∈ (𝐾 Cn 𝑀))
12 cntop1 13671 . . . . 5 (𝐺 ∈ (𝐾 Cn 𝑀) β†’ 𝐾 ∈ Top)
1311, 12syl 14 . . . 4 (πœ‘ β†’ 𝐾 ∈ Top)
14 txhmeo.2 . . . . 5 π‘Œ = βˆͺ 𝐾
1514toptopon 13488 . . . 4 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOnβ€˜π‘Œ))
1613, 15sylib 122 . . 3 (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜π‘Œ))
178, 16cnmpt1st 13758 . . . 4 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ π‘₯) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐽))
188, 16, 17, 3cnmpt21f 13762 . . 3 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ (πΉβ€˜π‘₯)) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿))
198, 16cnmpt2nd 13759 . . . 4 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ 𝑦) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐾))
208, 16, 19, 11cnmpt21f 13762 . . 3 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ (πΊβ€˜π‘¦)) ∈ ((𝐽 Γ—t 𝐾) Cn 𝑀))
218, 16, 18, 20cnmpt2t 13763 . 2 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) ∈ ((𝐽 Γ—t 𝐾) Cn (𝐿 Γ—t 𝑀)))
22 vex 2740 . . . . . . . . . . 11 π‘₯ ∈ V
23 vex 2740 . . . . . . . . . . 11 𝑦 ∈ V
2422, 23op1std 6148 . . . . . . . . . 10 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ (1st β€˜π‘’) = π‘₯)
2524fveq2d 5519 . . . . . . . . 9 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ (πΉβ€˜(1st β€˜π‘’)) = (πΉβ€˜π‘₯))
2622, 23op2ndd 6149 . . . . . . . . . 10 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ (2nd β€˜π‘’) = 𝑦)
2726fveq2d 5519 . . . . . . . . 9 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ (πΊβ€˜(2nd β€˜π‘’)) = (πΊβ€˜π‘¦))
2825, 27opeq12d 3786 . . . . . . . 8 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩ = ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩)
2928mpompt 5966 . . . . . . 7 (𝑒 ∈ (𝑋 Γ— π‘Œ) ↦ ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩) = (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩)
3029eqcomi 2181 . . . . . 6 (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) = (𝑒 ∈ (𝑋 Γ— π‘Œ) ↦ ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩)
31 eqid 2177 . . . . . . . . . 10 βˆͺ 𝐿 = βˆͺ 𝐿
326, 31cnf 13674 . . . . . . . . 9 (𝐹 ∈ (𝐽 Cn 𝐿) β†’ 𝐹:π‘‹βŸΆβˆͺ 𝐿)
333, 32syl 14 . . . . . . . 8 (πœ‘ β†’ 𝐹:π‘‹βŸΆβˆͺ 𝐿)
34 xp1st 6165 . . . . . . . 8 (𝑒 ∈ (𝑋 Γ— π‘Œ) β†’ (1st β€˜π‘’) ∈ 𝑋)
35 ffvelcdm 5649 . . . . . . . 8 ((𝐹:π‘‹βŸΆβˆͺ 𝐿 ∧ (1st β€˜π‘’) ∈ 𝑋) β†’ (πΉβ€˜(1st β€˜π‘’)) ∈ βˆͺ 𝐿)
3633, 34, 35syl2an 289 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ (𝑋 Γ— π‘Œ)) β†’ (πΉβ€˜(1st β€˜π‘’)) ∈ βˆͺ 𝐿)
37 eqid 2177 . . . . . . . . . 10 βˆͺ 𝑀 = βˆͺ 𝑀
3814, 37cnf 13674 . . . . . . . . 9 (𝐺 ∈ (𝐾 Cn 𝑀) β†’ 𝐺:π‘ŒβŸΆβˆͺ 𝑀)
3911, 38syl 14 . . . . . . . 8 (πœ‘ β†’ 𝐺:π‘ŒβŸΆβˆͺ 𝑀)
40 xp2nd 6166 . . . . . . . 8 (𝑒 ∈ (𝑋 Γ— π‘Œ) β†’ (2nd β€˜π‘’) ∈ π‘Œ)
41 ffvelcdm 5649 . . . . . . . 8 ((𝐺:π‘ŒβŸΆβˆͺ 𝑀 ∧ (2nd β€˜π‘’) ∈ π‘Œ) β†’ (πΊβ€˜(2nd β€˜π‘’)) ∈ βˆͺ 𝑀)
4239, 40, 41syl2an 289 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ (𝑋 Γ— π‘Œ)) β†’ (πΊβ€˜(2nd β€˜π‘’)) ∈ βˆͺ 𝑀)
4336, 42opelxpd 4659 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ (𝑋 Γ— π‘Œ)) β†’ ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩ ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))
446, 31hmeof1o 13779 . . . . . . . . . 10 (𝐹 ∈ (𝐽Homeo𝐿) β†’ 𝐹:𝑋–1-1-ontoβ†’βˆͺ 𝐿)
451, 44syl 14 . . . . . . . . 9 (πœ‘ β†’ 𝐹:𝑋–1-1-ontoβ†’βˆͺ 𝐿)
46 f1ocnv 5474 . . . . . . . . 9 (𝐹:𝑋–1-1-ontoβ†’βˆͺ 𝐿 β†’ ◑𝐹:βˆͺ 𝐿–1-1-onto→𝑋)
47 f1of 5461 . . . . . . . . 9 (◑𝐹:βˆͺ 𝐿–1-1-onto→𝑋 β†’ ◑𝐹:βˆͺ πΏβŸΆπ‘‹)
4845, 46, 473syl 17 . . . . . . . 8 (πœ‘ β†’ ◑𝐹:βˆͺ πΏβŸΆπ‘‹)
49 xp1st 6165 . . . . . . . 8 (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) β†’ (1st β€˜π‘£) ∈ βˆͺ 𝐿)
50 ffvelcdm 5649 . . . . . . . 8 ((◑𝐹:βˆͺ πΏβŸΆπ‘‹ ∧ (1st β€˜π‘£) ∈ βˆͺ 𝐿) β†’ (β—‘πΉβ€˜(1st β€˜π‘£)) ∈ 𝑋)
5148, 49, 50syl2an 289 . . . . . . 7 ((πœ‘ ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀)) β†’ (β—‘πΉβ€˜(1st β€˜π‘£)) ∈ 𝑋)
5214, 37hmeof1o 13779 . . . . . . . . . 10 (𝐺 ∈ (𝐾Homeo𝑀) β†’ 𝐺:π‘Œβ€“1-1-ontoβ†’βˆͺ 𝑀)
539, 52syl 14 . . . . . . . . 9 (πœ‘ β†’ 𝐺:π‘Œβ€“1-1-ontoβ†’βˆͺ 𝑀)
54 f1ocnv 5474 . . . . . . . . 9 (𝐺:π‘Œβ€“1-1-ontoβ†’βˆͺ 𝑀 β†’ ◑𝐺:βˆͺ 𝑀–1-1-ontoβ†’π‘Œ)
55 f1of 5461 . . . . . . . . 9 (◑𝐺:βˆͺ 𝑀–1-1-ontoβ†’π‘Œ β†’ ◑𝐺:βˆͺ π‘€βŸΆπ‘Œ)
5653, 54, 553syl 17 . . . . . . . 8 (πœ‘ β†’ ◑𝐺:βˆͺ π‘€βŸΆπ‘Œ)
57 xp2nd 6166 . . . . . . . 8 (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) β†’ (2nd β€˜π‘£) ∈ βˆͺ 𝑀)
58 ffvelcdm 5649 . . . . . . . 8 ((◑𝐺:βˆͺ π‘€βŸΆπ‘Œ ∧ (2nd β€˜π‘£) ∈ βˆͺ 𝑀) β†’ (β—‘πΊβ€˜(2nd β€˜π‘£)) ∈ π‘Œ)
5956, 57, 58syl2an 289 . . . . . . 7 ((πœ‘ ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀)) β†’ (β—‘πΊβ€˜(2nd β€˜π‘£)) ∈ π‘Œ)
6051, 59opelxpd 4659 . . . . . 6 ((πœ‘ ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀)) β†’ ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩ ∈ (𝑋 Γ— π‘Œ))
6145adantr 276 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ 𝐹:𝑋–1-1-ontoβ†’βˆͺ 𝐿)
6234ad2antrl 490 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (1st β€˜π‘’) ∈ 𝑋)
6349ad2antll 491 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (1st β€˜π‘£) ∈ βˆͺ 𝐿)
64 f1ocnvfvb 5780 . . . . . . . . . 10 ((𝐹:𝑋–1-1-ontoβ†’βˆͺ 𝐿 ∧ (1st β€˜π‘’) ∈ 𝑋 ∧ (1st β€˜π‘£) ∈ βˆͺ 𝐿) β†’ ((πΉβ€˜(1st β€˜π‘’)) = (1st β€˜π‘£) ↔ (β—‘πΉβ€˜(1st β€˜π‘£)) = (1st β€˜π‘’)))
6561, 62, 63, 64syl3anc 1238 . . . . . . . . 9 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ ((πΉβ€˜(1st β€˜π‘’)) = (1st β€˜π‘£) ↔ (β—‘πΉβ€˜(1st β€˜π‘£)) = (1st β€˜π‘’)))
66 eqcom 2179 . . . . . . . . 9 ((1st β€˜π‘£) = (πΉβ€˜(1st β€˜π‘’)) ↔ (πΉβ€˜(1st β€˜π‘’)) = (1st β€˜π‘£))
67 eqcom 2179 . . . . . . . . 9 ((1st β€˜π‘’) = (β—‘πΉβ€˜(1st β€˜π‘£)) ↔ (β—‘πΉβ€˜(1st β€˜π‘£)) = (1st β€˜π‘’))
6865, 66, 673bitr4g 223 . . . . . . . 8 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ ((1st β€˜π‘£) = (πΉβ€˜(1st β€˜π‘’)) ↔ (1st β€˜π‘’) = (β—‘πΉβ€˜(1st β€˜π‘£))))
6953adantr 276 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ 𝐺:π‘Œβ€“1-1-ontoβ†’βˆͺ 𝑀)
7040ad2antrl 490 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (2nd β€˜π‘’) ∈ π‘Œ)
7157ad2antll 491 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (2nd β€˜π‘£) ∈ βˆͺ 𝑀)
72 f1ocnvfvb 5780 . . . . . . . . . 10 ((𝐺:π‘Œβ€“1-1-ontoβ†’βˆͺ 𝑀 ∧ (2nd β€˜π‘’) ∈ π‘Œ ∧ (2nd β€˜π‘£) ∈ βˆͺ 𝑀) β†’ ((πΊβ€˜(2nd β€˜π‘’)) = (2nd β€˜π‘£) ↔ (β—‘πΊβ€˜(2nd β€˜π‘£)) = (2nd β€˜π‘’)))
7369, 70, 71, 72syl3anc 1238 . . . . . . . . 9 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ ((πΊβ€˜(2nd β€˜π‘’)) = (2nd β€˜π‘£) ↔ (β—‘πΊβ€˜(2nd β€˜π‘£)) = (2nd β€˜π‘’)))
74 eqcom 2179 . . . . . . . . 9 ((2nd β€˜π‘£) = (πΊβ€˜(2nd β€˜π‘’)) ↔ (πΊβ€˜(2nd β€˜π‘’)) = (2nd β€˜π‘£))
75 eqcom 2179 . . . . . . . . 9 ((2nd β€˜π‘’) = (β—‘πΊβ€˜(2nd β€˜π‘£)) ↔ (β—‘πΊβ€˜(2nd β€˜π‘£)) = (2nd β€˜π‘’))
7673, 74, 753bitr4g 223 . . . . . . . 8 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ ((2nd β€˜π‘£) = (πΊβ€˜(2nd β€˜π‘’)) ↔ (2nd β€˜π‘’) = (β—‘πΊβ€˜(2nd β€˜π‘£))))
7768, 76anbi12d 473 . . . . . . 7 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (((1st β€˜π‘£) = (πΉβ€˜(1st β€˜π‘’)) ∧ (2nd β€˜π‘£) = (πΊβ€˜(2nd β€˜π‘’))) ↔ ((1st β€˜π‘’) = (β—‘πΉβ€˜(1st β€˜π‘£)) ∧ (2nd β€˜π‘’) = (β—‘πΊβ€˜(2nd β€˜π‘£)))))
78 eqop 6177 . . . . . . . 8 (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) β†’ (𝑣 = ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩ ↔ ((1st β€˜π‘£) = (πΉβ€˜(1st β€˜π‘’)) ∧ (2nd β€˜π‘£) = (πΊβ€˜(2nd β€˜π‘’)))))
7978ad2antll 491 . . . . . . 7 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (𝑣 = ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩ ↔ ((1st β€˜π‘£) = (πΉβ€˜(1st β€˜π‘’)) ∧ (2nd β€˜π‘£) = (πΊβ€˜(2nd β€˜π‘’)))))
80 eqop 6177 . . . . . . . 8 (𝑒 ∈ (𝑋 Γ— π‘Œ) β†’ (𝑒 = ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩ ↔ ((1st β€˜π‘’) = (β—‘πΉβ€˜(1st β€˜π‘£)) ∧ (2nd β€˜π‘’) = (β—‘πΊβ€˜(2nd β€˜π‘£)))))
8180ad2antrl 490 . . . . . . 7 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (𝑒 = ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩ ↔ ((1st β€˜π‘’) = (β—‘πΉβ€˜(1st β€˜π‘£)) ∧ (2nd β€˜π‘’) = (β—‘πΊβ€˜(2nd β€˜π‘£)))))
8277, 79, 813bitr4rd 221 . . . . . 6 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (𝑒 = ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩ ↔ 𝑣 = ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩))
8330, 43, 60, 82f1ocnv2d 6074 . . . . 5 (πœ‘ β†’ ((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩):(𝑋 Γ— π‘Œ)–1-1-ontoβ†’(βˆͺ 𝐿 Γ— βˆͺ 𝑀) ∧ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) = (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) ↦ ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩)))
8483simprd 114 . . . 4 (πœ‘ β†’ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) = (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) ↦ ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩))
85 vex 2740 . . . . . . . 8 𝑧 ∈ V
86 vex 2740 . . . . . . . 8 𝑀 ∈ V
8785, 86op1std 6148 . . . . . . 7 (𝑣 = βŸ¨π‘§, π‘€βŸ© β†’ (1st β€˜π‘£) = 𝑧)
8887fveq2d 5519 . . . . . 6 (𝑣 = βŸ¨π‘§, π‘€βŸ© β†’ (β—‘πΉβ€˜(1st β€˜π‘£)) = (β—‘πΉβ€˜π‘§))
8985, 86op2ndd 6149 . . . . . . 7 (𝑣 = βŸ¨π‘§, π‘€βŸ© β†’ (2nd β€˜π‘£) = 𝑀)
9089fveq2d 5519 . . . . . 6 (𝑣 = βŸ¨π‘§, π‘€βŸ© β†’ (β—‘πΊβ€˜(2nd β€˜π‘£)) = (β—‘πΊβ€˜π‘€))
9188, 90opeq12d 3786 . . . . 5 (𝑣 = βŸ¨π‘§, π‘€βŸ© β†’ ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩ = ⟨(β—‘πΉβ€˜π‘§), (β—‘πΊβ€˜π‘€)⟩)
9291mpompt 5966 . . . 4 (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) ↦ ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩) = (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ ⟨(β—‘πΉβ€˜π‘§), (β—‘πΊβ€˜π‘€)⟩)
9384, 92eqtrdi 2226 . . 3 (πœ‘ β†’ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) = (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ ⟨(β—‘πΉβ€˜π‘§), (β—‘πΊβ€˜π‘€)⟩))
94 cntop2 13672 . . . . . 6 (𝐹 ∈ (𝐽 Cn 𝐿) β†’ 𝐿 ∈ Top)
953, 94syl 14 . . . . 5 (πœ‘ β†’ 𝐿 ∈ Top)
9631toptopon 13488 . . . . 5 (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿))
9795, 96sylib 122 . . . 4 (πœ‘ β†’ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿))
98 cntop2 13672 . . . . . 6 (𝐺 ∈ (𝐾 Cn 𝑀) β†’ 𝑀 ∈ Top)
9911, 98syl 14 . . . . 5 (πœ‘ β†’ 𝑀 ∈ Top)
10037toptopon 13488 . . . . 5 (𝑀 ∈ Top ↔ 𝑀 ∈ (TopOnβ€˜βˆͺ 𝑀))
10199, 100sylib 122 . . . 4 (πœ‘ β†’ 𝑀 ∈ (TopOnβ€˜βˆͺ 𝑀))
10297, 101cnmpt1st 13758 . . . . 5 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ 𝑧) ∈ ((𝐿 Γ—t 𝑀) Cn 𝐿))
103 hmeocnvcn 13776 . . . . . 6 (𝐹 ∈ (𝐽Homeo𝐿) β†’ ◑𝐹 ∈ (𝐿 Cn 𝐽))
1041, 103syl 14 . . . . 5 (πœ‘ β†’ ◑𝐹 ∈ (𝐿 Cn 𝐽))
10597, 101, 102, 104cnmpt21f 13762 . . . 4 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ (β—‘πΉβ€˜π‘§)) ∈ ((𝐿 Γ—t 𝑀) Cn 𝐽))
10697, 101cnmpt2nd 13759 . . . . 5 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ 𝑀) ∈ ((𝐿 Γ—t 𝑀) Cn 𝑀))
107 hmeocnvcn 13776 . . . . . 6 (𝐺 ∈ (𝐾Homeo𝑀) β†’ ◑𝐺 ∈ (𝑀 Cn 𝐾))
1089, 107syl 14 . . . . 5 (πœ‘ β†’ ◑𝐺 ∈ (𝑀 Cn 𝐾))
10997, 101, 106, 108cnmpt21f 13762 . . . 4 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ (β—‘πΊβ€˜π‘€)) ∈ ((𝐿 Γ—t 𝑀) Cn 𝐾))
11097, 101, 105, 109cnmpt2t 13763 . . 3 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ ⟨(β—‘πΉβ€˜π‘§), (β—‘πΊβ€˜π‘€)⟩) ∈ ((𝐿 Γ—t 𝑀) Cn (𝐽 Γ—t 𝐾)))
11193, 110eqeltrd 2254 . 2 (πœ‘ β†’ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) ∈ ((𝐿 Γ—t 𝑀) Cn (𝐽 Γ—t 𝐾)))
112 ishmeo 13774 . 2 ((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) ∈ ((𝐽 Γ—t 𝐾)Homeo(𝐿 Γ—t 𝑀)) ↔ ((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) ∈ ((𝐽 Γ—t 𝐾) Cn (𝐿 Γ—t 𝑀)) ∧ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) ∈ ((𝐿 Γ—t 𝑀) Cn (𝐽 Γ—t 𝐾))))
11321, 111, 112sylanbrc 417 1 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) ∈ ((𝐽 Γ—t 𝐾)Homeo(𝐿 Γ—t 𝑀)))
Colors of variables: wff set class
Syntax hints:   β†’ wi 4   ∧ wa 104   ↔ wb 105   = wceq 1353   ∈ wcel 2148  βŸ¨cop 3595  βˆͺ cuni 3809   ↦ cmpt 4064   Γ— cxp 4624  β—‘ccnv 4625  βŸΆwf 5212  β€“1-1-ontoβ†’wf1o 5215  β€˜cfv 5216  (class class class)co 5874   ∈ cmpo 5876  1st c1st 6138  2nd c2nd 6139  Topctop 13467  TopOnctopon 13480   Cn ccn 13655   Γ—t ctx 13722  Homeochmeo 13770
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4118  ax-sep 4121  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-iun 3888  df-br 4004  df-opab 4065  df-mpt 4066  df-id 4293  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-res 4638  df-ima 4639  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-f1 5221  df-fo 5222  df-f1o 5223  df-fv 5224  df-ov 5877  df-oprab 5878  df-mpo 5879  df-1st 6140  df-2nd 6141  df-map 6649  df-topgen 12708  df-top 13468  df-topon 13481  df-bases 13513  df-cn 13658  df-tx 13723  df-hmeo 13771
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator