Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  txhmeo GIF version

Theorem txhmeo 12497
 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 12483 . . . . . 6 (𝐹 ∈ (𝐽Homeo𝐿) → 𝐹 ∈ (𝐽 Cn 𝐿))
31, 2syl 14 . . . . 5 (𝜑𝐹 ∈ (𝐽 Cn 𝐿))
4 cntop1 12379 . . . . 5 (𝐹 ∈ (𝐽 Cn 𝐿) → 𝐽 ∈ Top)
53, 4syl 14 . . . 4 (𝜑𝐽 ∈ Top)
6 txhmeo.1 . . . . 5 𝑋 = 𝐽
76toptopon 12194 . . . 4 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
85, 7sylib 121 . . 3 (𝜑𝐽 ∈ (TopOn‘𝑋))
9 txhmeo.4 . . . . . 6 (𝜑𝐺 ∈ (𝐾Homeo𝑀))
10 hmeocn 12483 . . . . . 6 (𝐺 ∈ (𝐾Homeo𝑀) → 𝐺 ∈ (𝐾 Cn 𝑀))
119, 10syl 14 . . . . 5 (𝜑𝐺 ∈ (𝐾 Cn 𝑀))
12 cntop1 12379 . . . . 5 (𝐺 ∈ (𝐾 Cn 𝑀) → 𝐾 ∈ Top)
1311, 12syl 14 . . . 4 (𝜑𝐾 ∈ Top)
14 txhmeo.2 . . . . 5 𝑌 = 𝐾
1514toptopon 12194 . . . 4 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌))
1613, 15sylib 121 . . 3 (𝜑𝐾 ∈ (TopOn‘𝑌))
178, 16cnmpt1st 12466 . . . 4 (𝜑 → (𝑥𝑋, 𝑦𝑌𝑥) ∈ ((𝐽 ×t 𝐾) Cn 𝐽))
188, 16, 17, 3cnmpt21f 12470 . . 3 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ (𝐹𝑥)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
198, 16cnmpt2nd 12467 . . . 4 (𝜑 → (𝑥𝑋, 𝑦𝑌𝑦) ∈ ((𝐽 ×t 𝐾) Cn 𝐾))
208, 16, 19, 11cnmpt21f 12470 . . 3 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ (𝐺𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝑀))
218, 16, 18, 20cnmpt2t 12471 . 2 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐽 ×t 𝐾) Cn (𝐿 ×t 𝑀)))
22 vex 2689 . . . . . . . . . . 11 𝑥 ∈ V
23 vex 2689 . . . . . . . . . . 11 𝑦 ∈ V
2422, 23op1std 6046 . . . . . . . . . 10 (𝑢 = ⟨𝑥, 𝑦⟩ → (1st𝑢) = 𝑥)
2524fveq2d 5425 . . . . . . . . 9 (𝑢 = ⟨𝑥, 𝑦⟩ → (𝐹‘(1st𝑢)) = (𝐹𝑥))
2622, 23op2ndd 6047 . . . . . . . . . 10 (𝑢 = ⟨𝑥, 𝑦⟩ → (2nd𝑢) = 𝑦)
2726fveq2d 5425 . . . . . . . . 9 (𝑢 = ⟨𝑥, 𝑦⟩ → (𝐺‘(2nd𝑢)) = (𝐺𝑦))
2825, 27opeq12d 3713 . . . . . . . 8 (𝑢 = ⟨𝑥, 𝑦⟩ → ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩ = ⟨(𝐹𝑥), (𝐺𝑦)⟩)
2928mpompt 5863 . . . . . . 7 (𝑢 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩) = (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩)
3029eqcomi 2143 . . . . . 6 (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) = (𝑢 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩)
31 eqid 2139 . . . . . . . . . 10 𝐿 = 𝐿
326, 31cnf 12382 . . . . . . . . 9 (𝐹 ∈ (𝐽 Cn 𝐿) → 𝐹:𝑋 𝐿)
333, 32syl 14 . . . . . . . 8 (𝜑𝐹:𝑋 𝐿)
34 xp1st 6063 . . . . . . . 8 (𝑢 ∈ (𝑋 × 𝑌) → (1st𝑢) ∈ 𝑋)
35 ffvelrn 5553 . . . . . . . 8 ((𝐹:𝑋 𝐿 ∧ (1st𝑢) ∈ 𝑋) → (𝐹‘(1st𝑢)) ∈ 𝐿)
3633, 34, 35syl2an 287 . . . . . . 7 ((𝜑𝑢 ∈ (𝑋 × 𝑌)) → (𝐹‘(1st𝑢)) ∈ 𝐿)
37 eqid 2139 . . . . . . . . . 10 𝑀 = 𝑀
3814, 37cnf 12382 . . . . . . . . 9 (𝐺 ∈ (𝐾 Cn 𝑀) → 𝐺:𝑌 𝑀)
3911, 38syl 14 . . . . . . . 8 (𝜑𝐺:𝑌 𝑀)
40 xp2nd 6064 . . . . . . . 8 (𝑢 ∈ (𝑋 × 𝑌) → (2nd𝑢) ∈ 𝑌)
41 ffvelrn 5553 . . . . . . . 8 ((𝐺:𝑌 𝑀 ∧ (2nd𝑢) ∈ 𝑌) → (𝐺‘(2nd𝑢)) ∈ 𝑀)
4239, 40, 41syl2an 287 . . . . . . 7 ((𝜑𝑢 ∈ (𝑋 × 𝑌)) → (𝐺‘(2nd𝑢)) ∈ 𝑀)
4336, 42opelxpd 4572 . . . . . 6 ((𝜑𝑢 ∈ (𝑋 × 𝑌)) → ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩ ∈ ( 𝐿 × 𝑀))
446, 31hmeof1o 12487 . . . . . . . . . 10 (𝐹 ∈ (𝐽Homeo𝐿) → 𝐹:𝑋1-1-onto 𝐿)
451, 44syl 14 . . . . . . . . 9 (𝜑𝐹:𝑋1-1-onto 𝐿)
46 f1ocnv 5380 . . . . . . . . 9 (𝐹:𝑋1-1-onto 𝐿𝐹: 𝐿1-1-onto𝑋)
47 f1of 5367 . . . . . . . . 9 (𝐹: 𝐿1-1-onto𝑋𝐹: 𝐿𝑋)
4845, 46, 473syl 17 . . . . . . . 8 (𝜑𝐹: 𝐿𝑋)
49 xp1st 6063 . . . . . . . 8 (𝑣 ∈ ( 𝐿 × 𝑀) → (1st𝑣) ∈ 𝐿)
50 ffvelrn 5553 . . . . . . . 8 ((𝐹: 𝐿𝑋 ∧ (1st𝑣) ∈ 𝐿) → (𝐹‘(1st𝑣)) ∈ 𝑋)
5148, 49, 50syl2an 287 . . . . . . 7 ((𝜑𝑣 ∈ ( 𝐿 × 𝑀)) → (𝐹‘(1st𝑣)) ∈ 𝑋)
5214, 37hmeof1o 12487 . . . . . . . . . 10 (𝐺 ∈ (𝐾Homeo𝑀) → 𝐺:𝑌1-1-onto 𝑀)
539, 52syl 14 . . . . . . . . 9 (𝜑𝐺:𝑌1-1-onto 𝑀)
54 f1ocnv 5380 . . . . . . . . 9 (𝐺:𝑌1-1-onto 𝑀𝐺: 𝑀1-1-onto𝑌)
55 f1of 5367 . . . . . . . . 9 (𝐺: 𝑀1-1-onto𝑌𝐺: 𝑀𝑌)
5653, 54, 553syl 17 . . . . . . . 8 (𝜑𝐺: 𝑀𝑌)
57 xp2nd 6064 . . . . . . . 8 (𝑣 ∈ ( 𝐿 × 𝑀) → (2nd𝑣) ∈ 𝑀)
58 ffvelrn 5553 . . . . . . . 8 ((𝐺: 𝑀𝑌 ∧ (2nd𝑣) ∈ 𝑀) → (𝐺‘(2nd𝑣)) ∈ 𝑌)
5956, 57, 58syl2an 287 . . . . . . 7 ((𝜑𝑣 ∈ ( 𝐿 × 𝑀)) → (𝐺‘(2nd𝑣)) ∈ 𝑌)
6051, 59opelxpd 4572 . . . . . 6 ((𝜑𝑣 ∈ ( 𝐿 × 𝑀)) → ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ ∈ (𝑋 × 𝑌))
6145adantr 274 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → 𝐹:𝑋1-1-onto 𝐿)
6234ad2antrl 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (1st𝑢) ∈ 𝑋)
6349ad2antll 482 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (1st𝑣) ∈ 𝐿)
64 f1ocnvfvb 5681 . . . . . . . . . 10 ((𝐹:𝑋1-1-onto 𝐿 ∧ (1st𝑢) ∈ 𝑋 ∧ (1st𝑣) ∈ 𝐿) → ((𝐹‘(1st𝑢)) = (1st𝑣) ↔ (𝐹‘(1st𝑣)) = (1st𝑢)))
6561, 62, 63, 64syl3anc 1216 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → ((𝐹‘(1st𝑢)) = (1st𝑣) ↔ (𝐹‘(1st𝑣)) = (1st𝑢)))
66 eqcom 2141 . . . . . . . . 9 ((1st𝑣) = (𝐹‘(1st𝑢)) ↔ (𝐹‘(1st𝑢)) = (1st𝑣))
67 eqcom 2141 . . . . . . . . 9 ((1st𝑢) = (𝐹‘(1st𝑣)) ↔ (𝐹‘(1st𝑣)) = (1st𝑢))
6865, 66, 673bitr4g 222 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → ((1st𝑣) = (𝐹‘(1st𝑢)) ↔ (1st𝑢) = (𝐹‘(1st𝑣))))
6953adantr 274 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → 𝐺:𝑌1-1-onto 𝑀)
7040ad2antrl 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (2nd𝑢) ∈ 𝑌)
7157ad2antll 482 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (2nd𝑣) ∈ 𝑀)
72 f1ocnvfvb 5681 . . . . . . . . . 10 ((𝐺:𝑌1-1-onto 𝑀 ∧ (2nd𝑢) ∈ 𝑌 ∧ (2nd𝑣) ∈ 𝑀) → ((𝐺‘(2nd𝑢)) = (2nd𝑣) ↔ (𝐺‘(2nd𝑣)) = (2nd𝑢)))
7369, 70, 71, 72syl3anc 1216 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → ((𝐺‘(2nd𝑢)) = (2nd𝑣) ↔ (𝐺‘(2nd𝑣)) = (2nd𝑢)))
74 eqcom 2141 . . . . . . . . 9 ((2nd𝑣) = (𝐺‘(2nd𝑢)) ↔ (𝐺‘(2nd𝑢)) = (2nd𝑣))
75 eqcom 2141 . . . . . . . . 9 ((2nd𝑢) = (𝐺‘(2nd𝑣)) ↔ (𝐺‘(2nd𝑣)) = (2nd𝑢))
7673, 74, 753bitr4g 222 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → ((2nd𝑣) = (𝐺‘(2nd𝑢)) ↔ (2nd𝑢) = (𝐺‘(2nd𝑣))))
7768, 76anbi12d 464 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (((1st𝑣) = (𝐹‘(1st𝑢)) ∧ (2nd𝑣) = (𝐺‘(2nd𝑢))) ↔ ((1st𝑢) = (𝐹‘(1st𝑣)) ∧ (2nd𝑢) = (𝐺‘(2nd𝑣)))))
78 eqop 6075 . . . . . . . 8 (𝑣 ∈ ( 𝐿 × 𝑀) → (𝑣 = ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩ ↔ ((1st𝑣) = (𝐹‘(1st𝑢)) ∧ (2nd𝑣) = (𝐺‘(2nd𝑢)))))
7978ad2antll 482 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (𝑣 = ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩ ↔ ((1st𝑣) = (𝐹‘(1st𝑢)) ∧ (2nd𝑣) = (𝐺‘(2nd𝑢)))))
80 eqop 6075 . . . . . . . 8 (𝑢 ∈ (𝑋 × 𝑌) → (𝑢 = ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ ↔ ((1st𝑢) = (𝐹‘(1st𝑣)) ∧ (2nd𝑢) = (𝐺‘(2nd𝑣)))))
8180ad2antrl 481 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (𝑢 = ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ ↔ ((1st𝑢) = (𝐹‘(1st𝑣)) ∧ (2nd𝑢) = (𝐺‘(2nd𝑣)))))
8277, 79, 813bitr4rd 220 . . . . . 6 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (𝑢 = ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ ↔ 𝑣 = ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩))
8330, 43, 60, 82f1ocnv2d 5974 . . . . 5 (𝜑 → ((𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩):(𝑋 × 𝑌)–1-1-onto→( 𝐿 × 𝑀) ∧ (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) = (𝑣 ∈ ( 𝐿 × 𝑀) ↦ ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩)))
8483simprd 113 . . . 4 (𝜑(𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) = (𝑣 ∈ ( 𝐿 × 𝑀) ↦ ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩))
85 vex 2689 . . . . . . . 8 𝑧 ∈ V
86 vex 2689 . . . . . . . 8 𝑤 ∈ V
8785, 86op1std 6046 . . . . . . 7 (𝑣 = ⟨𝑧, 𝑤⟩ → (1st𝑣) = 𝑧)
8887fveq2d 5425 . . . . . 6 (𝑣 = ⟨𝑧, 𝑤⟩ → (𝐹‘(1st𝑣)) = (𝐹𝑧))
8985, 86op2ndd 6047 . . . . . . 7 (𝑣 = ⟨𝑧, 𝑤⟩ → (2nd𝑣) = 𝑤)
9089fveq2d 5425 . . . . . 6 (𝑣 = ⟨𝑧, 𝑤⟩ → (𝐺‘(2nd𝑣)) = (𝐺𝑤))
9188, 90opeq12d 3713 . . . . 5 (𝑣 = ⟨𝑧, 𝑤⟩ → ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ = ⟨(𝐹𝑧), (𝐺𝑤)⟩)
9291mpompt 5863 . . . 4 (𝑣 ∈ ( 𝐿 × 𝑀) ↦ ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩) = (𝑧 𝐿, 𝑤 𝑀 ↦ ⟨(𝐹𝑧), (𝐺𝑤)⟩)
9384, 92syl6eq 2188 . . 3 (𝜑(𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) = (𝑧 𝐿, 𝑤 𝑀 ↦ ⟨(𝐹𝑧), (𝐺𝑤)⟩))
94 cntop2 12380 . . . . . 6 (𝐹 ∈ (𝐽 Cn 𝐿) → 𝐿 ∈ Top)
953, 94syl 14 . . . . 5 (𝜑𝐿 ∈ Top)
9631toptopon 12194 . . . . 5 (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘ 𝐿))
9795, 96sylib 121 . . . 4 (𝜑𝐿 ∈ (TopOn‘ 𝐿))
98 cntop2 12380 . . . . . 6 (𝐺 ∈ (𝐾 Cn 𝑀) → 𝑀 ∈ Top)
9911, 98syl 14 . . . . 5 (𝜑𝑀 ∈ Top)
10037toptopon 12194 . . . . 5 (𝑀 ∈ Top ↔ 𝑀 ∈ (TopOn‘ 𝑀))
10199, 100sylib 121 . . . 4 (𝜑𝑀 ∈ (TopOn‘ 𝑀))
10297, 101cnmpt1st 12466 . . . . 5 (𝜑 → (𝑧 𝐿, 𝑤 𝑀𝑧) ∈ ((𝐿 ×t 𝑀) Cn 𝐿))
103 hmeocnvcn 12484 . . . . . 6 (𝐹 ∈ (𝐽Homeo𝐿) → 𝐹 ∈ (𝐿 Cn 𝐽))
1041, 103syl 14 . . . . 5 (𝜑𝐹 ∈ (𝐿 Cn 𝐽))
10597, 101, 102, 104cnmpt21f 12470 . . . 4 (𝜑 → (𝑧 𝐿, 𝑤 𝑀 ↦ (𝐹𝑧)) ∈ ((𝐿 ×t 𝑀) Cn 𝐽))
10697, 101cnmpt2nd 12467 . . . . 5 (𝜑 → (𝑧 𝐿, 𝑤 𝑀𝑤) ∈ ((𝐿 ×t 𝑀) Cn 𝑀))
107 hmeocnvcn 12484 . . . . . 6 (𝐺 ∈ (𝐾Homeo𝑀) → 𝐺 ∈ (𝑀 Cn 𝐾))
1089, 107syl 14 . . . . 5 (𝜑𝐺 ∈ (𝑀 Cn 𝐾))
10997, 101, 106, 108cnmpt21f 12470 . . . 4 (𝜑 → (𝑧 𝐿, 𝑤 𝑀 ↦ (𝐺𝑤)) ∈ ((𝐿 ×t 𝑀) Cn 𝐾))
11097, 101, 105, 109cnmpt2t 12471 . . 3 (𝜑 → (𝑧 𝐿, 𝑤 𝑀 ↦ ⟨(𝐹𝑧), (𝐺𝑤)⟩) ∈ ((𝐿 ×t 𝑀) Cn (𝐽 ×t 𝐾)))
11193, 110eqeltrd 2216 . 2 (𝜑(𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐿 ×t 𝑀) Cn (𝐽 ×t 𝐾)))
112 ishmeo 12482 . 2 ((𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐽 ×t 𝐾)Homeo(𝐿 ×t 𝑀)) ↔ ((𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐽 ×t 𝐾) Cn (𝐿 ×t 𝑀)) ∧ (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐿 ×t 𝑀) Cn (𝐽 ×t 𝐾))))
11321, 111, 112sylanbrc 413 1 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐽 ×t 𝐾)Homeo(𝐿 ×t 𝑀)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1331   ∈ wcel 1480  ⟨cop 3530  ∪ cuni 3736   ↦ cmpt 3989   × cxp 4537  ◡ccnv 4538  ⟶wf 5119  –1-1-onto→wf1o 5122  ‘cfv 5123  (class class class)co 5774   ∈ cmpo 5776  1st c1st 6036  2nd c2nd 6037  Topctop 12173  TopOnctopon 12186   Cn ccn 12363   ×t ctx 12430  Homeochmeo 12478 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452 This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-id 4215  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-map 6544  df-topgen 12150  df-top 12174  df-topon 12187  df-bases 12219  df-cn 12366  df-tx 12431  df-hmeo 12479 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator