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

Theorem txhmeo 22405
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 22362 . . . . . 6 (𝐹 ∈ (𝐽Homeo𝐿) → 𝐹 ∈ (𝐽 Cn 𝐿))
31, 2syl 17 . . . . 5 (𝜑𝐹 ∈ (𝐽 Cn 𝐿))
4 cntop1 21842 . . . . 5 (𝐹 ∈ (𝐽 Cn 𝐿) → 𝐽 ∈ Top)
53, 4syl 17 . . . 4 (𝜑𝐽 ∈ Top)
6 txhmeo.1 . . . . 5 𝑋 = 𝐽
76toptopon 21519 . . . 4 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
85, 7sylib 220 . . 3 (𝜑𝐽 ∈ (TopOn‘𝑋))
9 txhmeo.4 . . . . . 6 (𝜑𝐺 ∈ (𝐾Homeo𝑀))
10 hmeocn 22362 . . . . . 6 (𝐺 ∈ (𝐾Homeo𝑀) → 𝐺 ∈ (𝐾 Cn 𝑀))
119, 10syl 17 . . . . 5 (𝜑𝐺 ∈ (𝐾 Cn 𝑀))
12 cntop1 21842 . . . . 5 (𝐺 ∈ (𝐾 Cn 𝑀) → 𝐾 ∈ Top)
1311, 12syl 17 . . . 4 (𝜑𝐾 ∈ Top)
14 txhmeo.2 . . . . 5 𝑌 = 𝐾
1514toptopon 21519 . . . 4 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌))
1613, 15sylib 220 . . 3 (𝜑𝐾 ∈ (TopOn‘𝑌))
178, 16cnmpt1st 22270 . . . 4 (𝜑 → (𝑥𝑋, 𝑦𝑌𝑥) ∈ ((𝐽 ×t 𝐾) Cn 𝐽))
188, 16, 17, 3cnmpt21f 22274 . . 3 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ (𝐹𝑥)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
198, 16cnmpt2nd 22271 . . . 4 (𝜑 → (𝑥𝑋, 𝑦𝑌𝑦) ∈ ((𝐽 ×t 𝐾) Cn 𝐾))
208, 16, 19, 11cnmpt21f 22274 . . 3 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ (𝐺𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝑀))
218, 16, 18, 20cnmpt2t 22275 . 2 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐽 ×t 𝐾) Cn (𝐿 ×t 𝑀)))
22 vex 3498 . . . . . . . . . . 11 𝑥 ∈ V
23 vex 3498 . . . . . . . . . . 11 𝑦 ∈ V
2422, 23op1std 7693 . . . . . . . . . 10 (𝑢 = ⟨𝑥, 𝑦⟩ → (1st𝑢) = 𝑥)
2524fveq2d 6669 . . . . . . . . 9 (𝑢 = ⟨𝑥, 𝑦⟩ → (𝐹‘(1st𝑢)) = (𝐹𝑥))
2622, 23op2ndd 7694 . . . . . . . . . 10 (𝑢 = ⟨𝑥, 𝑦⟩ → (2nd𝑢) = 𝑦)
2726fveq2d 6669 . . . . . . . . 9 (𝑢 = ⟨𝑥, 𝑦⟩ → (𝐺‘(2nd𝑢)) = (𝐺𝑦))
2825, 27opeq12d 4805 . . . . . . . 8 (𝑢 = ⟨𝑥, 𝑦⟩ → ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩ = ⟨(𝐹𝑥), (𝐺𝑦)⟩)
2928mpompt 7260 . . . . . . 7 (𝑢 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩) = (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩)
3029eqcomi 2830 . . . . . 6 (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) = (𝑢 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩)
31 eqid 2821 . . . . . . . . . 10 𝐿 = 𝐿
326, 31cnf 21848 . . . . . . . . 9 (𝐹 ∈ (𝐽 Cn 𝐿) → 𝐹:𝑋 𝐿)
333, 32syl 17 . . . . . . . 8 (𝜑𝐹:𝑋 𝐿)
34 xp1st 7715 . . . . . . . 8 (𝑢 ∈ (𝑋 × 𝑌) → (1st𝑢) ∈ 𝑋)
35 ffvelrn 6844 . . . . . . . 8 ((𝐹:𝑋 𝐿 ∧ (1st𝑢) ∈ 𝑋) → (𝐹‘(1st𝑢)) ∈ 𝐿)
3633, 34, 35syl2an 597 . . . . . . 7 ((𝜑𝑢 ∈ (𝑋 × 𝑌)) → (𝐹‘(1st𝑢)) ∈ 𝐿)
37 eqid 2821 . . . . . . . . . 10 𝑀 = 𝑀
3814, 37cnf 21848 . . . . . . . . 9 (𝐺 ∈ (𝐾 Cn 𝑀) → 𝐺:𝑌 𝑀)
3911, 38syl 17 . . . . . . . 8 (𝜑𝐺:𝑌 𝑀)
40 xp2nd 7716 . . . . . . . 8 (𝑢 ∈ (𝑋 × 𝑌) → (2nd𝑢) ∈ 𝑌)
41 ffvelrn 6844 . . . . . . . 8 ((𝐺:𝑌 𝑀 ∧ (2nd𝑢) ∈ 𝑌) → (𝐺‘(2nd𝑢)) ∈ 𝑀)
4239, 40, 41syl2an 597 . . . . . . 7 ((𝜑𝑢 ∈ (𝑋 × 𝑌)) → (𝐺‘(2nd𝑢)) ∈ 𝑀)
4336, 42opelxpd 5588 . . . . . 6 ((𝜑𝑢 ∈ (𝑋 × 𝑌)) → ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩ ∈ ( 𝐿 × 𝑀))
446, 31hmeof1o 22366 . . . . . . . . . 10 (𝐹 ∈ (𝐽Homeo𝐿) → 𝐹:𝑋1-1-onto 𝐿)
451, 44syl 17 . . . . . . . . 9 (𝜑𝐹:𝑋1-1-onto 𝐿)
46 f1ocnv 6622 . . . . . . . . 9 (𝐹:𝑋1-1-onto 𝐿𝐹: 𝐿1-1-onto𝑋)
47 f1of 6610 . . . . . . . . 9 (𝐹: 𝐿1-1-onto𝑋𝐹: 𝐿𝑋)
4845, 46, 473syl 18 . . . . . . . 8 (𝜑𝐹: 𝐿𝑋)
49 xp1st 7715 . . . . . . . 8 (𝑣 ∈ ( 𝐿 × 𝑀) → (1st𝑣) ∈ 𝐿)
50 ffvelrn 6844 . . . . . . . 8 ((𝐹: 𝐿𝑋 ∧ (1st𝑣) ∈ 𝐿) → (𝐹‘(1st𝑣)) ∈ 𝑋)
5148, 49, 50syl2an 597 . . . . . . 7 ((𝜑𝑣 ∈ ( 𝐿 × 𝑀)) → (𝐹‘(1st𝑣)) ∈ 𝑋)
5214, 37hmeof1o 22366 . . . . . . . . . 10 (𝐺 ∈ (𝐾Homeo𝑀) → 𝐺:𝑌1-1-onto 𝑀)
539, 52syl 17 . . . . . . . . 9 (𝜑𝐺:𝑌1-1-onto 𝑀)
54 f1ocnv 6622 . . . . . . . . 9 (𝐺:𝑌1-1-onto 𝑀𝐺: 𝑀1-1-onto𝑌)
55 f1of 6610 . . . . . . . . 9 (𝐺: 𝑀1-1-onto𝑌𝐺: 𝑀𝑌)
5653, 54, 553syl 18 . . . . . . . 8 (𝜑𝐺: 𝑀𝑌)
57 xp2nd 7716 . . . . . . . 8 (𝑣 ∈ ( 𝐿 × 𝑀) → (2nd𝑣) ∈ 𝑀)
58 ffvelrn 6844 . . . . . . . 8 ((𝐺: 𝑀𝑌 ∧ (2nd𝑣) ∈ 𝑀) → (𝐺‘(2nd𝑣)) ∈ 𝑌)
5956, 57, 58syl2an 597 . . . . . . 7 ((𝜑𝑣 ∈ ( 𝐿 × 𝑀)) → (𝐺‘(2nd𝑣)) ∈ 𝑌)
6051, 59opelxpd 5588 . . . . . 6 ((𝜑𝑣 ∈ ( 𝐿 × 𝑀)) → ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ ∈ (𝑋 × 𝑌))
6145adantr 483 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → 𝐹:𝑋1-1-onto 𝐿)
6234ad2antrl 726 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (1st𝑢) ∈ 𝑋)
6349ad2antll 727 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (1st𝑣) ∈ 𝐿)
64 f1ocnvfvb 7030 . . . . . . . . . 10 ((𝐹:𝑋1-1-onto 𝐿 ∧ (1st𝑢) ∈ 𝑋 ∧ (1st𝑣) ∈ 𝐿) → ((𝐹‘(1st𝑢)) = (1st𝑣) ↔ (𝐹‘(1st𝑣)) = (1st𝑢)))
6561, 62, 63, 64syl3anc 1367 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → ((𝐹‘(1st𝑢)) = (1st𝑣) ↔ (𝐹‘(1st𝑣)) = (1st𝑢)))
66 eqcom 2828 . . . . . . . . 9 ((1st𝑣) = (𝐹‘(1st𝑢)) ↔ (𝐹‘(1st𝑢)) = (1st𝑣))
67 eqcom 2828 . . . . . . . . 9 ((1st𝑢) = (𝐹‘(1st𝑣)) ↔ (𝐹‘(1st𝑣)) = (1st𝑢))
6865, 66, 673bitr4g 316 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → ((1st𝑣) = (𝐹‘(1st𝑢)) ↔ (1st𝑢) = (𝐹‘(1st𝑣))))
6953adantr 483 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → 𝐺:𝑌1-1-onto 𝑀)
7040ad2antrl 726 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (2nd𝑢) ∈ 𝑌)
7157ad2antll 727 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (2nd𝑣) ∈ 𝑀)
72 f1ocnvfvb 7030 . . . . . . . . . 10 ((𝐺:𝑌1-1-onto 𝑀 ∧ (2nd𝑢) ∈ 𝑌 ∧ (2nd𝑣) ∈ 𝑀) → ((𝐺‘(2nd𝑢)) = (2nd𝑣) ↔ (𝐺‘(2nd𝑣)) = (2nd𝑢)))
7369, 70, 71, 72syl3anc 1367 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → ((𝐺‘(2nd𝑢)) = (2nd𝑣) ↔ (𝐺‘(2nd𝑣)) = (2nd𝑢)))
74 eqcom 2828 . . . . . . . . 9 ((2nd𝑣) = (𝐺‘(2nd𝑢)) ↔ (𝐺‘(2nd𝑢)) = (2nd𝑣))
75 eqcom 2828 . . . . . . . . 9 ((2nd𝑢) = (𝐺‘(2nd𝑣)) ↔ (𝐺‘(2nd𝑣)) = (2nd𝑢))
7673, 74, 753bitr4g 316 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → ((2nd𝑣) = (𝐺‘(2nd𝑢)) ↔ (2nd𝑢) = (𝐺‘(2nd𝑣))))
7768, 76anbi12d 632 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (((1st𝑣) = (𝐹‘(1st𝑢)) ∧ (2nd𝑣) = (𝐺‘(2nd𝑢))) ↔ ((1st𝑢) = (𝐹‘(1st𝑣)) ∧ (2nd𝑢) = (𝐺‘(2nd𝑣)))))
78 eqop 7725 . . . . . . . 8 (𝑣 ∈ ( 𝐿 × 𝑀) → (𝑣 = ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩ ↔ ((1st𝑣) = (𝐹‘(1st𝑢)) ∧ (2nd𝑣) = (𝐺‘(2nd𝑢)))))
7978ad2antll 727 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (𝑣 = ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩ ↔ ((1st𝑣) = (𝐹‘(1st𝑢)) ∧ (2nd𝑣) = (𝐺‘(2nd𝑢)))))
80 eqop 7725 . . . . . . . 8 (𝑢 ∈ (𝑋 × 𝑌) → (𝑢 = ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ ↔ ((1st𝑢) = (𝐹‘(1st𝑣)) ∧ (2nd𝑢) = (𝐺‘(2nd𝑣)))))
8180ad2antrl 726 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (𝑢 = ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ ↔ ((1st𝑢) = (𝐹‘(1st𝑣)) ∧ (2nd𝑢) = (𝐺‘(2nd𝑣)))))
8277, 79, 813bitr4rd 314 . . . . . 6 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (𝑢 = ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ ↔ 𝑣 = ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩))
8330, 43, 60, 82f1ocnv2d 7392 . . . . 5 (𝜑 → ((𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩):(𝑋 × 𝑌)–1-1-onto→( 𝐿 × 𝑀) ∧ (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) = (𝑣 ∈ ( 𝐿 × 𝑀) ↦ ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩)))
8483simprd 498 . . . 4 (𝜑(𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) = (𝑣 ∈ ( 𝐿 × 𝑀) ↦ ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩))
85 vex 3498 . . . . . . . 8 𝑧 ∈ V
86 vex 3498 . . . . . . . 8 𝑤 ∈ V
8785, 86op1std 7693 . . . . . . 7 (𝑣 = ⟨𝑧, 𝑤⟩ → (1st𝑣) = 𝑧)
8887fveq2d 6669 . . . . . 6 (𝑣 = ⟨𝑧, 𝑤⟩ → (𝐹‘(1st𝑣)) = (𝐹𝑧))
8985, 86op2ndd 7694 . . . . . . 7 (𝑣 = ⟨𝑧, 𝑤⟩ → (2nd𝑣) = 𝑤)
9089fveq2d 6669 . . . . . 6 (𝑣 = ⟨𝑧, 𝑤⟩ → (𝐺‘(2nd𝑣)) = (𝐺𝑤))
9188, 90opeq12d 4805 . . . . 5 (𝑣 = ⟨𝑧, 𝑤⟩ → ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ = ⟨(𝐹𝑧), (𝐺𝑤)⟩)
9291mpompt 7260 . . . 4 (𝑣 ∈ ( 𝐿 × 𝑀) ↦ ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩) = (𝑧 𝐿, 𝑤 𝑀 ↦ ⟨(𝐹𝑧), (𝐺𝑤)⟩)
9384, 92syl6eq 2872 . . 3 (𝜑(𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) = (𝑧 𝐿, 𝑤 𝑀 ↦ ⟨(𝐹𝑧), (𝐺𝑤)⟩))
94 cntop2 21843 . . . . . 6 (𝐹 ∈ (𝐽 Cn 𝐿) → 𝐿 ∈ Top)
953, 94syl 17 . . . . 5 (𝜑𝐿 ∈ Top)
9631toptopon 21519 . . . . 5 (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘ 𝐿))
9795, 96sylib 220 . . . 4 (𝜑𝐿 ∈ (TopOn‘ 𝐿))
98 cntop2 21843 . . . . . 6 (𝐺 ∈ (𝐾 Cn 𝑀) → 𝑀 ∈ Top)
9911, 98syl 17 . . . . 5 (𝜑𝑀 ∈ Top)
10037toptopon 21519 . . . . 5 (𝑀 ∈ Top ↔ 𝑀 ∈ (TopOn‘ 𝑀))
10199, 100sylib 220 . . . 4 (𝜑𝑀 ∈ (TopOn‘ 𝑀))
10297, 101cnmpt1st 22270 . . . . 5 (𝜑 → (𝑧 𝐿, 𝑤 𝑀𝑧) ∈ ((𝐿 ×t 𝑀) Cn 𝐿))
103 hmeocnvcn 22363 . . . . . 6 (𝐹 ∈ (𝐽Homeo𝐿) → 𝐹 ∈ (𝐿 Cn 𝐽))
1041, 103syl 17 . . . . 5 (𝜑𝐹 ∈ (𝐿 Cn 𝐽))
10597, 101, 102, 104cnmpt21f 22274 . . . 4 (𝜑 → (𝑧 𝐿, 𝑤 𝑀 ↦ (𝐹𝑧)) ∈ ((𝐿 ×t 𝑀) Cn 𝐽))
10697, 101cnmpt2nd 22271 . . . . 5 (𝜑 → (𝑧 𝐿, 𝑤 𝑀𝑤) ∈ ((𝐿 ×t 𝑀) Cn 𝑀))
107 hmeocnvcn 22363 . . . . . 6 (𝐺 ∈ (𝐾Homeo𝑀) → 𝐺 ∈ (𝑀 Cn 𝐾))
1089, 107syl 17 . . . . 5 (𝜑𝐺 ∈ (𝑀 Cn 𝐾))
10997, 101, 106, 108cnmpt21f 22274 . . . 4 (𝜑 → (𝑧 𝐿, 𝑤 𝑀 ↦ (𝐺𝑤)) ∈ ((𝐿 ×t 𝑀) Cn 𝐾))
11097, 101, 105, 109cnmpt2t 22275 . . 3 (𝜑 → (𝑧 𝐿, 𝑤 𝑀 ↦ ⟨(𝐹𝑧), (𝐺𝑤)⟩) ∈ ((𝐿 ×t 𝑀) Cn (𝐽 ×t 𝐾)))
11193, 110eqeltrd 2913 . 2 (𝜑(𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐿 ×t 𝑀) Cn (𝐽 ×t 𝐾)))
112 ishmeo 22361 . 2 ((𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐽 ×t 𝐾)Homeo(𝐿 ×t 𝑀)) ↔ ((𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐽 ×t 𝐾) Cn (𝐿 ×t 𝑀)) ∧ (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐿 ×t 𝑀) Cn (𝐽 ×t 𝐾))))
11321, 111, 112sylanbrc 585 1 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐽 ×t 𝐾)Homeo(𝐿 ×t 𝑀)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398   = wceq 1533  wcel 2110  cop 4567   cuni 4832  cmpt 5139   × cxp 5548  ccnv 5549  wf 6346  1-1-ontowf1o 6349  cfv 6350  (class class class)co 7150  cmpo 7152  1st c1st 7681  2nd c2nd 7682  Topctop 21495  TopOnctopon 21512   Cn ccn 21826   ×t ctx 22162  Homeochmeo 22355
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-iun 4914  df-br 5060  df-opab 5122  df-mpt 5140  df-id 5455  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-ov 7153  df-oprab 7154  df-mpo 7155  df-1st 7683  df-2nd 7684  df-map 8402  df-topgen 16711  df-top 21496  df-topon 21513  df-bases 21548  df-cn 21829  df-tx 22164  df-hmeo 22357
This theorem is referenced by:  xpstopnlem1  22411
  Copyright terms: Public domain W3C validator