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

Theorem txhmeo 21654
 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 21611 . . . . . 6 (𝐹 ∈ (𝐽Homeo𝐿) → 𝐹 ∈ (𝐽 Cn 𝐿))
31, 2syl 17 . . . . 5 (𝜑𝐹 ∈ (𝐽 Cn 𝐿))
4 cntop1 21092 . . . . 5 (𝐹 ∈ (𝐽 Cn 𝐿) → 𝐽 ∈ Top)
53, 4syl 17 . . . 4 (𝜑𝐽 ∈ Top)
6 txhmeo.1 . . . . 5 𝑋 = 𝐽
76toptopon 20770 . . . 4 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
85, 7sylib 208 . . 3 (𝜑𝐽 ∈ (TopOn‘𝑋))
9 txhmeo.4 . . . . . 6 (𝜑𝐺 ∈ (𝐾Homeo𝑀))
10 hmeocn 21611 . . . . . 6 (𝐺 ∈ (𝐾Homeo𝑀) → 𝐺 ∈ (𝐾 Cn 𝑀))
119, 10syl 17 . . . . 5 (𝜑𝐺 ∈ (𝐾 Cn 𝑀))
12 cntop1 21092 . . . . 5 (𝐺 ∈ (𝐾 Cn 𝑀) → 𝐾 ∈ Top)
1311, 12syl 17 . . . 4 (𝜑𝐾 ∈ Top)
14 txhmeo.2 . . . . 5 𝑌 = 𝐾
1514toptopon 20770 . . . 4 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌))
1613, 15sylib 208 . . 3 (𝜑𝐾 ∈ (TopOn‘𝑌))
178, 16cnmpt1st 21519 . . . 4 (𝜑 → (𝑥𝑋, 𝑦𝑌𝑥) ∈ ((𝐽 ×t 𝐾) Cn 𝐽))
188, 16, 17, 3cnmpt21f 21523 . . 3 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ (𝐹𝑥)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
198, 16cnmpt2nd 21520 . . . 4 (𝜑 → (𝑥𝑋, 𝑦𝑌𝑦) ∈ ((𝐽 ×t 𝐾) Cn 𝐾))
208, 16, 19, 11cnmpt21f 21523 . . 3 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ (𝐺𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝑀))
218, 16, 18, 20cnmpt2t 21524 . 2 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐽 ×t 𝐾) Cn (𝐿 ×t 𝑀)))
22 vex 3234 . . . . . . . . . . 11 𝑥 ∈ V
23 vex 3234 . . . . . . . . . . 11 𝑦 ∈ V
2422, 23op1std 7220 . . . . . . . . . 10 (𝑢 = ⟨𝑥, 𝑦⟩ → (1st𝑢) = 𝑥)
2524fveq2d 6233 . . . . . . . . 9 (𝑢 = ⟨𝑥, 𝑦⟩ → (𝐹‘(1st𝑢)) = (𝐹𝑥))
2622, 23op2ndd 7221 . . . . . . . . . 10 (𝑢 = ⟨𝑥, 𝑦⟩ → (2nd𝑢) = 𝑦)
2726fveq2d 6233 . . . . . . . . 9 (𝑢 = ⟨𝑥, 𝑦⟩ → (𝐺‘(2nd𝑢)) = (𝐺𝑦))
2825, 27opeq12d 4441 . . . . . . . 8 (𝑢 = ⟨𝑥, 𝑦⟩ → ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩ = ⟨(𝐹𝑥), (𝐺𝑦)⟩)
2928mpt2mpt 6794 . . . . . . 7 (𝑢 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩) = (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩)
3029eqcomi 2660 . . . . . 6 (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) = (𝑢 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩)
31 eqid 2651 . . . . . . . . . 10 𝐿 = 𝐿
326, 31cnf 21098 . . . . . . . . 9 (𝐹 ∈ (𝐽 Cn 𝐿) → 𝐹:𝑋 𝐿)
333, 32syl 17 . . . . . . . 8 (𝜑𝐹:𝑋 𝐿)
34 xp1st 7242 . . . . . . . 8 (𝑢 ∈ (𝑋 × 𝑌) → (1st𝑢) ∈ 𝑋)
35 ffvelrn 6397 . . . . . . . 8 ((𝐹:𝑋 𝐿 ∧ (1st𝑢) ∈ 𝑋) → (𝐹‘(1st𝑢)) ∈ 𝐿)
3633, 34, 35syl2an 493 . . . . . . 7 ((𝜑𝑢 ∈ (𝑋 × 𝑌)) → (𝐹‘(1st𝑢)) ∈ 𝐿)
37 eqid 2651 . . . . . . . . . 10 𝑀 = 𝑀
3814, 37cnf 21098 . . . . . . . . 9 (𝐺 ∈ (𝐾 Cn 𝑀) → 𝐺:𝑌 𝑀)
3911, 38syl 17 . . . . . . . 8 (𝜑𝐺:𝑌 𝑀)
40 xp2nd 7243 . . . . . . . 8 (𝑢 ∈ (𝑋 × 𝑌) → (2nd𝑢) ∈ 𝑌)
41 ffvelrn 6397 . . . . . . . 8 ((𝐺:𝑌 𝑀 ∧ (2nd𝑢) ∈ 𝑌) → (𝐺‘(2nd𝑢)) ∈ 𝑀)
4239, 40, 41syl2an 493 . . . . . . 7 ((𝜑𝑢 ∈ (𝑋 × 𝑌)) → (𝐺‘(2nd𝑢)) ∈ 𝑀)
43 opelxpi 5182 . . . . . . 7 (((𝐹‘(1st𝑢)) ∈ 𝐿 ∧ (𝐺‘(2nd𝑢)) ∈ 𝑀) → ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩ ∈ ( 𝐿 × 𝑀))
4436, 42, 43syl2anc 694 . . . . . 6 ((𝜑𝑢 ∈ (𝑋 × 𝑌)) → ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩ ∈ ( 𝐿 × 𝑀))
456, 31hmeof1o 21615 . . . . . . . . . 10 (𝐹 ∈ (𝐽Homeo𝐿) → 𝐹:𝑋1-1-onto 𝐿)
461, 45syl 17 . . . . . . . . 9 (𝜑𝐹:𝑋1-1-onto 𝐿)
47 f1ocnv 6187 . . . . . . . . 9 (𝐹:𝑋1-1-onto 𝐿𝐹: 𝐿1-1-onto𝑋)
48 f1of 6175 . . . . . . . . 9 (𝐹: 𝐿1-1-onto𝑋𝐹: 𝐿𝑋)
4946, 47, 483syl 18 . . . . . . . 8 (𝜑𝐹: 𝐿𝑋)
50 xp1st 7242 . . . . . . . 8 (𝑣 ∈ ( 𝐿 × 𝑀) → (1st𝑣) ∈ 𝐿)
51 ffvelrn 6397 . . . . . . . 8 ((𝐹: 𝐿𝑋 ∧ (1st𝑣) ∈ 𝐿) → (𝐹‘(1st𝑣)) ∈ 𝑋)
5249, 50, 51syl2an 493 . . . . . . 7 ((𝜑𝑣 ∈ ( 𝐿 × 𝑀)) → (𝐹‘(1st𝑣)) ∈ 𝑋)
5314, 37hmeof1o 21615 . . . . . . . . . 10 (𝐺 ∈ (𝐾Homeo𝑀) → 𝐺:𝑌1-1-onto 𝑀)
549, 53syl 17 . . . . . . . . 9 (𝜑𝐺:𝑌1-1-onto 𝑀)
55 f1ocnv 6187 . . . . . . . . 9 (𝐺:𝑌1-1-onto 𝑀𝐺: 𝑀1-1-onto𝑌)
56 f1of 6175 . . . . . . . . 9 (𝐺: 𝑀1-1-onto𝑌𝐺: 𝑀𝑌)
5754, 55, 563syl 18 . . . . . . . 8 (𝜑𝐺: 𝑀𝑌)
58 xp2nd 7243 . . . . . . . 8 (𝑣 ∈ ( 𝐿 × 𝑀) → (2nd𝑣) ∈ 𝑀)
59 ffvelrn 6397 . . . . . . . 8 ((𝐺: 𝑀𝑌 ∧ (2nd𝑣) ∈ 𝑀) → (𝐺‘(2nd𝑣)) ∈ 𝑌)
6057, 58, 59syl2an 493 . . . . . . 7 ((𝜑𝑣 ∈ ( 𝐿 × 𝑀)) → (𝐺‘(2nd𝑣)) ∈ 𝑌)
61 opelxpi 5182 . . . . . . 7 (((𝐹‘(1st𝑣)) ∈ 𝑋 ∧ (𝐺‘(2nd𝑣)) ∈ 𝑌) → ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ ∈ (𝑋 × 𝑌))
6252, 60, 61syl2anc 694 . . . . . 6 ((𝜑𝑣 ∈ ( 𝐿 × 𝑀)) → ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ ∈ (𝑋 × 𝑌))
6346adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → 𝐹:𝑋1-1-onto 𝐿)
6434ad2antrl 764 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (1st𝑢) ∈ 𝑋)
6550ad2antll 765 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (1st𝑣) ∈ 𝐿)
66 f1ocnvfvb 6575 . . . . . . . . . 10 ((𝐹:𝑋1-1-onto 𝐿 ∧ (1st𝑢) ∈ 𝑋 ∧ (1st𝑣) ∈ 𝐿) → ((𝐹‘(1st𝑢)) = (1st𝑣) ↔ (𝐹‘(1st𝑣)) = (1st𝑢)))
6763, 64, 65, 66syl3anc 1366 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → ((𝐹‘(1st𝑢)) = (1st𝑣) ↔ (𝐹‘(1st𝑣)) = (1st𝑢)))
68 eqcom 2658 . . . . . . . . 9 ((1st𝑣) = (𝐹‘(1st𝑢)) ↔ (𝐹‘(1st𝑢)) = (1st𝑣))
69 eqcom 2658 . . . . . . . . 9 ((1st𝑢) = (𝐹‘(1st𝑣)) ↔ (𝐹‘(1st𝑣)) = (1st𝑢))
7067, 68, 693bitr4g 303 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → ((1st𝑣) = (𝐹‘(1st𝑢)) ↔ (1st𝑢) = (𝐹‘(1st𝑣))))
7154adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → 𝐺:𝑌1-1-onto 𝑀)
7240ad2antrl 764 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (2nd𝑢) ∈ 𝑌)
7358ad2antll 765 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (2nd𝑣) ∈ 𝑀)
74 f1ocnvfvb 6575 . . . . . . . . . 10 ((𝐺:𝑌1-1-onto 𝑀 ∧ (2nd𝑢) ∈ 𝑌 ∧ (2nd𝑣) ∈ 𝑀) → ((𝐺‘(2nd𝑢)) = (2nd𝑣) ↔ (𝐺‘(2nd𝑣)) = (2nd𝑢)))
7571, 72, 73, 74syl3anc 1366 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → ((𝐺‘(2nd𝑢)) = (2nd𝑣) ↔ (𝐺‘(2nd𝑣)) = (2nd𝑢)))
76 eqcom 2658 . . . . . . . . 9 ((2nd𝑣) = (𝐺‘(2nd𝑢)) ↔ (𝐺‘(2nd𝑢)) = (2nd𝑣))
77 eqcom 2658 . . . . . . . . 9 ((2nd𝑢) = (𝐺‘(2nd𝑣)) ↔ (𝐺‘(2nd𝑣)) = (2nd𝑢))
7875, 76, 773bitr4g 303 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → ((2nd𝑣) = (𝐺‘(2nd𝑢)) ↔ (2nd𝑢) = (𝐺‘(2nd𝑣))))
7970, 78anbi12d 747 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (((1st𝑣) = (𝐹‘(1st𝑢)) ∧ (2nd𝑣) = (𝐺‘(2nd𝑢))) ↔ ((1st𝑢) = (𝐹‘(1st𝑣)) ∧ (2nd𝑢) = (𝐺‘(2nd𝑣)))))
80 eqop 7252 . . . . . . . 8 (𝑣 ∈ ( 𝐿 × 𝑀) → (𝑣 = ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩ ↔ ((1st𝑣) = (𝐹‘(1st𝑢)) ∧ (2nd𝑣) = (𝐺‘(2nd𝑢)))))
8180ad2antll 765 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (𝑣 = ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩ ↔ ((1st𝑣) = (𝐹‘(1st𝑢)) ∧ (2nd𝑣) = (𝐺‘(2nd𝑢)))))
82 eqop 7252 . . . . . . . 8 (𝑢 ∈ (𝑋 × 𝑌) → (𝑢 = ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ ↔ ((1st𝑢) = (𝐹‘(1st𝑣)) ∧ (2nd𝑢) = (𝐺‘(2nd𝑣)))))
8382ad2antrl 764 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (𝑢 = ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ ↔ ((1st𝑢) = (𝐹‘(1st𝑣)) ∧ (2nd𝑢) = (𝐺‘(2nd𝑣)))))
8479, 81, 833bitr4rd 301 . . . . . 6 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (𝑢 = ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ ↔ 𝑣 = ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩))
8530, 44, 62, 84f1ocnv2d 6928 . . . . 5 (𝜑 → ((𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩):(𝑋 × 𝑌)–1-1-onto→( 𝐿 × 𝑀) ∧ (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) = (𝑣 ∈ ( 𝐿 × 𝑀) ↦ ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩)))
8685simprd 478 . . . 4 (𝜑(𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) = (𝑣 ∈ ( 𝐿 × 𝑀) ↦ ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩))
87 vex 3234 . . . . . . . 8 𝑧 ∈ V
88 vex 3234 . . . . . . . 8 𝑤 ∈ V
8987, 88op1std 7220 . . . . . . 7 (𝑣 = ⟨𝑧, 𝑤⟩ → (1st𝑣) = 𝑧)
9089fveq2d 6233 . . . . . 6 (𝑣 = ⟨𝑧, 𝑤⟩ → (𝐹‘(1st𝑣)) = (𝐹𝑧))
9187, 88op2ndd 7221 . . . . . . 7 (𝑣 = ⟨𝑧, 𝑤⟩ → (2nd𝑣) = 𝑤)
9291fveq2d 6233 . . . . . 6 (𝑣 = ⟨𝑧, 𝑤⟩ → (𝐺‘(2nd𝑣)) = (𝐺𝑤))
9390, 92opeq12d 4441 . . . . 5 (𝑣 = ⟨𝑧, 𝑤⟩ → ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ = ⟨(𝐹𝑧), (𝐺𝑤)⟩)
9493mpt2mpt 6794 . . . 4 (𝑣 ∈ ( 𝐿 × 𝑀) ↦ ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩) = (𝑧 𝐿, 𝑤 𝑀 ↦ ⟨(𝐹𝑧), (𝐺𝑤)⟩)
9586, 94syl6eq 2701 . . 3 (𝜑(𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) = (𝑧 𝐿, 𝑤 𝑀 ↦ ⟨(𝐹𝑧), (𝐺𝑤)⟩))
96 cntop2 21093 . . . . . 6 (𝐹 ∈ (𝐽 Cn 𝐿) → 𝐿 ∈ Top)
973, 96syl 17 . . . . 5 (𝜑𝐿 ∈ Top)
9831toptopon 20770 . . . . 5 (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘ 𝐿))
9997, 98sylib 208 . . . 4 (𝜑𝐿 ∈ (TopOn‘ 𝐿))
100 cntop2 21093 . . . . . 6 (𝐺 ∈ (𝐾 Cn 𝑀) → 𝑀 ∈ Top)
10111, 100syl 17 . . . . 5 (𝜑𝑀 ∈ Top)
10237toptopon 20770 . . . . 5 (𝑀 ∈ Top ↔ 𝑀 ∈ (TopOn‘ 𝑀))
103101, 102sylib 208 . . . 4 (𝜑𝑀 ∈ (TopOn‘ 𝑀))
10499, 103cnmpt1st 21519 . . . . 5 (𝜑 → (𝑧 𝐿, 𝑤 𝑀𝑧) ∈ ((𝐿 ×t 𝑀) Cn 𝐿))
105 hmeocnvcn 21612 . . . . . 6 (𝐹 ∈ (𝐽Homeo𝐿) → 𝐹 ∈ (𝐿 Cn 𝐽))
1061, 105syl 17 . . . . 5 (𝜑𝐹 ∈ (𝐿 Cn 𝐽))
10799, 103, 104, 106cnmpt21f 21523 . . . 4 (𝜑 → (𝑧 𝐿, 𝑤 𝑀 ↦ (𝐹𝑧)) ∈ ((𝐿 ×t 𝑀) Cn 𝐽))
10899, 103cnmpt2nd 21520 . . . . 5 (𝜑 → (𝑧 𝐿, 𝑤 𝑀𝑤) ∈ ((𝐿 ×t 𝑀) Cn 𝑀))
109 hmeocnvcn 21612 . . . . . 6 (𝐺 ∈ (𝐾Homeo𝑀) → 𝐺 ∈ (𝑀 Cn 𝐾))
1109, 109syl 17 . . . . 5 (𝜑𝐺 ∈ (𝑀 Cn 𝐾))
11199, 103, 108, 110cnmpt21f 21523 . . . 4 (𝜑 → (𝑧 𝐿, 𝑤 𝑀 ↦ (𝐺𝑤)) ∈ ((𝐿 ×t 𝑀) Cn 𝐾))
11299, 103, 107, 111cnmpt2t 21524 . . 3 (𝜑 → (𝑧 𝐿, 𝑤 𝑀 ↦ ⟨(𝐹𝑧), (𝐺𝑤)⟩) ∈ ((𝐿 ×t 𝑀) Cn (𝐽 ×t 𝐾)))
11395, 112eqeltrd 2730 . 2 (𝜑(𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐿 ×t 𝑀) Cn (𝐽 ×t 𝐾)))
114 ishmeo 21610 . 2 ((𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐽 ×t 𝐾)Homeo(𝐿 ×t 𝑀)) ↔ ((𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐽 ×t 𝐾) Cn (𝐿 ×t 𝑀)) ∧ (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐿 ×t 𝑀) Cn (𝐽 ×t 𝐾))))
11521, 113, 114sylanbrc 699 1 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐽 ×t 𝐾)Homeo(𝐿 ×t 𝑀)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523   ∈ wcel 2030  ⟨cop 4216  ∪ cuni 4468   ↦ cmpt 4762   × cxp 5141  ◡ccnv 5142  ⟶wf 5922  –1-1-onto→wf1o 5925  ‘cfv 5926  (class class class)co 6690   ↦ cmpt2 6692  1st c1st 7208  2nd c2nd 7209  Topctop 20746  TopOnctopon 20763   Cn ccn 21076   ×t ctx 21411  Homeochmeo 21604 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211  df-map 7901  df-topgen 16151  df-top 20747  df-topon 20764  df-bases 20798  df-cn 21079  df-tx 21413  df-hmeo 21606 This theorem is referenced by:  xpstopnlem1  21660
 Copyright terms: Public domain W3C validator