ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  txhmeo GIF version
Theorem txhmeo 13980
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 13966 . . . . . 6 (𝐹 ∈ (𝐽Homeo𝐿) β†’ 𝐹 ∈ (𝐽 Cn 𝐿))
31, 2syl 14 . . . . 5 (πœ‘ β†’ 𝐹 ∈ (𝐽 Cn 𝐿))
4 cntop1 13862 . . . . 5 (𝐹 ∈ (𝐽 Cn 𝐿) β†’ 𝐽 ∈ Top)
53, 4syl 14 . . . 4 (πœ‘ β†’ 𝐽 ∈ Top)
6 txhmeo.1 . . . . 5 𝑋 = βˆͺ 𝐽
76toptopon 13679 . . . 4 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOnβ€˜π‘‹))
85, 7sylib 122 . . 3 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
9 txhmeo.4 . . . . . 6 (πœ‘ β†’ 𝐺 ∈ (𝐾Homeo𝑀))
10 hmeocn 13966 . . . . . 6 (𝐺 ∈ (𝐾Homeo𝑀) β†’ 𝐺 ∈ (𝐾 Cn 𝑀))
119, 10syl 14 . . . . 5 (πœ‘ β†’ 𝐺 ∈ (𝐾 Cn 𝑀))
12 cntop1 13862 . . . . 5 (𝐺 ∈ (𝐾 Cn 𝑀) β†’ 𝐾 ∈ Top)
1311, 12syl 14 . . . 4 (πœ‘ β†’ 𝐾 ∈ Top)
14 txhmeo.2 . . . . 5 π‘Œ = βˆͺ 𝐾
1514toptopon 13679 . . . 4 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOnβ€˜π‘Œ))
1613, 15sylib 122 . . 3 (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜π‘Œ))
178, 16cnmpt1st 13949 . . . 4 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ π‘₯) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐽))
188, 16, 17, 3cnmpt21f 13953 . . 3 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ (πΉβ€˜π‘₯)) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿))
198, 16cnmpt2nd 13950 . . . 4 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ 𝑦) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐾))
208, 16, 19, 11cnmpt21f 13953 . . 3 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ (πΊβ€˜π‘¦)) ∈ ((𝐽 Γ—t 𝐾) Cn 𝑀))
218, 16, 18, 20cnmpt2t 13954 . 2 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) ∈ ((𝐽 Γ—t 𝐾) Cn (𝐿 Γ—t 𝑀)))
22 vex 2742 . . . . . . . . . . 11 π‘₯ ∈ V
23 vex 2742 . . . . . . . . . . 11 𝑦 ∈ V
2422, 23op1std 6152 . . . . . . . . . 10 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ (1st β€˜π‘’) = π‘₯)
2524fveq2d 5521 . . . . . . . . 9 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ (πΉβ€˜(1st β€˜π‘’)) = (πΉβ€˜π‘₯))
2622, 23op2ndd 6153 . . . . . . . . . 10 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ (2nd β€˜π‘’) = 𝑦)
2726fveq2d 5521 . . . . . . . . 9 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ (πΊβ€˜(2nd β€˜π‘’)) = (πΊβ€˜π‘¦))
2825, 27opeq12d 3788 . . . . . . . 8 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩ = ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩)
2928mpompt 5970 . . . . . . 7 (𝑒 ∈ (𝑋 Γ— π‘Œ) ↦ ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩) = (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩)
3029eqcomi 2181 . . . . . 6 (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) = (𝑒 ∈ (𝑋 Γ— π‘Œ) ↦ ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩)
31 eqid 2177 . . . . . . . . . 10 βˆͺ 𝐿 = βˆͺ 𝐿
326, 31cnf 13865 . . . . . . . . 9 (𝐹 ∈ (𝐽 Cn 𝐿) β†’ 𝐹:π‘‹βŸΆβˆͺ 𝐿)
333, 32syl 14 . . . . . . . 8 (πœ‘ β†’ 𝐹:π‘‹βŸΆβˆͺ 𝐿)
34 xp1st 6169 . . . . . . . 8 (𝑒 ∈ (𝑋 Γ— π‘Œ) β†’ (1st β€˜π‘’) ∈ 𝑋)
35 ffvelcdm 5652 . . . . . . . 8 ((𝐹:π‘‹βŸΆβˆͺ 𝐿 ∧ (1st β€˜π‘’) ∈ 𝑋) β†’ (πΉβ€˜(1st β€˜π‘’)) ∈ βˆͺ 𝐿)
3633, 34, 35syl2an 289 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ (𝑋 Γ— π‘Œ)) β†’ (πΉβ€˜(1st β€˜π‘’)) ∈ βˆͺ 𝐿)
37 eqid 2177 . . . . . . . . . 10 βˆͺ 𝑀 = βˆͺ 𝑀
3814, 37cnf 13865 . . . . . . . . 9 (𝐺 ∈ (𝐾 Cn 𝑀) β†’ 𝐺:π‘ŒβŸΆβˆͺ 𝑀)
3911, 38syl 14 . . . . . . . 8 (πœ‘ β†’ 𝐺:π‘ŒβŸΆβˆͺ 𝑀)
40 xp2nd 6170 . . . . . . . 8 (𝑒 ∈ (𝑋 Γ— π‘Œ) β†’ (2nd β€˜π‘’) ∈ π‘Œ)
41 ffvelcdm 5652 . . . . . . . 8 ((𝐺:π‘ŒβŸΆβˆͺ 𝑀 ∧ (2nd β€˜π‘’) ∈ π‘Œ) β†’ (πΊβ€˜(2nd β€˜π‘’)) ∈ βˆͺ 𝑀)
4239, 40, 41syl2an 289 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ (𝑋 Γ— π‘Œ)) β†’ (πΊβ€˜(2nd β€˜π‘’)) ∈ βˆͺ 𝑀)
4336, 42opelxpd 4661 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ (𝑋 Γ— π‘Œ)) β†’ ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩ ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))
446, 31hmeof1o 13970 . . . . . . . . . 10 (𝐹 ∈ (𝐽Homeo𝐿) β†’ 𝐹:𝑋–1-1-ontoβ†’βˆͺ 𝐿)
451, 44syl 14 . . . . . . . . 9 (πœ‘ β†’ 𝐹:𝑋–1-1-ontoβ†’βˆͺ 𝐿)
46 f1ocnv 5476 . . . . . . . . 9 (𝐹:𝑋–1-1-ontoβ†’βˆͺ 𝐿 β†’ ◑𝐹:βˆͺ 𝐿–1-1-onto→𝑋)
47 f1of 5463 . . . . . . . . 9 (◑𝐹:βˆͺ 𝐿–1-1-onto→𝑋 β†’ ◑𝐹:βˆͺ πΏβŸΆπ‘‹)
4845, 46, 473syl 17 . . . . . . . 8 (πœ‘ β†’ ◑𝐹:βˆͺ πΏβŸΆπ‘‹)
49 xp1st 6169 . . . . . . . 8 (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) β†’ (1st β€˜π‘£) ∈ βˆͺ 𝐿)
50 ffvelcdm 5652 . . . . . . . 8 ((◑𝐹:βˆͺ πΏβŸΆπ‘‹ ∧ (1st β€˜π‘£) ∈ βˆͺ 𝐿) β†’ (β—‘πΉβ€˜(1st β€˜π‘£)) ∈ 𝑋)
5148, 49, 50syl2an 289 . . . . . . 7 ((πœ‘ ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀)) β†’ (β—‘πΉβ€˜(1st β€˜π‘£)) ∈ 𝑋)
5214, 37hmeof1o 13970 . . . . . . . . . 10 (𝐺 ∈ (𝐾Homeo𝑀) β†’ 𝐺:π‘Œβ€“1-1-ontoβ†’βˆͺ 𝑀)
539, 52syl 14 . . . . . . . . 9 (πœ‘ β†’ 𝐺:π‘Œβ€“1-1-ontoβ†’βˆͺ 𝑀)
54 f1ocnv 5476 . . . . . . . . 9 (𝐺:π‘Œβ€“1-1-ontoβ†’βˆͺ 𝑀 β†’ ◑𝐺:βˆͺ 𝑀–1-1-ontoβ†’π‘Œ)
55 f1of 5463 . . . . . . . . 9 (◑𝐺:βˆͺ 𝑀–1-1-ontoβ†’π‘Œ β†’ ◑𝐺:βˆͺ π‘€βŸΆπ‘Œ)
5653, 54, 553syl 17 . . . . . . . 8 (πœ‘ β†’ ◑𝐺:βˆͺ π‘€βŸΆπ‘Œ)
57 xp2nd 6170 . . . . . . . 8 (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) β†’ (2nd β€˜π‘£) ∈ βˆͺ 𝑀)
58 ffvelcdm 5652 . . . . . . . 8 ((◑𝐺:βˆͺ π‘€βŸΆπ‘Œ ∧ (2nd β€˜π‘£) ∈ βˆͺ 𝑀) β†’ (β—‘πΊβ€˜(2nd β€˜π‘£)) ∈ π‘Œ)
5956, 57, 58syl2an 289 . . . . . . 7 ((πœ‘ ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀)) β†’ (β—‘πΊβ€˜(2nd β€˜π‘£)) ∈ π‘Œ)
6051, 59opelxpd 4661 . . . . . 6 ((πœ‘ ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀)) β†’ ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩ ∈ (𝑋 Γ— π‘Œ))
6145adantr 276 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ 𝐹:𝑋–1-1-ontoβ†’βˆͺ 𝐿)
6234ad2antrl 490 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (1st β€˜π‘’) ∈ 𝑋)
6349ad2antll 491 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (1st β€˜π‘£) ∈ βˆͺ 𝐿)
64 f1ocnvfvb 5784 . . . . . . . . . 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 5784 . . . . . . . . . 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 6181 . . . . . . . 8 (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) β†’ (𝑣 = ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩ ↔ ((1st β€˜π‘£) = (πΉβ€˜(1st β€˜π‘’)) ∧ (2nd β€˜π‘£) = (πΊβ€˜(2nd β€˜π‘’)))))
7978ad2antll 491 . . . . . . 7 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (𝑣 = ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩ ↔ ((1st β€˜π‘£) = (πΉβ€˜(1st β€˜π‘’)) ∧ (2nd β€˜π‘£) = (πΊβ€˜(2nd β€˜π‘’)))))
80 eqop 6181 . . . . . . . 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 6078 . . . . 5 (πœ‘ β†’ ((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩):(𝑋 Γ— π‘Œ)–1-1-ontoβ†’(βˆͺ 𝐿 Γ— βˆͺ 𝑀) ∧ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) = (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) ↦ ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩)))
8483simprd 114 . . . 4 (πœ‘ β†’ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) = (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) ↦ ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩))
85 vex 2742 . . . . . . . 8 𝑧 ∈ V
86 vex 2742 . . . . . . . 8 𝑀 ∈ V
8785, 86op1std 6152 . . . . . . 7 (𝑣 = βŸ¨π‘§, π‘€βŸ© β†’ (1st β€˜π‘£) = 𝑧)
8887fveq2d 5521 . . . . . 6 (𝑣 = βŸ¨π‘§, π‘€βŸ© β†’ (β—‘πΉβ€˜(1st β€˜π‘£)) = (β—‘πΉβ€˜π‘§))
8985, 86op2ndd 6153 . . . . . . 7 (𝑣 = βŸ¨π‘§, π‘€βŸ© β†’ (2nd β€˜π‘£) = 𝑀)
9089fveq2d 5521 . . . . . 6 (𝑣 = βŸ¨π‘§, π‘€βŸ© β†’ (β—‘πΊβ€˜(2nd β€˜π‘£)) = (β—‘πΊβ€˜π‘€))
9188, 90opeq12d 3788 . . . . 5 (𝑣 = βŸ¨π‘§, π‘€βŸ© β†’ ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩ = ⟨(β—‘πΉβ€˜π‘§), (β—‘πΊβ€˜π‘€)⟩)
9291mpompt 5970 . . . 4 (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) ↦ ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩) = (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ ⟨(β—‘πΉβ€˜π‘§), (β—‘πΊβ€˜π‘€)⟩)
9384, 92eqtrdi 2226 . . 3 (πœ‘ β†’ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) = (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ ⟨(β—‘πΉβ€˜π‘§), (β—‘πΊβ€˜π‘€)⟩))
94 cntop2 13863 . . . . . 6 (𝐹 ∈ (𝐽 Cn 𝐿) β†’ 𝐿 ∈ Top)
953, 94syl 14 . . . . 5 (πœ‘ β†’ 𝐿 ∈ Top)
9631toptopon 13679 . . . . 5 (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿))
9795, 96sylib 122 . . . 4 (πœ‘ β†’ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿))
98 cntop2 13863 . . . . . 6 (𝐺 ∈ (𝐾 Cn 𝑀) β†’ 𝑀 ∈ Top)
9911, 98syl 14 . . . . 5 (πœ‘ β†’ 𝑀 ∈ Top)
10037toptopon 13679 . . . . 5 (𝑀 ∈ Top ↔ 𝑀 ∈ (TopOnβ€˜βˆͺ 𝑀))
10199, 100sylib 122 . . . 4 (πœ‘ β†’ 𝑀 ∈ (TopOnβ€˜βˆͺ 𝑀))
10297, 101cnmpt1st 13949 . . . . 5 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ 𝑧) ∈ ((𝐿 Γ—t 𝑀) Cn 𝐿))
103 hmeocnvcn 13967 . . . . . 6 (𝐹 ∈ (𝐽Homeo𝐿) β†’ ◑𝐹 ∈ (𝐿 Cn 𝐽))
1041, 103syl 14 . . . . 5 (πœ‘ β†’ ◑𝐹 ∈ (𝐿 Cn 𝐽))
10597, 101, 102, 104cnmpt21f 13953 . . . 4 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ (β—‘πΉβ€˜π‘§)) ∈ ((𝐿 Γ—t 𝑀) Cn 𝐽))
10697, 101cnmpt2nd 13950 . . . . 5 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ 𝑀) ∈ ((𝐿 Γ—t 𝑀) Cn 𝑀))
107 hmeocnvcn 13967 . . . . . 6 (𝐺 ∈ (𝐾Homeo𝑀) β†’ ◑𝐺 ∈ (𝑀 Cn 𝐾))
1089, 107syl 14 . . . . 5 (πœ‘ β†’ ◑𝐺 ∈ (𝑀 Cn 𝐾))
10997, 101, 106, 108cnmpt21f 13953 . . . 4 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ (β—‘πΊβ€˜π‘€)) ∈ ((𝐿 Γ—t 𝑀) Cn 𝐾))
11097, 101, 105, 109cnmpt2t 13954 . . 3 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ ⟨(β—‘πΉβ€˜π‘§), (β—‘πΊβ€˜π‘€)⟩) ∈ ((𝐿 Γ—t 𝑀) Cn (𝐽 Γ—t 𝐾)))
11193, 110eqeltrd 2254 . 2 (πœ‘ β†’ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) ∈ ((𝐿 Γ—t 𝑀) Cn (𝐽 Γ—t 𝐾)))
112 ishmeo 13965 . 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 3597  βˆͺ cuni 3811   ↦ cmpt 4066   Γ— cxp 4626  β—‘ccnv 4627  βŸΆwf 5214  β€“1-1-ontoβ†’wf1o 5217  β€˜cfv 5218  (class class class)co 5878   ∈ cmpo 5880  1st c1st 6142  2nd c2nd 6143  Topctop 13658  TopOnctopon 13671   Cn ccn 13846   Γ—t ctx 13913  Homeochmeo 13961
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 4120  ax-sep 4123  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538
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 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-id 4295  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-ov 5881  df-oprab 5882  df-mpo 5883  df-1st 6144  df-2nd 6145  df-map 6653  df-topgen 12715  df-top 13659  df-topon 13672  df-bases 13704  df-cn 13849  df-tx 13914  df-hmeo 13962
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator