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

Theorem txhmeo 13078
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 13064 . . . . . 6 (𝐹 ∈ (𝐽Homeo𝐿) → 𝐹 ∈ (𝐽 Cn 𝐿))
31, 2syl 14 . . . . 5 (𝜑𝐹 ∈ (𝐽 Cn 𝐿))
4 cntop1 12960 . . . . 5 (𝐹 ∈ (𝐽 Cn 𝐿) → 𝐽 ∈ Top)
53, 4syl 14 . . . 4 (𝜑𝐽 ∈ Top)
6 txhmeo.1 . . . . 5 𝑋 = 𝐽
76toptopon 12775 . . . 4 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
85, 7sylib 121 . . 3 (𝜑𝐽 ∈ (TopOn‘𝑋))
9 txhmeo.4 . . . . . 6 (𝜑𝐺 ∈ (𝐾Homeo𝑀))
10 hmeocn 13064 . . . . . 6 (𝐺 ∈ (𝐾Homeo𝑀) → 𝐺 ∈ (𝐾 Cn 𝑀))
119, 10syl 14 . . . . 5 (𝜑𝐺 ∈ (𝐾 Cn 𝑀))
12 cntop1 12960 . . . . 5 (𝐺 ∈ (𝐾 Cn 𝑀) → 𝐾 ∈ Top)
1311, 12syl 14 . . . 4 (𝜑𝐾 ∈ Top)
14 txhmeo.2 . . . . 5 𝑌 = 𝐾
1514toptopon 12775 . . . 4 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌))
1613, 15sylib 121 . . 3 (𝜑𝐾 ∈ (TopOn‘𝑌))
178, 16cnmpt1st 13047 . . . 4 (𝜑 → (𝑥𝑋, 𝑦𝑌𝑥) ∈ ((𝐽 ×t 𝐾) Cn 𝐽))
188, 16, 17, 3cnmpt21f 13051 . . 3 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ (𝐹𝑥)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
198, 16cnmpt2nd 13048 . . . 4 (𝜑 → (𝑥𝑋, 𝑦𝑌𝑦) ∈ ((𝐽 ×t 𝐾) Cn 𝐾))
208, 16, 19, 11cnmpt21f 13051 . . 3 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ (𝐺𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝑀))
218, 16, 18, 20cnmpt2t 13052 . 2 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐽 ×t 𝐾) Cn (𝐿 ×t 𝑀)))
22 vex 2733 . . . . . . . . . . 11 𝑥 ∈ V
23 vex 2733 . . . . . . . . . . 11 𝑦 ∈ V
2422, 23op1std 6125 . . . . . . . . . 10 (𝑢 = ⟨𝑥, 𝑦⟩ → (1st𝑢) = 𝑥)
2524fveq2d 5498 . . . . . . . . 9 (𝑢 = ⟨𝑥, 𝑦⟩ → (𝐹‘(1st𝑢)) = (𝐹𝑥))
2622, 23op2ndd 6126 . . . . . . . . . 10 (𝑢 = ⟨𝑥, 𝑦⟩ → (2nd𝑢) = 𝑦)
2726fveq2d 5498 . . . . . . . . 9 (𝑢 = ⟨𝑥, 𝑦⟩ → (𝐺‘(2nd𝑢)) = (𝐺𝑦))
2825, 27opeq12d 3771 . . . . . . . 8 (𝑢 = ⟨𝑥, 𝑦⟩ → ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩ = ⟨(𝐹𝑥), (𝐺𝑦)⟩)
2928mpompt 5943 . . . . . . 7 (𝑢 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩) = (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩)
3029eqcomi 2174 . . . . . 6 (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) = (𝑢 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩)
31 eqid 2170 . . . . . . . . . 10 𝐿 = 𝐿
326, 31cnf 12963 . . . . . . . . 9 (𝐹 ∈ (𝐽 Cn 𝐿) → 𝐹:𝑋 𝐿)
333, 32syl 14 . . . . . . . 8 (𝜑𝐹:𝑋 𝐿)
34 xp1st 6142 . . . . . . . 8 (𝑢 ∈ (𝑋 × 𝑌) → (1st𝑢) ∈ 𝑋)
35 ffvelrn 5627 . . . . . . . 8 ((𝐹:𝑋 𝐿 ∧ (1st𝑢) ∈ 𝑋) → (𝐹‘(1st𝑢)) ∈ 𝐿)
3633, 34, 35syl2an 287 . . . . . . 7 ((𝜑𝑢 ∈ (𝑋 × 𝑌)) → (𝐹‘(1st𝑢)) ∈ 𝐿)
37 eqid 2170 . . . . . . . . . 10 𝑀 = 𝑀
3814, 37cnf 12963 . . . . . . . . 9 (𝐺 ∈ (𝐾 Cn 𝑀) → 𝐺:𝑌 𝑀)
3911, 38syl 14 . . . . . . . 8 (𝜑𝐺:𝑌 𝑀)
40 xp2nd 6143 . . . . . . . 8 (𝑢 ∈ (𝑋 × 𝑌) → (2nd𝑢) ∈ 𝑌)
41 ffvelrn 5627 . . . . . . . 8 ((𝐺:𝑌 𝑀 ∧ (2nd𝑢) ∈ 𝑌) → (𝐺‘(2nd𝑢)) ∈ 𝑀)
4239, 40, 41syl2an 287 . . . . . . 7 ((𝜑𝑢 ∈ (𝑋 × 𝑌)) → (𝐺‘(2nd𝑢)) ∈ 𝑀)
4336, 42opelxpd 4642 . . . . . 6 ((𝜑𝑢 ∈ (𝑋 × 𝑌)) → ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩ ∈ ( 𝐿 × 𝑀))
446, 31hmeof1o 13068 . . . . . . . . . 10 (𝐹 ∈ (𝐽Homeo𝐿) → 𝐹:𝑋1-1-onto 𝐿)
451, 44syl 14 . . . . . . . . 9 (𝜑𝐹:𝑋1-1-onto 𝐿)
46 f1ocnv 5453 . . . . . . . . 9 (𝐹:𝑋1-1-onto 𝐿𝐹: 𝐿1-1-onto𝑋)
47 f1of 5440 . . . . . . . . 9 (𝐹: 𝐿1-1-onto𝑋𝐹: 𝐿𝑋)
4845, 46, 473syl 17 . . . . . . . 8 (𝜑𝐹: 𝐿𝑋)
49 xp1st 6142 . . . . . . . 8 (𝑣 ∈ ( 𝐿 × 𝑀) → (1st𝑣) ∈ 𝐿)
50 ffvelrn 5627 . . . . . . . 8 ((𝐹: 𝐿𝑋 ∧ (1st𝑣) ∈ 𝐿) → (𝐹‘(1st𝑣)) ∈ 𝑋)
5148, 49, 50syl2an 287 . . . . . . 7 ((𝜑𝑣 ∈ ( 𝐿 × 𝑀)) → (𝐹‘(1st𝑣)) ∈ 𝑋)
5214, 37hmeof1o 13068 . . . . . . . . . 10 (𝐺 ∈ (𝐾Homeo𝑀) → 𝐺:𝑌1-1-onto 𝑀)
539, 52syl 14 . . . . . . . . 9 (𝜑𝐺:𝑌1-1-onto 𝑀)
54 f1ocnv 5453 . . . . . . . . 9 (𝐺:𝑌1-1-onto 𝑀𝐺: 𝑀1-1-onto𝑌)
55 f1of 5440 . . . . . . . . 9 (𝐺: 𝑀1-1-onto𝑌𝐺: 𝑀𝑌)
5653, 54, 553syl 17 . . . . . . . 8 (𝜑𝐺: 𝑀𝑌)
57 xp2nd 6143 . . . . . . . 8 (𝑣 ∈ ( 𝐿 × 𝑀) → (2nd𝑣) ∈ 𝑀)
58 ffvelrn 5627 . . . . . . . 8 ((𝐺: 𝑀𝑌 ∧ (2nd𝑣) ∈ 𝑀) → (𝐺‘(2nd𝑣)) ∈ 𝑌)
5956, 57, 58syl2an 287 . . . . . . 7 ((𝜑𝑣 ∈ ( 𝐿 × 𝑀)) → (𝐺‘(2nd𝑣)) ∈ 𝑌)
6051, 59opelxpd 4642 . . . . . 6 ((𝜑𝑣 ∈ ( 𝐿 × 𝑀)) → ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ ∈ (𝑋 × 𝑌))
6145adantr 274 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → 𝐹:𝑋1-1-onto 𝐿)
6234ad2antrl 487 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (1st𝑢) ∈ 𝑋)
6349ad2antll 488 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (1st𝑣) ∈ 𝐿)
64 f1ocnvfvb 5757 . . . . . . . . . 10 ((𝐹:𝑋1-1-onto 𝐿 ∧ (1st𝑢) ∈ 𝑋 ∧ (1st𝑣) ∈ 𝐿) → ((𝐹‘(1st𝑢)) = (1st𝑣) ↔ (𝐹‘(1st𝑣)) = (1st𝑢)))
6561, 62, 63, 64syl3anc 1233 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → ((𝐹‘(1st𝑢)) = (1st𝑣) ↔ (𝐹‘(1st𝑣)) = (1st𝑢)))
66 eqcom 2172 . . . . . . . . 9 ((1st𝑣) = (𝐹‘(1st𝑢)) ↔ (𝐹‘(1st𝑢)) = (1st𝑣))
67 eqcom 2172 . . . . . . . . 9 ((1st𝑢) = (𝐹‘(1st𝑣)) ↔ (𝐹‘(1st𝑣)) = (1st𝑢))
6865, 66, 673bitr4g 222 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → ((1st𝑣) = (𝐹‘(1st𝑢)) ↔ (1st𝑢) = (𝐹‘(1st𝑣))))
6953adantr 274 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → 𝐺:𝑌1-1-onto 𝑀)
7040ad2antrl 487 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (2nd𝑢) ∈ 𝑌)
7157ad2antll 488 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (2nd𝑣) ∈ 𝑀)
72 f1ocnvfvb 5757 . . . . . . . . . 10 ((𝐺:𝑌1-1-onto 𝑀 ∧ (2nd𝑢) ∈ 𝑌 ∧ (2nd𝑣) ∈ 𝑀) → ((𝐺‘(2nd𝑢)) = (2nd𝑣) ↔ (𝐺‘(2nd𝑣)) = (2nd𝑢)))
7369, 70, 71, 72syl3anc 1233 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → ((𝐺‘(2nd𝑢)) = (2nd𝑣) ↔ (𝐺‘(2nd𝑣)) = (2nd𝑢)))
74 eqcom 2172 . . . . . . . . 9 ((2nd𝑣) = (𝐺‘(2nd𝑢)) ↔ (𝐺‘(2nd𝑢)) = (2nd𝑣))
75 eqcom 2172 . . . . . . . . 9 ((2nd𝑢) = (𝐺‘(2nd𝑣)) ↔ (𝐺‘(2nd𝑣)) = (2nd𝑢))
7673, 74, 753bitr4g 222 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → ((2nd𝑣) = (𝐺‘(2nd𝑢)) ↔ (2nd𝑢) = (𝐺‘(2nd𝑣))))
7768, 76anbi12d 470 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (((1st𝑣) = (𝐹‘(1st𝑢)) ∧ (2nd𝑣) = (𝐺‘(2nd𝑢))) ↔ ((1st𝑢) = (𝐹‘(1st𝑣)) ∧ (2nd𝑢) = (𝐺‘(2nd𝑣)))))
78 eqop 6154 . . . . . . . 8 (𝑣 ∈ ( 𝐿 × 𝑀) → (𝑣 = ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩ ↔ ((1st𝑣) = (𝐹‘(1st𝑢)) ∧ (2nd𝑣) = (𝐺‘(2nd𝑢)))))
7978ad2antll 488 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (𝑣 = ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩ ↔ ((1st𝑣) = (𝐹‘(1st𝑢)) ∧ (2nd𝑣) = (𝐺‘(2nd𝑢)))))
80 eqop 6154 . . . . . . . 8 (𝑢 ∈ (𝑋 × 𝑌) → (𝑢 = ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ ↔ ((1st𝑢) = (𝐹‘(1st𝑣)) ∧ (2nd𝑢) = (𝐺‘(2nd𝑣)))))
8180ad2antrl 487 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (𝑢 = ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ ↔ ((1st𝑢) = (𝐹‘(1st𝑣)) ∧ (2nd𝑢) = (𝐺‘(2nd𝑣)))))
8277, 79, 813bitr4rd 220 . . . . . 6 ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ ( 𝐿 × 𝑀))) → (𝑢 = ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ ↔ 𝑣 = ⟨(𝐹‘(1st𝑢)), (𝐺‘(2nd𝑢))⟩))
8330, 43, 60, 82f1ocnv2d 6051 . . . . 5 (𝜑 → ((𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩):(𝑋 × 𝑌)–1-1-onto→( 𝐿 × 𝑀) ∧ (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) = (𝑣 ∈ ( 𝐿 × 𝑀) ↦ ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩)))
8483simprd 113 . . . 4 (𝜑(𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) = (𝑣 ∈ ( 𝐿 × 𝑀) ↦ ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩))
85 vex 2733 . . . . . . . 8 𝑧 ∈ V
86 vex 2733 . . . . . . . 8 𝑤 ∈ V
8785, 86op1std 6125 . . . . . . 7 (𝑣 = ⟨𝑧, 𝑤⟩ → (1st𝑣) = 𝑧)
8887fveq2d 5498 . . . . . 6 (𝑣 = ⟨𝑧, 𝑤⟩ → (𝐹‘(1st𝑣)) = (𝐹𝑧))
8985, 86op2ndd 6126 . . . . . . 7 (𝑣 = ⟨𝑧, 𝑤⟩ → (2nd𝑣) = 𝑤)
9089fveq2d 5498 . . . . . 6 (𝑣 = ⟨𝑧, 𝑤⟩ → (𝐺‘(2nd𝑣)) = (𝐺𝑤))
9188, 90opeq12d 3771 . . . . 5 (𝑣 = ⟨𝑧, 𝑤⟩ → ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩ = ⟨(𝐹𝑧), (𝐺𝑤)⟩)
9291mpompt 5943 . . . 4 (𝑣 ∈ ( 𝐿 × 𝑀) ↦ ⟨(𝐹‘(1st𝑣)), (𝐺‘(2nd𝑣))⟩) = (𝑧 𝐿, 𝑤 𝑀 ↦ ⟨(𝐹𝑧), (𝐺𝑤)⟩)
9384, 92eqtrdi 2219 . . 3 (𝜑(𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) = (𝑧 𝐿, 𝑤 𝑀 ↦ ⟨(𝐹𝑧), (𝐺𝑤)⟩))
94 cntop2 12961 . . . . . 6 (𝐹 ∈ (𝐽 Cn 𝐿) → 𝐿 ∈ Top)
953, 94syl 14 . . . . 5 (𝜑𝐿 ∈ Top)
9631toptopon 12775 . . . . 5 (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘ 𝐿))
9795, 96sylib 121 . . . 4 (𝜑𝐿 ∈ (TopOn‘ 𝐿))
98 cntop2 12961 . . . . . 6 (𝐺 ∈ (𝐾 Cn 𝑀) → 𝑀 ∈ Top)
9911, 98syl 14 . . . . 5 (𝜑𝑀 ∈ Top)
10037toptopon 12775 . . . . 5 (𝑀 ∈ Top ↔ 𝑀 ∈ (TopOn‘ 𝑀))
10199, 100sylib 121 . . . 4 (𝜑𝑀 ∈ (TopOn‘ 𝑀))
10297, 101cnmpt1st 13047 . . . . 5 (𝜑 → (𝑧 𝐿, 𝑤 𝑀𝑧) ∈ ((𝐿 ×t 𝑀) Cn 𝐿))
103 hmeocnvcn 13065 . . . . . 6 (𝐹 ∈ (𝐽Homeo𝐿) → 𝐹 ∈ (𝐿 Cn 𝐽))
1041, 103syl 14 . . . . 5 (𝜑𝐹 ∈ (𝐿 Cn 𝐽))
10597, 101, 102, 104cnmpt21f 13051 . . . 4 (𝜑 → (𝑧 𝐿, 𝑤 𝑀 ↦ (𝐹𝑧)) ∈ ((𝐿 ×t 𝑀) Cn 𝐽))
10697, 101cnmpt2nd 13048 . . . . 5 (𝜑 → (𝑧 𝐿, 𝑤 𝑀𝑤) ∈ ((𝐿 ×t 𝑀) Cn 𝑀))
107 hmeocnvcn 13065 . . . . . 6 (𝐺 ∈ (𝐾Homeo𝑀) → 𝐺 ∈ (𝑀 Cn 𝐾))
1089, 107syl 14 . . . . 5 (𝜑𝐺 ∈ (𝑀 Cn 𝐾))
10997, 101, 106, 108cnmpt21f 13051 . . . 4 (𝜑 → (𝑧 𝐿, 𝑤 𝑀 ↦ (𝐺𝑤)) ∈ ((𝐿 ×t 𝑀) Cn 𝐾))
11097, 101, 105, 109cnmpt2t 13052 . . 3 (𝜑 → (𝑧 𝐿, 𝑤 𝑀 ↦ ⟨(𝐹𝑧), (𝐺𝑤)⟩) ∈ ((𝐿 ×t 𝑀) Cn (𝐽 ×t 𝐾)))
11193, 110eqeltrd 2247 . 2 (𝜑(𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐿 ×t 𝑀) Cn (𝐽 ×t 𝐾)))
112 ishmeo 13063 . 2 ((𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐽 ×t 𝐾)Homeo(𝐿 ×t 𝑀)) ↔ ((𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐽 ×t 𝐾) Cn (𝐿 ×t 𝑀)) ∧ (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐿 ×t 𝑀) Cn (𝐽 ×t 𝐾))))
11321, 111, 112sylanbrc 415 1 (𝜑 → (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) ∈ ((𝐽 ×t 𝐾)Homeo(𝐿 ×t 𝑀)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104   = wceq 1348  wcel 2141  cop 3584   cuni 3794  cmpt 4048   × cxp 4607  ccnv 4608  wf 5192  1-1-ontowf1o 5195  cfv 5196  (class class class)co 5851  cmpo 5853  1st c1st 6115  2nd c2nd 6116  Topctop 12754  TopOnctopon 12767   Cn ccn 12944   ×t ctx 13011  Homeochmeo 13059
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 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4102  ax-sep 4105  ax-pow 4158  ax-pr 4192  ax-un 4416  ax-setind 4519
This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-pw 3566  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-iun 3873  df-br 3988  df-opab 4049  df-mpt 4050  df-id 4276  df-xp 4615  df-rel 4616  df-cnv 4617  df-co 4618  df-dm 4619  df-rn 4620  df-res 4621  df-ima 4622  df-iota 5158  df-fun 5198  df-fn 5199  df-f 5200  df-f1 5201  df-fo 5202  df-f1o 5203  df-fv 5204  df-ov 5854  df-oprab 5855  df-mpo 5856  df-1st 6117  df-2nd 6118  df-map 6626  df-topgen 12593  df-top 12755  df-topon 12768  df-bases 12800  df-cn 12947  df-tx 13012  df-hmeo 13060
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator