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

Theorem txhmeo 21511
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 21468 . . . . . 6 (𝐹 ∈ (𝐽Homeo𝐿) → 𝐹 ∈ (𝐽 Cn 𝐿))
31, 2syl 17 . . . . 5 (𝜑𝐹 ∈ (𝐽 Cn 𝐿))
4 cntop1 20949 . . . . 5 (𝐹 ∈ (𝐽 Cn 𝐿) → 𝐽 ∈ Top)
53, 4syl 17 . . . 4 (𝜑𝐽 ∈ Top)
6 txhmeo.1 . . . . 5 𝑋 = 𝐽
76toptopon 20643 . . . 4 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
85, 7sylib 208 . . 3 (𝜑𝐽 ∈ (TopOn‘𝑋))
9 txhmeo.4 . . . . . 6 (𝜑𝐺 ∈ (𝐾Homeo𝑀))
10 hmeocn 21468 . . . . . 6 (𝐺 ∈ (𝐾Homeo𝑀) → 𝐺 ∈ (𝐾 Cn 𝑀))
119, 10syl 17 . . . . 5 (𝜑𝐺 ∈ (𝐾 Cn 𝑀))
12 cntop1 20949 . . . . 5 (𝐺 ∈ (𝐾 Cn 𝑀) → 𝐾 ∈ Top)
1311, 12syl 17 . . . 4 (𝜑𝐾 ∈ Top)
14 txhmeo.2 . . . . 5 𝑌 = 𝐾
1514toptopon 20643 . . . 4 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌))
1613, 15sylib 208 . . 3 (𝜑𝐾 ∈ (TopOn‘𝑌))
178, 16cnmpt1st 21376 . . . 4 (𝜑 → (𝑥𝑋, 𝑦𝑌𝑥) ∈ ((𝐽 ×t 𝐾) Cn 𝐽))
188, 16, 17, 3cnmpt21f 21380 . . 3 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ (𝐹𝑥)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
198, 16cnmpt2nd 21377 . . . 4 (𝜑 → (𝑥𝑋, 𝑦𝑌𝑦) ∈ ((𝐽 ×t 𝐾) Cn 𝐾))
208, 16, 19, 11cnmpt21f 21380 . . 3 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ (𝐺𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝑀))
218, 16, 18, 20cnmpt2t 21381 . 2 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐽 ×t 𝐾) Cn (𝐿 ×t 𝑀)))
22 vex 3194 . . . . . . . . . . 11 𝑥 ∈ V
23 vex 3194 . . . . . . . . . . 11 𝑦 ∈ V
2422, 23op1std 7126 . . . . . . . . . 10 (𝑢 = ⟨𝑥, 𝑦⟩ → (1st𝑢) = 𝑥)
2524fveq2d 6154 . . . . . . . . 9 (𝑢 = ⟨𝑥, 𝑦⟩ → (𝐹‘(1st𝑢)) = (𝐹𝑥))
2622, 23op2ndd 7127 . . . . . . . . . 10 (𝑢 = ⟨𝑥, 𝑦⟩ → (2nd𝑢) = 𝑦)
2726fveq2d 6154 . . . . . . . . 9 (𝑢 = ⟨𝑥, 𝑦⟩ → (𝐺‘(2nd𝑢)) = (𝐺𝑦))
2825, 27opeq12d 4383 . . . . . . . 8 (𝑢 = ⟨𝑥, 𝑦⟩ → ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩ = ⟨(𝐹𝑥), (𝐺𝑦)⟩)
2928mpt2mpt 6706 . . . . . . 7 (𝑢 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩) = (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩)
3029eqcomi 2635 . . . . . 6 (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) = (𝑢 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩)
31 eqid 2626 . . . . . . . . . 10 𝐿 = 𝐿
326, 31cnf 20955 . . . . . . . . 9 (𝐹 ∈ (𝐽 Cn 𝐿) → 𝐹:𝑋 𝐿)
333, 32syl 17 . . . . . . . 8 (𝜑𝐹:𝑋 𝐿)
34 xp1st 7146 . . . . . . . 8 (𝑢 ∈ (𝑋 × 𝑌) → (1st𝑢) ∈ 𝑋)
35 ffvelrn 6314 . . . . . . . 8 ((𝐹:𝑋 𝐿 ∧ (1st𝑢) ∈ 𝑋) → (𝐹‘(1st𝑢)) ∈ 𝐿)
3633, 34, 35syl2an 494 . . . . . . 7 ((𝜑𝑢 ∈ (𝑋 × 𝑌)) → (𝐹‘(1st𝑢)) ∈ 𝐿)
37 eqid 2626 . . . . . . . . . 10 𝑀 = 𝑀
3814, 37cnf 20955 . . . . . . . . 9 (𝐺 ∈ (𝐾 Cn 𝑀) → 𝐺:𝑌 𝑀)
3911, 38syl 17 . . . . . . . 8 (𝜑𝐺:𝑌 𝑀)
40 xp2nd 7147 . . . . . . . 8 (𝑢 ∈ (𝑋 × 𝑌) → (2nd𝑢) ∈ 𝑌)
41 ffvelrn 6314 . . . . . . . 8 ((𝐺:𝑌 𝑀 ∧ (2nd𝑢) ∈ 𝑌) → (𝐺‘(2nd𝑢)) ∈ 𝑀)
4239, 40, 41syl2an 494 . . . . . . 7 ((𝜑𝑢 ∈ (𝑋 × 𝑌)) → (𝐺‘(2nd𝑢)) ∈ 𝑀)
43 opelxpi 5113 . . . . . . 7 (((𝐹‘(1st𝑢)) ∈ 𝐿 ∧ (𝐺‘(2nd𝑢)) ∈ 𝑀) → ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩ ∈ ( 𝐿 × 𝑀))
4436, 42, 43syl2anc 692 . . . . . 6 ((𝜑𝑢 ∈ (𝑋 × 𝑌)) → ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩ ∈ ( 𝐿 × 𝑀))
456, 31hmeof1o 21472 . . . . . . . . . 10 (𝐹 ∈ (𝐽Homeo𝐿) → 𝐹:𝑋1-1-onto 𝐿)
461, 45syl 17 . . . . . . . . 9 (𝜑𝐹:𝑋1-1-onto 𝐿)
47 f1ocnv 6108 . . . . . . . . 9 (𝐹:𝑋1-1-onto 𝐿𝐹: 𝐿1-1-onto𝑋)
48 f1of 6096 . . . . . . . . 9 (𝐹: 𝐿1-1-onto𝑋𝐹: 𝐿𝑋)
4946, 47, 483syl 18 . . . . . . . 8 (𝜑𝐹: 𝐿𝑋)
50 xp1st 7146 . . . . . . . 8 (𝑣 ∈ ( 𝐿 × 𝑀) → (1st𝑣) ∈ 𝐿)
51 ffvelrn 6314 . . . . . . . 8 ((𝐹: 𝐿𝑋 ∧ (1st𝑣) ∈ 𝐿) → (𝐹‘(1st𝑣)) ∈ 𝑋)
5249, 50, 51syl2an 494 . . . . . . 7 ((𝜑𝑣 ∈ ( 𝐿 × 𝑀)) → (𝐹‘(1st𝑣)) ∈ 𝑋)
5314, 37hmeof1o 21472 . . . . . . . . . 10 (𝐺 ∈ (𝐾Homeo𝑀) → 𝐺:𝑌1-1-onto 𝑀)
549, 53syl 17 . . . . . . . . 9 (𝜑𝐺:𝑌1-1-onto 𝑀)
55 f1ocnv 6108 . . . . . . . . 9 (𝐺:𝑌1-1-onto 𝑀𝐺: 𝑀1-1-onto𝑌)
56 f1of 6096 . . . . . . . . 9 (𝐺: 𝑀1-1-onto𝑌𝐺: 𝑀𝑌)
5754, 55, 563syl 18 . . . . . . . 8 (𝜑𝐺: 𝑀𝑌)
58 xp2nd 7147 . . . . . . . 8 (𝑣 ∈ ( 𝐿 × 𝑀) → (2nd𝑣) ∈ 𝑀)
59 ffvelrn 6314 . . . . . . . 8 ((𝐺: 𝑀𝑌 ∧ (2nd𝑣) ∈ 𝑀) → (𝐺‘(2nd𝑣)) ∈ 𝑌)
6057, 58, 59syl2an 494 . . . . . . 7 ((𝜑𝑣 ∈ ( 𝐿 × 𝑀)) → (𝐺‘(2nd𝑣)) ∈ 𝑌)
61 opelxpi 5113 . . . . . . 7 (((𝐹‘(1st𝑣)) ∈ 𝑋 ∧ (𝐺‘(2nd𝑣)) ∈ 𝑌) → ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ ∈ (𝑋 × 𝑌))
6252, 60, 61syl2anc 692 . . . . . 6 ((𝜑𝑣 ∈ ( 𝐿 × 𝑀)) → ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ ∈ (𝑋 × 𝑌))
6346adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → 𝐹:𝑋1-1-onto 𝐿)
6434ad2antrl 763 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (1st𝑢) ∈ 𝑋)
6550ad2antll 764 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (1st𝑣) ∈ 𝐿)
66 f1ocnvfvb 6490 . . . . . . . . . 10 ((𝐹:𝑋1-1-onto 𝐿 ∧ (1st𝑢) ∈ 𝑋 ∧ (1st𝑣) ∈ 𝐿) → ((𝐹‘(1st𝑢)) = (1st𝑣) ↔ (𝐹‘(1st𝑣)) = (1st𝑢)))
6763, 64, 65, 66syl3anc 1323 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → ((𝐹‘(1st𝑢)) = (1st𝑣) ↔ (𝐹‘(1st𝑣)) = (1st𝑢)))
68 eqcom 2633 . . . . . . . . 9 ((1st𝑣) = (𝐹‘(1st𝑢)) ↔ (𝐹‘(1st𝑢)) = (1st𝑣))
69 eqcom 2633 . . . . . . . . 9 ((1st𝑢) = (𝐹‘(1st𝑣)) ↔ (𝐹‘(1st𝑣)) = (1st𝑢))
7067, 68, 693bitr4g 303 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → ((1st𝑣) = (𝐹‘(1st𝑢)) ↔ (1st𝑢) = (𝐹‘(1st𝑣))))
7154adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → 𝐺:𝑌1-1-onto 𝑀)
7240ad2antrl 763 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (2nd𝑢) ∈ 𝑌)
7358ad2antll 764 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (2nd𝑣) ∈ 𝑀)
74 f1ocnvfvb 6490 . . . . . . . . . 10 ((𝐺:𝑌1-1-onto 𝑀 ∧ (2nd𝑢) ∈ 𝑌 ∧ (2nd𝑣) ∈ 𝑀) → ((𝐺‘(2nd𝑢)) = (2nd𝑣) ↔ (𝐺‘(2nd𝑣)) = (2nd𝑢)))
7571, 72, 73, 74syl3anc 1323 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → ((𝐺‘(2nd𝑢)) = (2nd𝑣) ↔ (𝐺‘(2nd𝑣)) = (2nd𝑢)))
76 eqcom 2633 . . . . . . . . 9 ((2nd𝑣) = (𝐺‘(2nd𝑢)) ↔ (𝐺‘(2nd𝑢)) = (2nd𝑣))
77 eqcom 2633 . . . . . . . . 9 ((2nd𝑢) = (𝐺‘(2nd𝑣)) ↔ (𝐺‘(2nd𝑣)) = (2nd𝑢))
7875, 76, 773bitr4g 303 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → ((2nd𝑣) = (𝐺‘(2nd𝑢)) ↔ (2nd𝑢) = (𝐺‘(2nd𝑣))))
7970, 78anbi12d 746 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (((1st𝑣) = (𝐹‘(1st𝑢)) ∧ (2nd𝑣) = (𝐺‘(2nd𝑢))) ↔ ((1st𝑢) = (𝐹‘(1st𝑣)) ∧ (2nd𝑢) = (𝐺‘(2nd𝑣)))))
80 eqop 7156 . . . . . . . 8 (𝑣 ∈ ( 𝐿 × 𝑀) → (𝑣 = ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩ ↔ ((1st𝑣) = (𝐹‘(1st𝑢)) ∧ (2nd𝑣) = (𝐺‘(2nd𝑢)))))
8180ad2antll 764 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (𝑣 = ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩ ↔ ((1st𝑣) = (𝐹‘(1st𝑢)) ∧ (2nd𝑣) = (𝐺‘(2nd𝑢)))))
82 eqop 7156 . . . . . . . 8 (𝑢 ∈ (𝑋 × 𝑌) → (𝑢 = ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ ↔ ((1st𝑢) = (𝐹‘(1st𝑣)) ∧ (2nd𝑢) = (𝐺‘(2nd𝑣)))))
8382ad2antrl 763 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (𝑢 = ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ ↔ ((1st𝑢) = (𝐹‘(1st𝑣)) ∧ (2nd𝑢) = (𝐺‘(2nd𝑣)))))
8479, 81, 833bitr4rd 301 . . . . . 6 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (𝑢 = ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ ↔ 𝑣 = ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩))
8530, 44, 62, 84f1ocnv2d 6840 . . . . 5 (𝜑 → ((𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩):(𝑋 × 𝑌)–1-1-onto→( 𝐿 × 𝑀) ∧ (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) = (𝑣 ∈ ( 𝐿 × 𝑀) ↦ ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩)))
8685simprd 479 . . . 4 (𝜑(𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) = (𝑣 ∈ ( 𝐿 × 𝑀) ↦ ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩))
87 vex 3194 . . . . . . . 8 𝑧 ∈ V
88 vex 3194 . . . . . . . 8 𝑤 ∈ V
8987, 88op1std 7126 . . . . . . 7 (𝑣 = ⟨𝑧, 𝑤⟩ → (1st𝑣) = 𝑧)
9089fveq2d 6154 . . . . . 6 (𝑣 = ⟨𝑧, 𝑤⟩ → (𝐹‘(1st𝑣)) = (𝐹𝑧))
9187, 88op2ndd 7127 . . . . . . 7 (𝑣 = ⟨𝑧, 𝑤⟩ → (2nd𝑣) = 𝑤)
9291fveq2d 6154 . . . . . 6 (𝑣 = ⟨𝑧, 𝑤⟩ → (𝐺‘(2nd𝑣)) = (𝐺𝑤))
9390, 92opeq12d 4383 . . . . 5 (𝑣 = ⟨𝑧, 𝑤⟩ → ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ = ⟨(𝐹𝑧), (𝐺𝑤)⟩)
9493mpt2mpt 6706 . . . 4 (𝑣 ∈ ( 𝐿 × 𝑀) ↦ ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩) = (𝑧 𝐿, 𝑤 𝑀 ↦ ⟨(𝐹𝑧), (𝐺𝑤)⟩)
9586, 94syl6eq 2676 . . 3 (𝜑(𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) = (𝑧 𝐿, 𝑤 𝑀 ↦ ⟨(𝐹𝑧), (𝐺𝑤)⟩))
96 cntop2 20950 . . . . . 6 (𝐹 ∈ (𝐽 Cn 𝐿) → 𝐿 ∈ Top)
973, 96syl 17 . . . . 5 (𝜑𝐿 ∈ Top)
9831toptopon 20643 . . . . 5 (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘ 𝐿))
9997, 98sylib 208 . . . 4 (𝜑𝐿 ∈ (TopOn‘ 𝐿))
100 cntop2 20950 . . . . . 6 (𝐺 ∈ (𝐾 Cn 𝑀) → 𝑀 ∈ Top)
10111, 100syl 17 . . . . 5 (𝜑𝑀 ∈ Top)
10237toptopon 20643 . . . . 5 (𝑀 ∈ Top ↔ 𝑀 ∈ (TopOn‘ 𝑀))
103101, 102sylib 208 . . . 4 (𝜑𝑀 ∈ (TopOn‘ 𝑀))
10499, 103cnmpt1st 21376 . . . . 5 (𝜑 → (𝑧 𝐿, 𝑤 𝑀𝑧) ∈ ((𝐿 ×t 𝑀) Cn 𝐿))
105 hmeocnvcn 21469 . . . . . 6 (𝐹 ∈ (𝐽Homeo𝐿) → 𝐹 ∈ (𝐿 Cn 𝐽))
1061, 105syl 17 . . . . 5 (𝜑𝐹 ∈ (𝐿 Cn 𝐽))
10799, 103, 104, 106cnmpt21f 21380 . . . 4 (𝜑 → (𝑧 𝐿, 𝑤 𝑀 ↦ (𝐹𝑧)) ∈ ((𝐿 ×t 𝑀) Cn 𝐽))
10899, 103cnmpt2nd 21377 . . . . 5 (𝜑 → (𝑧 𝐿, 𝑤 𝑀𝑤) ∈ ((𝐿 ×t 𝑀) Cn 𝑀))
109 hmeocnvcn 21469 . . . . . 6 (𝐺 ∈ (𝐾Homeo𝑀) → 𝐺 ∈ (𝑀 Cn 𝐾))
1109, 109syl 17 . . . . 5 (𝜑𝐺 ∈ (𝑀 Cn 𝐾))
11199, 103, 108, 110cnmpt21f 21380 . . . 4 (𝜑 → (𝑧 𝐿, 𝑤 𝑀 ↦ (𝐺𝑤)) ∈ ((𝐿 ×t 𝑀) Cn 𝐾))
11299, 103, 107, 111cnmpt2t 21381 . . 3 (𝜑 → (𝑧 𝐿, 𝑤 𝑀 ↦ ⟨(𝐹𝑧), (𝐺𝑤)⟩) ∈ ((𝐿 ×t 𝑀) Cn (𝐽 ×t 𝐾)))
11395, 112eqeltrd 2704 . 2 (𝜑(𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐿 ×t 𝑀) Cn (𝐽 ×t 𝐾)))
114 ishmeo 21467 . 2 ((𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐽 ×t 𝐾)Homeo(𝐿 ×t 𝑀)) ↔ ((𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐽 ×t 𝐾) Cn (𝐿 ×t 𝑀)) ∧ (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐿 ×t 𝑀) Cn (𝐽 ×t 𝐾))))
11521, 113, 114sylanbrc 697 1 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐽 ×t 𝐾)Homeo(𝐿 ×t 𝑀)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1992  cop 4159   cuni 4407  cmpt 4678   × cxp 5077  ccnv 5078  wf 5846  1-1-ontowf1o 5849  cfv 5850  (class class class)co 6605  cmpt2 6607  1st c1st 7114  2nd c2nd 7115  Topctop 20612  TopOnctopon 20613   Cn ccn 20933   ×t ctx 21268  Homeochmeo 21461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-1st 7116  df-2nd 7117  df-map 7805  df-topgen 16020  df-top 20616  df-bases 20617  df-topon 20618  df-cn 20936  df-tx 21270  df-hmeo 21463
This theorem is referenced by:  xpstopnlem1  21517
  Copyright terms: Public domain W3C validator