ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  txhmeo GIF version
Theorem txhmeo 14115
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 14101 . . . . . 6 (𝐹 ∈ (𝐽Homeo𝐿) β†’ 𝐹 ∈ (𝐽 Cn 𝐿))
31, 2syl 14 . . . . 5 (πœ‘ β†’ 𝐹 ∈ (𝐽 Cn 𝐿))
4 cntop1 13997 . . . . 5 (𝐹 ∈ (𝐽 Cn 𝐿) β†’ 𝐽 ∈ Top)
53, 4syl 14 . . . 4 (πœ‘ β†’ 𝐽 ∈ Top)
6 txhmeo.1 . . . . 5 𝑋 = βˆͺ 𝐽
76toptopon 13814 . . . 4 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOnβ€˜π‘‹))
85, 7sylib 122 . . 3 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
9 txhmeo.4 . . . . . 6 (πœ‘ β†’ 𝐺 ∈ (𝐾Homeo𝑀))
10 hmeocn 14101 . . . . . 6 (𝐺 ∈ (𝐾Homeo𝑀) β†’ 𝐺 ∈ (𝐾 Cn 𝑀))
119, 10syl 14 . . . . 5 (πœ‘ β†’ 𝐺 ∈ (𝐾 Cn 𝑀))
12 cntop1 13997 . . . . 5 (𝐺 ∈ (𝐾 Cn 𝑀) β†’ 𝐾 ∈ Top)
1311, 12syl 14 . . . 4 (πœ‘ β†’ 𝐾 ∈ Top)
14 txhmeo.2 . . . . 5 π‘Œ = βˆͺ 𝐾
1514toptopon 13814 . . . 4 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOnβ€˜π‘Œ))
1613, 15sylib 122 . . 3 (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜π‘Œ))
178, 16cnmpt1st 14084 . . . 4 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ π‘₯) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐽))
188, 16, 17, 3cnmpt21f 14088 . . 3 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ (πΉβ€˜π‘₯)) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿))
198, 16cnmpt2nd 14085 . . . 4 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ 𝑦) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐾))
208, 16, 19, 11cnmpt21f 14088 . . 3 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ (πΊβ€˜π‘¦)) ∈ ((𝐽 Γ—t 𝐾) Cn 𝑀))
218, 16, 18, 20cnmpt2t 14089 . 2 (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) ∈ ((𝐽 Γ—t 𝐾) Cn (𝐿 Γ—t 𝑀)))
22 vex 2752 . . . . . . . . . . 11 π‘₯ ∈ V
23 vex 2752 . . . . . . . . . . 11 𝑦 ∈ V
2422, 23op1std 6163 . . . . . . . . . 10 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ (1st β€˜π‘’) = π‘₯)
2524fveq2d 5531 . . . . . . . . 9 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ (πΉβ€˜(1st β€˜π‘’)) = (πΉβ€˜π‘₯))
2622, 23op2ndd 6164 . . . . . . . . . 10 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ (2nd β€˜π‘’) = 𝑦)
2726fveq2d 5531 . . . . . . . . 9 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ (πΊβ€˜(2nd β€˜π‘’)) = (πΊβ€˜π‘¦))
2825, 27opeq12d 3798 . . . . . . . 8 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩ = ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩)
2928mpompt 5980 . . . . . . 7 (𝑒 ∈ (𝑋 Γ— π‘Œ) ↦ ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩) = (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩)
3029eqcomi 2191 . . . . . 6 (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) = (𝑒 ∈ (𝑋 Γ— π‘Œ) ↦ ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩)
31 eqid 2187 . . . . . . . . . 10 βˆͺ 𝐿 = βˆͺ 𝐿
326, 31cnf 14000 . . . . . . . . 9 (𝐹 ∈ (𝐽 Cn 𝐿) β†’ 𝐹:π‘‹βŸΆβˆͺ 𝐿)
333, 32syl 14 . . . . . . . 8 (πœ‘ β†’ 𝐹:π‘‹βŸΆβˆͺ 𝐿)
34 xp1st 6180 . . . . . . . 8 (𝑒 ∈ (𝑋 Γ— π‘Œ) β†’ (1st β€˜π‘’) ∈ 𝑋)
35 ffvelcdm 5662 . . . . . . . 8 ((𝐹:π‘‹βŸΆβˆͺ 𝐿 ∧ (1st β€˜π‘’) ∈ 𝑋) β†’ (πΉβ€˜(1st β€˜π‘’)) ∈ βˆͺ 𝐿)
3633, 34, 35syl2an 289 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ (𝑋 Γ— π‘Œ)) β†’ (πΉβ€˜(1st β€˜π‘’)) ∈ βˆͺ 𝐿)
37 eqid 2187 . . . . . . . . . 10 βˆͺ 𝑀 = βˆͺ 𝑀
3814, 37cnf 14000 . . . . . . . . 9 (𝐺 ∈ (𝐾 Cn 𝑀) β†’ 𝐺:π‘ŒβŸΆβˆͺ 𝑀)
3911, 38syl 14 . . . . . . . 8 (πœ‘ β†’ 𝐺:π‘ŒβŸΆβˆͺ 𝑀)
40 xp2nd 6181 . . . . . . . 8 (𝑒 ∈ (𝑋 Γ— π‘Œ) β†’ (2nd β€˜π‘’) ∈ π‘Œ)
41 ffvelcdm 5662 . . . . . . . 8 ((𝐺:π‘ŒβŸΆβˆͺ 𝑀 ∧ (2nd β€˜π‘’) ∈ π‘Œ) β†’ (πΊβ€˜(2nd β€˜π‘’)) ∈ βˆͺ 𝑀)
4239, 40, 41syl2an 289 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ (𝑋 Γ— π‘Œ)) β†’ (πΊβ€˜(2nd β€˜π‘’)) ∈ βˆͺ 𝑀)
4336, 42opelxpd 4671 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ (𝑋 Γ— π‘Œ)) β†’ ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩ ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))
446, 31hmeof1o 14105 . . . . . . . . . 10 (𝐹 ∈ (𝐽Homeo𝐿) β†’ 𝐹:𝑋–1-1-ontoβ†’βˆͺ 𝐿)
451, 44syl 14 . . . . . . . . 9 (πœ‘ β†’ 𝐹:𝑋–1-1-ontoβ†’βˆͺ 𝐿)
46 f1ocnv 5486 . . . . . . . . 9 (𝐹:𝑋–1-1-ontoβ†’βˆͺ 𝐿 β†’ ◑𝐹:βˆͺ 𝐿–1-1-onto→𝑋)
47 f1of 5473 . . . . . . . . 9 (◑𝐹:βˆͺ 𝐿–1-1-onto→𝑋 β†’ ◑𝐹:βˆͺ πΏβŸΆπ‘‹)
4845, 46, 473syl 17 . . . . . . . 8 (πœ‘ β†’ ◑𝐹:βˆͺ πΏβŸΆπ‘‹)
49 xp1st 6180 . . . . . . . 8 (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) β†’ (1st β€˜π‘£) ∈ βˆͺ 𝐿)
50 ffvelcdm 5662 . . . . . . . 8 ((◑𝐹:βˆͺ πΏβŸΆπ‘‹ ∧ (1st β€˜π‘£) ∈ βˆͺ 𝐿) β†’ (β—‘πΉβ€˜(1st β€˜π‘£)) ∈ 𝑋)
5148, 49, 50syl2an 289 . . . . . . 7 ((πœ‘ ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀)) β†’ (β—‘πΉβ€˜(1st β€˜π‘£)) ∈ 𝑋)
5214, 37hmeof1o 14105 . . . . . . . . . 10 (𝐺 ∈ (𝐾Homeo𝑀) β†’ 𝐺:π‘Œβ€“1-1-ontoβ†’βˆͺ 𝑀)
539, 52syl 14 . . . . . . . . 9 (πœ‘ β†’ 𝐺:π‘Œβ€“1-1-ontoβ†’βˆͺ 𝑀)
54 f1ocnv 5486 . . . . . . . . 9 (𝐺:π‘Œβ€“1-1-ontoβ†’βˆͺ 𝑀 β†’ ◑𝐺:βˆͺ 𝑀–1-1-ontoβ†’π‘Œ)
55 f1of 5473 . . . . . . . . 9 (◑𝐺:βˆͺ 𝑀–1-1-ontoβ†’π‘Œ β†’ ◑𝐺:βˆͺ π‘€βŸΆπ‘Œ)
5653, 54, 553syl 17 . . . . . . . 8 (πœ‘ β†’ ◑𝐺:βˆͺ π‘€βŸΆπ‘Œ)
57 xp2nd 6181 . . . . . . . 8 (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) β†’ (2nd β€˜π‘£) ∈ βˆͺ 𝑀)
58 ffvelcdm 5662 . . . . . . . 8 ((◑𝐺:βˆͺ π‘€βŸΆπ‘Œ ∧ (2nd β€˜π‘£) ∈ βˆͺ 𝑀) β†’ (β—‘πΊβ€˜(2nd β€˜π‘£)) ∈ π‘Œ)
5956, 57, 58syl2an 289 . . . . . . 7 ((πœ‘ ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀)) β†’ (β—‘πΊβ€˜(2nd β€˜π‘£)) ∈ π‘Œ)
6051, 59opelxpd 4671 . . . . . 6 ((πœ‘ ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀)) β†’ ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩ ∈ (𝑋 Γ— π‘Œ))
6145adantr 276 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ 𝐹:𝑋–1-1-ontoβ†’βˆͺ 𝐿)
6234ad2antrl 490 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (1st β€˜π‘’) ∈ 𝑋)
6349ad2antll 491 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (1st β€˜π‘£) ∈ βˆͺ 𝐿)
64 f1ocnvfvb 5794 . . . . . . . . . 10 ((𝐹:𝑋–1-1-ontoβ†’βˆͺ 𝐿 ∧ (1st β€˜π‘’) ∈ 𝑋 ∧ (1st β€˜π‘£) ∈ βˆͺ 𝐿) β†’ ((πΉβ€˜(1st β€˜π‘’)) = (1st β€˜π‘£) ↔ (β—‘πΉβ€˜(1st β€˜π‘£)) = (1st β€˜π‘’)))
6561, 62, 63, 64syl3anc 1248 . . . . . . . . 9 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ ((πΉβ€˜(1st β€˜π‘’)) = (1st β€˜π‘£) ↔ (β—‘πΉβ€˜(1st β€˜π‘£)) = (1st β€˜π‘’)))
66 eqcom 2189 . . . . . . . . 9 ((1st β€˜π‘£) = (πΉβ€˜(1st β€˜π‘’)) ↔ (πΉβ€˜(1st β€˜π‘’)) = (1st β€˜π‘£))
67 eqcom 2189 . . . . . . . . 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 5794 . . . . . . . . . 10 ((𝐺:π‘Œβ€“1-1-ontoβ†’βˆͺ 𝑀 ∧ (2nd β€˜π‘’) ∈ π‘Œ ∧ (2nd β€˜π‘£) ∈ βˆͺ 𝑀) β†’ ((πΊβ€˜(2nd β€˜π‘’)) = (2nd β€˜π‘£) ↔ (β—‘πΊβ€˜(2nd β€˜π‘£)) = (2nd β€˜π‘’)))
7369, 70, 71, 72syl3anc 1248 . . . . . . . . 9 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ ((πΊβ€˜(2nd β€˜π‘’)) = (2nd β€˜π‘£) ↔ (β—‘πΊβ€˜(2nd β€˜π‘£)) = (2nd β€˜π‘’)))
74 eqcom 2189 . . . . . . . . 9 ((2nd β€˜π‘£) = (πΊβ€˜(2nd β€˜π‘’)) ↔ (πΊβ€˜(2nd β€˜π‘’)) = (2nd β€˜π‘£))
75 eqcom 2189 . . . . . . . . 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 6192 . . . . . . . 8 (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) β†’ (𝑣 = ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩ ↔ ((1st β€˜π‘£) = (πΉβ€˜(1st β€˜π‘’)) ∧ (2nd β€˜π‘£) = (πΊβ€˜(2nd β€˜π‘’)))))
7978ad2antll 491 . . . . . . 7 ((πœ‘ ∧ (𝑒 ∈ (𝑋 Γ— π‘Œ) ∧ 𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀))) β†’ (𝑣 = ⟨(πΉβ€˜(1st β€˜π‘’)), (πΊβ€˜(2nd β€˜π‘’))⟩ ↔ ((1st β€˜π‘£) = (πΉβ€˜(1st β€˜π‘’)) ∧ (2nd β€˜π‘£) = (πΊβ€˜(2nd β€˜π‘’)))))
80 eqop 6192 . . . . . . . 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 6089 . . . . 5 (πœ‘ β†’ ((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩):(𝑋 Γ— π‘Œ)–1-1-ontoβ†’(βˆͺ 𝐿 Γ— βˆͺ 𝑀) ∧ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) = (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) ↦ ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩)))
8483simprd 114 . . . 4 (πœ‘ β†’ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) = (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) ↦ ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩))
85 vex 2752 . . . . . . . 8 𝑧 ∈ V
86 vex 2752 . . . . . . . 8 𝑀 ∈ V
8785, 86op1std 6163 . . . . . . 7 (𝑣 = βŸ¨π‘§, π‘€βŸ© β†’ (1st β€˜π‘£) = 𝑧)
8887fveq2d 5531 . . . . . 6 (𝑣 = βŸ¨π‘§, π‘€βŸ© β†’ (β—‘πΉβ€˜(1st β€˜π‘£)) = (β—‘πΉβ€˜π‘§))
8985, 86op2ndd 6164 . . . . . . 7 (𝑣 = βŸ¨π‘§, π‘€βŸ© β†’ (2nd β€˜π‘£) = 𝑀)
9089fveq2d 5531 . . . . . 6 (𝑣 = βŸ¨π‘§, π‘€βŸ© β†’ (β—‘πΊβ€˜(2nd β€˜π‘£)) = (β—‘πΊβ€˜π‘€))
9188, 90opeq12d 3798 . . . . 5 (𝑣 = βŸ¨π‘§, π‘€βŸ© β†’ ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩ = ⟨(β—‘πΉβ€˜π‘§), (β—‘πΊβ€˜π‘€)⟩)
9291mpompt 5980 . . . 4 (𝑣 ∈ (βˆͺ 𝐿 Γ— βˆͺ 𝑀) ↦ ⟨(β—‘πΉβ€˜(1st β€˜π‘£)), (β—‘πΊβ€˜(2nd β€˜π‘£))⟩) = (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ ⟨(β—‘πΉβ€˜π‘§), (β—‘πΊβ€˜π‘€)⟩)
9384, 92eqtrdi 2236 . . 3 (πœ‘ β†’ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) = (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ ⟨(β—‘πΉβ€˜π‘§), (β—‘πΊβ€˜π‘€)⟩))
94 cntop2 13998 . . . . . 6 (𝐹 ∈ (𝐽 Cn 𝐿) β†’ 𝐿 ∈ Top)
953, 94syl 14 . . . . 5 (πœ‘ β†’ 𝐿 ∈ Top)
9631toptopon 13814 . . . . 5 (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿))
9795, 96sylib 122 . . . 4 (πœ‘ β†’ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿))
98 cntop2 13998 . . . . . 6 (𝐺 ∈ (𝐾 Cn 𝑀) β†’ 𝑀 ∈ Top)
9911, 98syl 14 . . . . 5 (πœ‘ β†’ 𝑀 ∈ Top)
10037toptopon 13814 . . . . 5 (𝑀 ∈ Top ↔ 𝑀 ∈ (TopOnβ€˜βˆͺ 𝑀))
10199, 100sylib 122 . . . 4 (πœ‘ β†’ 𝑀 ∈ (TopOnβ€˜βˆͺ 𝑀))
10297, 101cnmpt1st 14084 . . . . 5 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ 𝑧) ∈ ((𝐿 Γ—t 𝑀) Cn 𝐿))
103 hmeocnvcn 14102 . . . . . 6 (𝐹 ∈ (𝐽Homeo𝐿) β†’ ◑𝐹 ∈ (𝐿 Cn 𝐽))
1041, 103syl 14 . . . . 5 (πœ‘ β†’ ◑𝐹 ∈ (𝐿 Cn 𝐽))
10597, 101, 102, 104cnmpt21f 14088 . . . 4 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ (β—‘πΉβ€˜π‘§)) ∈ ((𝐿 Γ—t 𝑀) Cn 𝐽))
10697, 101cnmpt2nd 14085 . . . . 5 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ 𝑀) ∈ ((𝐿 Γ—t 𝑀) Cn 𝑀))
107 hmeocnvcn 14102 . . . . . 6 (𝐺 ∈ (𝐾Homeo𝑀) β†’ ◑𝐺 ∈ (𝑀 Cn 𝐾))
1089, 107syl 14 . . . . 5 (πœ‘ β†’ ◑𝐺 ∈ (𝑀 Cn 𝐾))
10997, 101, 106, 108cnmpt21f 14088 . . . 4 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ (β—‘πΊβ€˜π‘€)) ∈ ((𝐿 Γ—t 𝑀) Cn 𝐾))
11097, 101, 105, 109cnmpt2t 14089 . . 3 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝐿, 𝑀 ∈ βˆͺ 𝑀 ↦ ⟨(β—‘πΉβ€˜π‘§), (β—‘πΊβ€˜π‘€)⟩) ∈ ((𝐿 Γ—t 𝑀) Cn (𝐽 Γ—t 𝐾)))
11193, 110eqeltrd 2264 . 2 (πœ‘ β†’ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩) ∈ ((𝐿 Γ—t 𝑀) Cn (𝐽 Γ—t 𝐾)))
112 ishmeo 14100 . 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 1363   ∈ wcel 2158  βŸ¨cop 3607  βˆͺ cuni 3821   ↦ cmpt 4076   Γ— cxp 4636  β—‘ccnv 4637  βŸΆwf 5224  β€“1-1-ontoβ†’wf1o 5227  β€˜cfv 5228  (class class class)co 5888   ∈ cmpo 5890  1st c1st 6153  2nd c2nd 6154  Topctop 13793  TopOnctopon 13806   Cn ccn 13981   Γ—t ctx 14048  Homeochmeo 14096
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 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-coll 4130  ax-sep 4133  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548
This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-ral 2470  df-rex 2471  df-reu 2472  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-iun 3900  df-br 4016  df-opab 4077  df-mpt 4078  df-id 4305  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235  df-fv 5236  df-ov 5891  df-oprab 5892  df-mpo 5893  df-1st 6155  df-2nd 6156  df-map 6664  df-topgen 12727  df-top 13794  df-topon 13807  df-bases 13839  df-cn 13984  df-tx 14049  df-hmeo 14097
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator