Step | Hyp | Ref
| Expression |
1 | | txhmeo.3 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝐽Homeo𝐿)) |
2 | | hmeocn 21563 |
. . . . . 6
⊢ (𝐹 ∈ (𝐽Homeo𝐿) → 𝐹 ∈ (𝐽 Cn 𝐿)) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐿)) |
4 | | cntop1 21044 |
. . . . 5
⊢ (𝐹 ∈ (𝐽 Cn 𝐿) → 𝐽 ∈ Top) |
5 | 3, 4 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐽 ∈ Top) |
6 | | txhmeo.1 |
. . . . 5
⊢ 𝑋 = ∪
𝐽 |
7 | 6 | toptopon 20722 |
. . . 4
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
8 | 5, 7 | sylib 208 |
. . 3
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
9 | | txhmeo.4 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ (𝐾Homeo𝑀)) |
10 | | hmeocn 21563 |
. . . . . 6
⊢ (𝐺 ∈ (𝐾Homeo𝑀) → 𝐺 ∈ (𝐾 Cn 𝑀)) |
11 | 9, 10 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝑀)) |
12 | | cntop1 21044 |
. . . . 5
⊢ (𝐺 ∈ (𝐾 Cn 𝑀) → 𝐾 ∈ Top) |
13 | 11, 12 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ Top) |
14 | | txhmeo.2 |
. . . . 5
⊢ 𝑌 = ∪
𝐾 |
15 | 14 | toptopon 20722 |
. . . 4
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌)) |
16 | 13, 15 | sylib 208 |
. . 3
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
17 | 8, 16 | cnmpt1st 21471 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑥) ∈ ((𝐽 ×t 𝐾) Cn 𝐽)) |
18 | 8, 16, 17, 3 | cnmpt21f 21475 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐹‘𝑥)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) |
19 | 8, 16 | cnmpt2nd 21472 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑦) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) |
20 | 8, 16, 19, 11 | cnmpt21f 21475 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐺‘𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝑀)) |
21 | 8, 16, 18, 20 | cnmpt2t 21476 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) ∈ ((𝐽 ×t 𝐾) Cn (𝐿 ×t 𝑀))) |
22 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
23 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
24 | 22, 23 | op1std 7178 |
. . . . . . . . . 10
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (1st ‘𝑢) = 𝑥) |
25 | 24 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (𝐹‘(1st ‘𝑢)) = (𝐹‘𝑥)) |
26 | 22, 23 | op2ndd 7179 |
. . . . . . . . . 10
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (2nd ‘𝑢) = 𝑦) |
27 | 26 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑢 = 〈𝑥, 𝑦〉 → (𝐺‘(2nd ‘𝑢)) = (𝐺‘𝑦)) |
28 | 25, 27 | opeq12d 4410 |
. . . . . . . 8
⊢ (𝑢 = 〈𝑥, 𝑦〉 → 〈(𝐹‘(1st ‘𝑢)), (𝐺‘(2nd ‘𝑢))〉 = 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) |
29 | 28 | mpt2mpt 6752 |
. . . . . . 7
⊢ (𝑢 ∈ (𝑋 × 𝑌) ↦ 〈(𝐹‘(1st ‘𝑢)), (𝐺‘(2nd ‘𝑢))〉) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) |
30 | 29 | eqcomi 2631 |
. . . . . 6
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) = (𝑢 ∈ (𝑋 × 𝑌) ↦ 〈(𝐹‘(1st ‘𝑢)), (𝐺‘(2nd ‘𝑢))〉) |
31 | | eqid 2622 |
. . . . . . . . . 10
⊢ ∪ 𝐿 =
∪ 𝐿 |
32 | 6, 31 | cnf 21050 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝐽 Cn 𝐿) → 𝐹:𝑋⟶∪ 𝐿) |
33 | 3, 32 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝑋⟶∪ 𝐿) |
34 | | xp1st 7198 |
. . . . . . . 8
⊢ (𝑢 ∈ (𝑋 × 𝑌) → (1st ‘𝑢) ∈ 𝑋) |
35 | | ffvelrn 6357 |
. . . . . . . 8
⊢ ((𝐹:𝑋⟶∪ 𝐿 ∧ (1st
‘𝑢) ∈ 𝑋) → (𝐹‘(1st ‘𝑢)) ∈ ∪ 𝐿) |
36 | 33, 34, 35 | syl2an 494 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑋 × 𝑌)) → (𝐹‘(1st ‘𝑢)) ∈ ∪ 𝐿) |
37 | | eqid 2622 |
. . . . . . . . . 10
⊢ ∪ 𝑀 =
∪ 𝑀 |
38 | 14, 37 | cnf 21050 |
. . . . . . . . 9
⊢ (𝐺 ∈ (𝐾 Cn 𝑀) → 𝐺:𝑌⟶∪ 𝑀) |
39 | 11, 38 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:𝑌⟶∪ 𝑀) |
40 | | xp2nd 7199 |
. . . . . . . 8
⊢ (𝑢 ∈ (𝑋 × 𝑌) → (2nd ‘𝑢) ∈ 𝑌) |
41 | | ffvelrn 6357 |
. . . . . . . 8
⊢ ((𝐺:𝑌⟶∪ 𝑀 ∧ (2nd
‘𝑢) ∈ 𝑌) → (𝐺‘(2nd ‘𝑢)) ∈ ∪ 𝑀) |
42 | 39, 40, 41 | syl2an 494 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑋 × 𝑌)) → (𝐺‘(2nd ‘𝑢)) ∈ ∪ 𝑀) |
43 | | opelxpi 5148 |
. . . . . . 7
⊢ (((𝐹‘(1st
‘𝑢)) ∈ ∪ 𝐿
∧ (𝐺‘(2nd ‘𝑢)) ∈ ∪ 𝑀)
→ 〈(𝐹‘(1st ‘𝑢)), (𝐺‘(2nd ‘𝑢))〉 ∈ (∪ 𝐿
× ∪ 𝑀)) |
44 | 36, 42, 43 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑋 × 𝑌)) → 〈(𝐹‘(1st ‘𝑢)), (𝐺‘(2nd ‘𝑢))〉 ∈ (∪ 𝐿
× ∪ 𝑀)) |
45 | 6, 31 | hmeof1o 21567 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝐽Homeo𝐿) → 𝐹:𝑋–1-1-onto→∪ 𝐿) |
46 | 1, 45 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑋–1-1-onto→∪ 𝐿) |
47 | | f1ocnv 6149 |
. . . . . . . . 9
⊢ (𝐹:𝑋–1-1-onto→∪ 𝐿
→ ◡𝐹:∪ 𝐿–1-1-onto→𝑋) |
48 | | f1of 6137 |
. . . . . . . . 9
⊢ (◡𝐹:∪ 𝐿–1-1-onto→𝑋 → ◡𝐹:∪ 𝐿⟶𝑋) |
49 | 46, 47, 48 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → ◡𝐹:∪ 𝐿⟶𝑋) |
50 | | xp1st 7198 |
. . . . . . . 8
⊢ (𝑣 ∈ (∪ 𝐿
× ∪ 𝑀) → (1st ‘𝑣) ∈ ∪ 𝐿) |
51 | | ffvelrn 6357 |
. . . . . . . 8
⊢ ((◡𝐹:∪ 𝐿⟶𝑋 ∧ (1st ‘𝑣) ∈ ∪ 𝐿)
→ (◡𝐹‘(1st ‘𝑣)) ∈ 𝑋) |
52 | 49, 50, 51 | syl2an 494 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀))
→ (◡𝐹‘(1st ‘𝑣)) ∈ 𝑋) |
53 | 14, 37 | hmeof1o 21567 |
. . . . . . . . . 10
⊢ (𝐺 ∈ (𝐾Homeo𝑀) → 𝐺:𝑌–1-1-onto→∪ 𝑀) |
54 | 9, 53 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:𝑌–1-1-onto→∪ 𝑀) |
55 | | f1ocnv 6149 |
. . . . . . . . 9
⊢ (𝐺:𝑌–1-1-onto→∪ 𝑀
→ ◡𝐺:∪ 𝑀–1-1-onto→𝑌) |
56 | | f1of 6137 |
. . . . . . . . 9
⊢ (◡𝐺:∪ 𝑀–1-1-onto→𝑌 → ◡𝐺:∪ 𝑀⟶𝑌) |
57 | 54, 55, 56 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → ◡𝐺:∪ 𝑀⟶𝑌) |
58 | | xp2nd 7199 |
. . . . . . . 8
⊢ (𝑣 ∈ (∪ 𝐿
× ∪ 𝑀) → (2nd ‘𝑣) ∈ ∪ 𝑀) |
59 | | ffvelrn 6357 |
. . . . . . . 8
⊢ ((◡𝐺:∪ 𝑀⟶𝑌 ∧ (2nd ‘𝑣) ∈ ∪ 𝑀)
→ (◡𝐺‘(2nd ‘𝑣)) ∈ 𝑌) |
60 | 57, 58, 59 | syl2an 494 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀))
→ (◡𝐺‘(2nd ‘𝑣)) ∈ 𝑌) |
61 | | opelxpi 5148 |
. . . . . . 7
⊢ (((◡𝐹‘(1st ‘𝑣)) ∈ 𝑋 ∧ (◡𝐺‘(2nd ‘𝑣)) ∈ 𝑌) → 〈(◡𝐹‘(1st ‘𝑣)), (◡𝐺‘(2nd ‘𝑣))〉 ∈ (𝑋 × 𝑌)) |
62 | 52, 60, 61 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀))
→ 〈(◡𝐹‘(1st ‘𝑣)), (◡𝐺‘(2nd ‘𝑣))〉 ∈ (𝑋 × 𝑌)) |
63 | 46 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ 𝐹:𝑋–1-1-onto→∪ 𝐿) |
64 | 34 | ad2antrl 764 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ (1st ‘𝑢) ∈ 𝑋) |
65 | 50 | ad2antll 765 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ (1st ‘𝑣) ∈ ∪ 𝐿) |
66 | | f1ocnvfvb 6535 |
. . . . . . . . . 10
⊢ ((𝐹:𝑋–1-1-onto→∪ 𝐿
∧ (1st ‘𝑢) ∈ 𝑋 ∧ (1st ‘𝑣) ∈ ∪ 𝐿)
→ ((𝐹‘(1st ‘𝑢)) = (1st
‘𝑣) ↔ (◡𝐹‘(1st ‘𝑣)) = (1st
‘𝑢))) |
67 | 63, 64, 65, 66 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ ((𝐹‘(1st ‘𝑢)) = (1st
‘𝑣) ↔ (◡𝐹‘(1st ‘𝑣)) = (1st
‘𝑢))) |
68 | | eqcom 2629 |
. . . . . . . . 9
⊢
((1st ‘𝑣) = (𝐹‘(1st ‘𝑢)) ↔ (𝐹‘(1st ‘𝑢)) = (1st
‘𝑣)) |
69 | | eqcom 2629 |
. . . . . . . . 9
⊢
((1st ‘𝑢) = (◡𝐹‘(1st ‘𝑣)) ↔ (◡𝐹‘(1st ‘𝑣)) = (1st
‘𝑢)) |
70 | 67, 68, 69 | 3bitr4g 303 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ ((1st ‘𝑣) = (𝐹‘(1st ‘𝑢)) ↔ (1st
‘𝑢) = (◡𝐹‘(1st ‘𝑣)))) |
71 | 54 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ 𝐺:𝑌–1-1-onto→∪ 𝑀) |
72 | 40 | ad2antrl 764 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ (2nd ‘𝑢) ∈ 𝑌) |
73 | 58 | ad2antll 765 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ (2nd ‘𝑣) ∈ ∪ 𝑀) |
74 | | f1ocnvfvb 6535 |
. . . . . . . . . 10
⊢ ((𝐺:𝑌–1-1-onto→∪ 𝑀
∧ (2nd ‘𝑢) ∈ 𝑌 ∧ (2nd ‘𝑣) ∈ ∪ 𝑀)
→ ((𝐺‘(2nd ‘𝑢)) = (2nd
‘𝑣) ↔ (◡𝐺‘(2nd ‘𝑣)) = (2nd
‘𝑢))) |
75 | 71, 72, 73, 74 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ ((𝐺‘(2nd ‘𝑢)) = (2nd
‘𝑣) ↔ (◡𝐺‘(2nd ‘𝑣)) = (2nd
‘𝑢))) |
76 | | eqcom 2629 |
. . . . . . . . 9
⊢
((2nd ‘𝑣) = (𝐺‘(2nd ‘𝑢)) ↔ (𝐺‘(2nd ‘𝑢)) = (2nd
‘𝑣)) |
77 | | eqcom 2629 |
. . . . . . . . 9
⊢
((2nd ‘𝑢) = (◡𝐺‘(2nd ‘𝑣)) ↔ (◡𝐺‘(2nd ‘𝑣)) = (2nd
‘𝑢)) |
78 | 75, 76, 77 | 3bitr4g 303 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ ((2nd ‘𝑣) = (𝐺‘(2nd ‘𝑢)) ↔ (2nd
‘𝑢) = (◡𝐺‘(2nd ‘𝑣)))) |
79 | 70, 78 | anbi12d 747 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ (((1st ‘𝑣) = (𝐹‘(1st ‘𝑢)) ∧ (2nd
‘𝑣) = (𝐺‘(2nd
‘𝑢))) ↔
((1st ‘𝑢)
= (◡𝐹‘(1st ‘𝑣)) ∧ (2nd
‘𝑢) = (◡𝐺‘(2nd ‘𝑣))))) |
80 | | eqop 7208 |
. . . . . . . 8
⊢ (𝑣 ∈ (∪ 𝐿
× ∪ 𝑀) → (𝑣 = 〈(𝐹‘(1st ‘𝑢)), (𝐺‘(2nd ‘𝑢))〉 ↔ ((1st
‘𝑣) = (𝐹‘(1st
‘𝑢)) ∧
(2nd ‘𝑣) =
(𝐺‘(2nd
‘𝑢))))) |
81 | 80 | ad2antll 765 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ (𝑣 = 〈(𝐹‘(1st
‘𝑢)), (𝐺‘(2nd
‘𝑢))〉 ↔
((1st ‘𝑣)
= (𝐹‘(1st
‘𝑢)) ∧
(2nd ‘𝑣) =
(𝐺‘(2nd
‘𝑢))))) |
82 | | eqop 7208 |
. . . . . . . 8
⊢ (𝑢 ∈ (𝑋 × 𝑌) → (𝑢 = 〈(◡𝐹‘(1st ‘𝑣)), (◡𝐺‘(2nd ‘𝑣))〉 ↔ ((1st
‘𝑢) = (◡𝐹‘(1st ‘𝑣)) ∧ (2nd
‘𝑢) = (◡𝐺‘(2nd ‘𝑣))))) |
83 | 82 | ad2antrl 764 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ (𝑢 = 〈(◡𝐹‘(1st ‘𝑣)), (◡𝐺‘(2nd ‘𝑣))〉 ↔ ((1st
‘𝑢) = (◡𝐹‘(1st ‘𝑣)) ∧ (2nd
‘𝑢) = (◡𝐺‘(2nd ‘𝑣))))) |
84 | 79, 81, 83 | 3bitr4rd 301 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)))
→ (𝑢 = 〈(◡𝐹‘(1st ‘𝑣)), (◡𝐺‘(2nd ‘𝑣))〉 ↔ 𝑣 = 〈(𝐹‘(1st ‘𝑢)), (𝐺‘(2nd ‘𝑢))〉)) |
85 | 30, 44, 62, 84 | f1ocnv2d 6886 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉):(𝑋 × 𝑌)–1-1-onto→(∪ 𝐿 × ∪ 𝑀)
∧ ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) = (𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)
↦ 〈(◡𝐹‘(1st ‘𝑣)), (◡𝐺‘(2nd ‘𝑣))〉))) |
86 | 85 | simprd 479 |
. . . 4
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) = (𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)
↦ 〈(◡𝐹‘(1st ‘𝑣)), (◡𝐺‘(2nd ‘𝑣))〉)) |
87 | | vex 3203 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
88 | | vex 3203 |
. . . . . . . 8
⊢ 𝑤 ∈ V |
89 | 87, 88 | op1std 7178 |
. . . . . . 7
⊢ (𝑣 = 〈𝑧, 𝑤〉 → (1st ‘𝑣) = 𝑧) |
90 | 89 | fveq2d 6195 |
. . . . . 6
⊢ (𝑣 = 〈𝑧, 𝑤〉 → (◡𝐹‘(1st ‘𝑣)) = (◡𝐹‘𝑧)) |
91 | 87, 88 | op2ndd 7179 |
. . . . . . 7
⊢ (𝑣 = 〈𝑧, 𝑤〉 → (2nd ‘𝑣) = 𝑤) |
92 | 91 | fveq2d 6195 |
. . . . . 6
⊢ (𝑣 = 〈𝑧, 𝑤〉 → (◡𝐺‘(2nd ‘𝑣)) = (◡𝐺‘𝑤)) |
93 | 90, 92 | opeq12d 4410 |
. . . . 5
⊢ (𝑣 = 〈𝑧, 𝑤〉 → 〈(◡𝐹‘(1st ‘𝑣)), (◡𝐺‘(2nd ‘𝑣))〉 = 〈(◡𝐹‘𝑧), (◡𝐺‘𝑤)〉) |
94 | 93 | mpt2mpt 6752 |
. . . 4
⊢ (𝑣 ∈ (∪ 𝐿
× ∪ 𝑀) ↦ 〈(◡𝐹‘(1st ‘𝑣)), (◡𝐺‘(2nd ‘𝑣))〉) = (𝑧 ∈ ∪ 𝐿, 𝑤 ∈ ∪ 𝑀 ↦ 〈(◡𝐹‘𝑧), (◡𝐺‘𝑤)〉) |
95 | 86, 94 | syl6eq 2672 |
. . 3
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) = (𝑧 ∈ ∪ 𝐿, 𝑤 ∈ ∪ 𝑀 ↦ 〈(◡𝐹‘𝑧), (◡𝐺‘𝑤)〉)) |
96 | | cntop2 21045 |
. . . . . 6
⊢ (𝐹 ∈ (𝐽 Cn 𝐿) → 𝐿 ∈ Top) |
97 | 3, 96 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐿 ∈ Top) |
98 | 31 | toptopon 20722 |
. . . . 5
⊢ (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘∪ 𝐿)) |
99 | 97, 98 | sylib 208 |
. . . 4
⊢ (𝜑 → 𝐿 ∈ (TopOn‘∪ 𝐿)) |
100 | | cntop2 21045 |
. . . . . 6
⊢ (𝐺 ∈ (𝐾 Cn 𝑀) → 𝑀 ∈ Top) |
101 | 11, 100 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ Top) |
102 | 37 | toptopon 20722 |
. . . . 5
⊢ (𝑀 ∈ Top ↔ 𝑀 ∈ (TopOn‘∪ 𝑀)) |
103 | 101, 102 | sylib 208 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ (TopOn‘∪ 𝑀)) |
104 | 99, 103 | cnmpt1st 21471 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ ∪ 𝐿, 𝑤 ∈ ∪ 𝑀 ↦ 𝑧) ∈ ((𝐿 ×t 𝑀) Cn 𝐿)) |
105 | | hmeocnvcn 21564 |
. . . . . 6
⊢ (𝐹 ∈ (𝐽Homeo𝐿) → ◡𝐹 ∈ (𝐿 Cn 𝐽)) |
106 | 1, 105 | syl 17 |
. . . . 5
⊢ (𝜑 → ◡𝐹 ∈ (𝐿 Cn 𝐽)) |
107 | 99, 103, 104, 106 | cnmpt21f 21475 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ ∪ 𝐿, 𝑤 ∈ ∪ 𝑀 ↦ (◡𝐹‘𝑧)) ∈ ((𝐿 ×t 𝑀) Cn 𝐽)) |
108 | 99, 103 | cnmpt2nd 21472 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ ∪ 𝐿, 𝑤 ∈ ∪ 𝑀 ↦ 𝑤) ∈ ((𝐿 ×t 𝑀) Cn 𝑀)) |
109 | | hmeocnvcn 21564 |
. . . . . 6
⊢ (𝐺 ∈ (𝐾Homeo𝑀) → ◡𝐺 ∈ (𝑀 Cn 𝐾)) |
110 | 9, 109 | syl 17 |
. . . . 5
⊢ (𝜑 → ◡𝐺 ∈ (𝑀 Cn 𝐾)) |
111 | 99, 103, 108, 110 | cnmpt21f 21475 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ ∪ 𝐿, 𝑤 ∈ ∪ 𝑀 ↦ (◡𝐺‘𝑤)) ∈ ((𝐿 ×t 𝑀) Cn 𝐾)) |
112 | 99, 103, 107, 111 | cnmpt2t 21476 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ∪ 𝐿, 𝑤 ∈ ∪ 𝑀 ↦ 〈(◡𝐹‘𝑧), (◡𝐺‘𝑤)〉) ∈ ((𝐿 ×t 𝑀) Cn (𝐽 ×t 𝐾))) |
113 | 95, 112 | eqeltrd 2701 |
. 2
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) ∈ ((𝐿 ×t 𝑀) Cn (𝐽 ×t 𝐾))) |
114 | | ishmeo 21562 |
. 2
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) ∈ ((𝐽 ×t 𝐾)Homeo(𝐿 ×t 𝑀)) ↔ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) ∈ ((𝐽 ×t 𝐾) Cn (𝐿 ×t 𝑀)) ∧ ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) ∈ ((𝐿 ×t 𝑀) Cn (𝐽 ×t 𝐾)))) |
115 | 21, 113, 114 | sylanbrc 698 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) ∈ ((𝐽 ×t 𝐾)Homeo(𝐿 ×t 𝑀))) |