Step | Hyp | Ref
| Expression |
1 | | txhmeo.3 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝐽Homeo𝐿)) |
2 | | hmeocn 13064 |
. . . . . 6
⊢ (𝐹 ∈ (𝐽Homeo𝐿) → 𝐹 ∈ (𝐽 Cn 𝐿)) |
3 | 1, 2 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐿)) |
4 | | cntop1 12960 |
. . . . 5
⊢ (𝐹 ∈ (𝐽 Cn 𝐿) → 𝐽 ∈ Top) |
5 | 3, 4 | syl 14 |
. . . 4
⊢ (𝜑 → 𝐽 ∈ Top) |
6 | | txhmeo.1 |
. . . . 5
⊢ 𝑋 = ∪
𝐽 |
7 | 6 | toptopon 12775 |
. . . 4
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
8 | 5, 7 | sylib 121 |
. . 3
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
9 | | txhmeo.4 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ (𝐾Homeo𝑀)) |
10 | | hmeocn 13064 |
. . . . . 6
⊢ (𝐺 ∈ (𝐾Homeo𝑀) → 𝐺 ∈ (𝐾 Cn 𝑀)) |
11 | 9, 10 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝑀)) |
12 | | cntop1 12960 |
. . . . 5
⊢ (𝐺 ∈ (𝐾 Cn 𝑀) → 𝐾 ∈ Top) |
13 | 11, 12 | syl 14 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ Top) |
14 | | txhmeo.2 |
. . . . 5
⊢ 𝑌 = ∪
𝐾 |
15 | 14 | toptopon 12775 |
. . . 4
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌)) |
16 | 13, 15 | sylib 121 |
. . 3
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
17 | 8, 16 | cnmpt1st 13047 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑥) ∈ ((𝐽 ×t 𝐾) Cn 𝐽)) |
18 | 8, 16, 17, 3 | cnmpt21f 13051 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐹‘𝑥)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) |
19 | 8, 16 | cnmpt2nd 13048 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑦) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) |
20 | 8, 16, 19, 11 | cnmpt21f 13051 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐺‘𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝑀)) |
21 | 8, 16, 18, 20 | cnmpt2t 13052 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) ∈ ((𝐽 ×t 𝐾) Cn (𝐿 ×t 𝑀))) |
22 | | vex 2733 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
23 | | vex 2733 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
24 | 22, 23 | op1std 6125 |
. . . . . . . . . 10
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (1st ‘𝑢) = 𝑥) |
25 | 24 | fveq2d 5498 |
. . . . . . . . 9
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (𝐹‘(1st ‘𝑢)) = (𝐹‘𝑥)) |
26 | 22, 23 | op2ndd 6126 |
. . . . . . . . . 10
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (2nd ‘𝑢) = 𝑦) |
27 | 26 | fveq2d 5498 |
. . . . . . . . 9
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (𝐺‘(2nd ‘𝑢)) = (𝐺‘𝑦)) |
28 | 25, 27 | opeq12d 3771 |
. . . . . . . 8
⊢ (𝑢 = 〈𝑥, 𝑦〉 → 〈(𝐹‘(1st ‘𝑢)), (𝐺‘(2nd ‘𝑢))〉 = 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) |
29 | 28 | mpompt 5943 |
. . . . . . 7
⊢ (𝑢 ∈ (𝑋 × 𝑌) ↦ 〈(𝐹‘(1st ‘𝑢)), (𝐺‘(2nd ‘𝑢))〉) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) |
30 | 29 | eqcomi 2174 |
. . . . . 6
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) = (𝑢 ∈ (𝑋 × 𝑌) ↦ 〈(𝐹‘(1st ‘𝑢)), (𝐺‘(2nd ‘𝑢))〉) |
31 | | eqid 2170 |
. . . . . . . . . 10
⊢ ∪ 𝐿 =
∪ 𝐿 |
32 | 6, 31 | cnf 12963 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝐽 Cn 𝐿) → 𝐹:𝑋⟶∪ 𝐿) |
33 | 3, 32 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝑋⟶∪ 𝐿) |
34 | | xp1st 6142 |
. . . . . . . 8
⊢ (𝑢 ∈ (𝑋 × 𝑌) → (1st ‘𝑢) ∈ 𝑋) |
35 | | ffvelrn 5627 |
. . . . . . . 8
⊢ ((𝐹:𝑋⟶∪ 𝐿 ∧ (1st
‘𝑢) ∈ 𝑋) → (𝐹‘(1st ‘𝑢)) ∈ ∪ 𝐿) |
36 | 33, 34, 35 | syl2an 287 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑋 × 𝑌)) → (𝐹‘(1st ‘𝑢)) ∈ ∪ 𝐿) |
37 | | eqid 2170 |
. . . . . . . . . 10
⊢ ∪ 𝑀 =
∪ 𝑀 |
38 | 14, 37 | cnf 12963 |
. . . . . . . . 9
⊢ (𝐺 ∈ (𝐾 Cn 𝑀) → 𝐺:𝑌⟶∪ 𝑀) |
39 | 11, 38 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:𝑌⟶∪ 𝑀) |
40 | | xp2nd 6143 |
. . . . . . . 8
⊢ (𝑢 ∈ (𝑋 × 𝑌) → (2nd ‘𝑢) ∈ 𝑌) |
41 | | ffvelrn 5627 |
. . . . . . . 8
⊢ ((𝐺:𝑌⟶∪ 𝑀 ∧ (2nd
‘𝑢) ∈ 𝑌) → (𝐺‘(2nd ‘𝑢)) ∈ ∪ 𝑀) |
42 | 39, 40, 41 | syl2an 287 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑋 × 𝑌)) → (𝐺‘(2nd ‘𝑢)) ∈ ∪ 𝑀) |
43 | 36, 42 | opelxpd 4642 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑋 × 𝑌)) → 〈(𝐹‘(1st ‘𝑢)), (𝐺‘(2nd ‘𝑢))〉 ∈ (∪ 𝐿
× ∪ 𝑀)) |
44 | 6, 31 | hmeof1o 13068 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝐽Homeo𝐿) → 𝐹:𝑋–1-1-onto→∪ 𝐿) |
45 | 1, 44 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑋–1-1-onto→∪ 𝐿) |
46 | | f1ocnv 5453 |
. . . . . . . . 9
⊢ (𝐹:𝑋–1-1-onto→∪ 𝐿
→ ◡𝐹:∪ 𝐿–1-1-onto→𝑋) |
47 | | f1of 5440 |
. . . . . . . . 9
⊢ (◡𝐹:∪ 𝐿–1-1-onto→𝑋 → ◡𝐹:∪ 𝐿⟶𝑋) |
48 | 45, 46, 47 | 3syl 17 |
. . . . . . . 8
⊢ (𝜑 → ◡𝐹:∪ 𝐿⟶𝑋) |
49 | | xp1st 6142 |
. . . . . . . 8
⊢ (𝑣 ∈ (∪ 𝐿
× ∪ 𝑀) → (1st ‘𝑣) ∈ ∪ 𝐿) |
50 | | ffvelrn 5627 |
. . . . . . . 8
⊢ ((◡𝐹:∪ 𝐿⟶𝑋 ∧ (1st ‘𝑣) ∈ ∪ 𝐿)
→ (◡𝐹‘(1st ‘𝑣)) ∈ 𝑋) |
51 | 48, 49, 50 | syl2an 287 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀))
→ (◡𝐹‘(1st ‘𝑣)) ∈ 𝑋) |
52 | 14, 37 | hmeof1o 13068 |
. . . . . . . . . 10
⊢ (𝐺 ∈ (𝐾Homeo𝑀) → 𝐺:𝑌–1-1-onto→∪ 𝑀) |
53 | 9, 52 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:𝑌–1-1-onto→∪ 𝑀) |
54 | | f1ocnv 5453 |
. . . . . . . . 9
⊢ (𝐺:𝑌–1-1-onto→∪ 𝑀
→ ◡𝐺:∪ 𝑀–1-1-onto→𝑌) |
55 | | f1of 5440 |
. . . . . . . . 9
⊢ (◡𝐺:∪ 𝑀–1-1-onto→𝑌 → ◡𝐺:∪ 𝑀⟶𝑌) |
56 | 53, 54, 55 | 3syl 17 |
. . . . . . . 8
⊢ (𝜑 → ◡𝐺:∪ 𝑀⟶𝑌) |
57 | | xp2nd 6143 |
. . . . . . . 8
⊢ (𝑣 ∈ (∪ 𝐿
× ∪ 𝑀) → (2nd ‘𝑣) ∈ ∪ 𝑀) |
58 | | ffvelrn 5627 |
. . . . . . . 8
⊢ ((◡𝐺:∪ 𝑀⟶𝑌 ∧ (2nd ‘𝑣) ∈ ∪ 𝑀)
→ (◡𝐺‘(2nd ‘𝑣)) ∈ 𝑌) |
59 | 56, 57, 58 | syl2an 287 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀))
→ (◡𝐺‘(2nd ‘𝑣)) ∈ 𝑌) |
60 | 51, 59 | opelxpd 4642 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀))
→ 〈(◡𝐹‘(1st ‘𝑣)), (◡𝐺‘(2nd ‘𝑣))〉 ∈ (𝑋 × 𝑌)) |
61 | 45 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ 𝐹:𝑋–1-1-onto→∪ 𝐿) |
62 | 34 | ad2antrl 487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ (1st ‘𝑢) ∈ 𝑋) |
63 | 49 | ad2antll 488 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ (1st ‘𝑣) ∈ ∪ 𝐿) |
64 | | f1ocnvfvb 5757 |
. . . . . . . . . 10
⊢ ((𝐹:𝑋–1-1-onto→∪ 𝐿
∧ (1st ‘𝑢) ∈ 𝑋 ∧ (1st ‘𝑣) ∈ ∪ 𝐿)
→ ((𝐹‘(1st ‘𝑢)) = (1st
‘𝑣) ↔ (◡𝐹‘(1st ‘𝑣)) = (1st
‘𝑢))) |
65 | 61, 62, 63, 64 | syl3anc 1233 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ ((𝐹‘(1st ‘𝑢)) = (1st
‘𝑣) ↔ (◡𝐹‘(1st ‘𝑣)) = (1st
‘𝑢))) |
66 | | eqcom 2172 |
. . . . . . . . 9
⊢
((1st ‘𝑣) = (𝐹‘(1st ‘𝑢)) ↔ (𝐹‘(1st ‘𝑢)) = (1st
‘𝑣)) |
67 | | eqcom 2172 |
. . . . . . . . 9
⊢
((1st ‘𝑢) = (◡𝐹‘(1st ‘𝑣)) ↔ (◡𝐹‘(1st ‘𝑣)) = (1st
‘𝑢)) |
68 | 65, 66, 67 | 3bitr4g 222 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ ((1st ‘𝑣) = (𝐹‘(1st ‘𝑢)) ↔ (1st
‘𝑢) = (◡𝐹‘(1st ‘𝑣)))) |
69 | 53 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ 𝐺:𝑌–1-1-onto→∪ 𝑀) |
70 | 40 | ad2antrl 487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ (2nd ‘𝑢) ∈ 𝑌) |
71 | 57 | ad2antll 488 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ (2nd ‘𝑣) ∈ ∪ 𝑀) |
72 | | f1ocnvfvb 5757 |
. . . . . . . . . 10
⊢ ((𝐺:𝑌–1-1-onto→∪ 𝑀
∧ (2nd ‘𝑢) ∈ 𝑌 ∧ (2nd ‘𝑣) ∈ ∪ 𝑀)
→ ((𝐺‘(2nd ‘𝑢)) = (2nd
‘𝑣) ↔ (◡𝐺‘(2nd ‘𝑣)) = (2nd
‘𝑢))) |
73 | 69, 70, 71, 72 | syl3anc 1233 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ ((𝐺‘(2nd ‘𝑢)) = (2nd
‘𝑣) ↔ (◡𝐺‘(2nd ‘𝑣)) = (2nd
‘𝑢))) |
74 | | eqcom 2172 |
. . . . . . . . 9
⊢
((2nd ‘𝑣) = (𝐺‘(2nd ‘𝑢)) ↔ (𝐺‘(2nd ‘𝑢)) = (2nd
‘𝑣)) |
75 | | eqcom 2172 |
. . . . . . . . 9
⊢
((2nd ‘𝑢) = (◡𝐺‘(2nd ‘𝑣)) ↔ (◡𝐺‘(2nd ‘𝑣)) = (2nd
‘𝑢)) |
76 | 73, 74, 75 | 3bitr4g 222 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ ((2nd ‘𝑣) = (𝐺‘(2nd ‘𝑢)) ↔ (2nd
‘𝑢) = (◡𝐺‘(2nd ‘𝑣)))) |
77 | 68, 76 | anbi12d 470 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ (((1st ‘𝑣) = (𝐹‘(1st ‘𝑢)) ∧ (2nd
‘𝑣) = (𝐺‘(2nd
‘𝑢))) ↔
((1st ‘𝑢)
= (◡𝐹‘(1st ‘𝑣)) ∧ (2nd
‘𝑢) = (◡𝐺‘(2nd ‘𝑣))))) |
78 | | eqop 6154 |
. . . . . . . 8
⊢ (𝑣 ∈ (∪ 𝐿
× ∪ 𝑀) → (𝑣 = 〈(𝐹‘(1st ‘𝑢)), (𝐺‘(2nd ‘𝑢))〉 ↔ ((1st
‘𝑣) = (𝐹‘(1st
‘𝑢)) ∧
(2nd ‘𝑣) =
(𝐺‘(2nd
‘𝑢))))) |
79 | 78 | ad2antll 488 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ (𝑣 = 〈(𝐹‘(1st
‘𝑢)), (𝐺‘(2nd
‘𝑢))〉 ↔
((1st ‘𝑣)
= (𝐹‘(1st
‘𝑢)) ∧
(2nd ‘𝑣) =
(𝐺‘(2nd
‘𝑢))))) |
80 | | eqop 6154 |
. . . . . . . 8
⊢ (𝑢 ∈ (𝑋 × 𝑌) → (𝑢 = 〈(◡𝐹‘(1st ‘𝑣)), (◡𝐺‘(2nd ‘𝑣))〉 ↔ ((1st
‘𝑢) = (◡𝐹‘(1st ‘𝑣)) ∧ (2nd
‘𝑢) = (◡𝐺‘(2nd ‘𝑣))))) |
81 | 80 | ad2antrl 487 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ (𝑢 = 〈(◡𝐹‘(1st ‘𝑣)), (◡𝐺‘(2nd ‘𝑣))〉 ↔ ((1st
‘𝑢) = (◡𝐹‘(1st ‘𝑣)) ∧ (2nd
‘𝑢) = (◡𝐺‘(2nd ‘𝑣))))) |
82 | 77, 79, 81 | 3bitr4rd 220 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ (𝑢 = 〈(◡𝐹‘(1st ‘𝑣)), (◡𝐺‘(2nd ‘𝑣))〉 ↔ 𝑣 = 〈(𝐹‘(1st ‘𝑢)), (𝐺‘(2nd ‘𝑢))〉)) |
83 | 30, 43, 60, 82 | f1ocnv2d 6051 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉):(𝑋 × 𝑌)–1-1-onto→(∪ 𝐿 × ∪ 𝑀)
∧ ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) = (𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)
↦ 〈(◡𝐹‘(1st ‘𝑣)), (◡𝐺‘(2nd ‘𝑣))〉))) |
84 | 83 | simprd 113 |
. . . 4
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) = (𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)
↦ 〈(◡𝐹‘(1st ‘𝑣)), (◡𝐺‘(2nd ‘𝑣))〉)) |
85 | | vex 2733 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
86 | | vex 2733 |
. . . . . . . 8
⊢ 𝑤 ∈ V |
87 | 85, 86 | op1std 6125 |
. . . . . . 7
⊢ (𝑣 = 〈𝑧, 𝑤〉 → (1st ‘𝑣) = 𝑧) |
88 | 87 | fveq2d 5498 |
. . . . . 6
⊢ (𝑣 = 〈𝑧, 𝑤〉 → (◡𝐹‘(1st ‘𝑣)) = (◡𝐹‘𝑧)) |
89 | 85, 86 | op2ndd 6126 |
. . . . . . 7
⊢ (𝑣 = 〈𝑧, 𝑤〉 → (2nd ‘𝑣) = 𝑤) |
90 | 89 | fveq2d 5498 |
. . . . . 6
⊢ (𝑣 = 〈𝑧, 𝑤〉 → (◡𝐺‘(2nd ‘𝑣)) = (◡𝐺‘𝑤)) |
91 | 88, 90 | opeq12d 3771 |
. . . . 5
⊢ (𝑣 = 〈𝑧, 𝑤〉 → 〈(◡𝐹‘(1st ‘𝑣)), (◡𝐺‘(2nd ‘𝑣))〉 = 〈(◡𝐹‘𝑧), (◡𝐺‘𝑤)〉) |
92 | 91 | mpompt 5943 |
. . . 4
⊢ (𝑣 ∈ (∪ 𝐿
× ∪ 𝑀) ↦ 〈(◡𝐹‘(1st ‘𝑣)), (◡𝐺‘(2nd ‘𝑣))〉) = (𝑧 ∈ ∪ 𝐿, 𝑤 ∈ ∪ 𝑀 ↦ 〈(◡𝐹‘𝑧), (◡𝐺‘𝑤)〉) |
93 | 84, 92 | eqtrdi 2219 |
. . 3
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) = (𝑧 ∈ ∪ 𝐿, 𝑤 ∈ ∪ 𝑀 ↦ 〈(◡𝐹‘𝑧), (◡𝐺‘𝑤)〉)) |
94 | | cntop2 12961 |
. . . . . 6
⊢ (𝐹 ∈ (𝐽 Cn 𝐿) → 𝐿 ∈ Top) |
95 | 3, 94 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝐿 ∈ Top) |
96 | 31 | toptopon 12775 |
. . . . 5
⊢ (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘∪ 𝐿)) |
97 | 95, 96 | sylib 121 |
. . . 4
⊢ (𝜑 → 𝐿 ∈ (TopOn‘∪ 𝐿)) |
98 | | cntop2 12961 |
. . . . . 6
⊢ (𝐺 ∈ (𝐾 Cn 𝑀) → 𝑀 ∈ Top) |
99 | 11, 98 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ Top) |
100 | 37 | toptopon 12775 |
. . . . 5
⊢ (𝑀 ∈ Top ↔ 𝑀 ∈ (TopOn‘∪ 𝑀)) |
101 | 99, 100 | sylib 121 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ (TopOn‘∪ 𝑀)) |
102 | 97, 101 | cnmpt1st 13047 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ ∪ 𝐿, 𝑤 ∈ ∪ 𝑀 ↦ 𝑧) ∈ ((𝐿 ×t 𝑀) Cn 𝐿)) |
103 | | hmeocnvcn 13065 |
. . . . . 6
⊢ (𝐹 ∈ (𝐽Homeo𝐿) → ◡𝐹 ∈ (𝐿 Cn 𝐽)) |
104 | 1, 103 | syl 14 |
. . . . 5
⊢ (𝜑 → ◡𝐹 ∈ (𝐿 Cn 𝐽)) |
105 | 97, 101, 102, 104 | cnmpt21f 13051 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ ∪ 𝐿, 𝑤 ∈ ∪ 𝑀 ↦ (◡𝐹‘𝑧)) ∈ ((𝐿 ×t 𝑀) Cn 𝐽)) |
106 | 97, 101 | cnmpt2nd 13048 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ ∪ 𝐿, 𝑤 ∈ ∪ 𝑀 ↦ 𝑤) ∈ ((𝐿 ×t 𝑀) Cn 𝑀)) |
107 | | hmeocnvcn 13065 |
. . . . . 6
⊢ (𝐺 ∈ (𝐾Homeo𝑀) → ◡𝐺 ∈ (𝑀 Cn 𝐾)) |
108 | 9, 107 | syl 14 |
. . . . 5
⊢ (𝜑 → ◡𝐺 ∈ (𝑀 Cn 𝐾)) |
109 | 97, 101, 106, 108 | cnmpt21f 13051 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ ∪ 𝐿, 𝑤 ∈ ∪ 𝑀 ↦ (◡𝐺‘𝑤)) ∈ ((𝐿 ×t 𝑀) Cn 𝐾)) |
110 | 97, 101, 105, 109 | cnmpt2t 13052 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ∪ 𝐿, 𝑤 ∈ ∪ 𝑀 ↦ 〈(◡𝐹‘𝑧), (◡𝐺‘𝑤)〉) ∈ ((𝐿 ×t 𝑀) Cn (𝐽 ×t 𝐾))) |
111 | 93, 110 | eqeltrd 2247 |
. 2
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) ∈ ((𝐿 ×t 𝑀) Cn (𝐽 ×t 𝐾))) |
112 | | ishmeo 13063 |
. 2
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) ∈ ((𝐽 ×t 𝐾)Homeo(𝐿 ×t 𝑀)) ↔ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) ∈ ((𝐽 ×t 𝐾) Cn (𝐿 ×t 𝑀)) ∧ ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) ∈ ((𝐿 ×t 𝑀) Cn (𝐽 ×t 𝐾)))) |
113 | 21, 111, 112 | sylanbrc 415 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) ∈ ((𝐽 ×t 𝐾)Homeo(𝐿 ×t 𝑀))) |