Step | Hyp | Ref
| Expression |
1 | | txhmeo.3 |
. . . . . 6
β’ (π β πΉ β (π½HomeoπΏ)) |
2 | | hmeocn 22952 |
. . . . . 6
β’ (πΉ β (π½HomeoπΏ) β πΉ β (π½ Cn πΏ)) |
3 | 1, 2 | syl 17 |
. . . . 5
β’ (π β πΉ β (π½ Cn πΏ)) |
4 | | cntop1 22432 |
. . . . 5
β’ (πΉ β (π½ Cn πΏ) β π½ β Top) |
5 | 3, 4 | syl 17 |
. . . 4
β’ (π β π½ β Top) |
6 | | txhmeo.1 |
. . . . 5
β’ π = βͺ
π½ |
7 | 6 | toptopon 22107 |
. . . 4
β’ (π½ β Top β π½ β (TopOnβπ)) |
8 | 5, 7 | sylib 217 |
. . 3
β’ (π β π½ β (TopOnβπ)) |
9 | | txhmeo.4 |
. . . . . 6
β’ (π β πΊ β (πΎHomeoπ)) |
10 | | hmeocn 22952 |
. . . . . 6
β’ (πΊ β (πΎHomeoπ) β πΊ β (πΎ Cn π)) |
11 | 9, 10 | syl 17 |
. . . . 5
β’ (π β πΊ β (πΎ Cn π)) |
12 | | cntop1 22432 |
. . . . 5
β’ (πΊ β (πΎ Cn π) β πΎ β Top) |
13 | 11, 12 | syl 17 |
. . . 4
β’ (π β πΎ β Top) |
14 | | txhmeo.2 |
. . . . 5
β’ π = βͺ
πΎ |
15 | 14 | toptopon 22107 |
. . . 4
β’ (πΎ β Top β πΎ β (TopOnβπ)) |
16 | 13, 15 | sylib 217 |
. . 3
β’ (π β πΎ β (TopOnβπ)) |
17 | 8, 16 | cnmpt1st 22860 |
. . . 4
β’ (π β (π₯ β π, π¦ β π β¦ π₯) β ((π½ Γt πΎ) Cn π½)) |
18 | 8, 16, 17, 3 | cnmpt21f 22864 |
. . 3
β’ (π β (π₯ β π, π¦ β π β¦ (πΉβπ₯)) β ((π½ Γt πΎ) Cn πΏ)) |
19 | 8, 16 | cnmpt2nd 22861 |
. . . 4
β’ (π β (π₯ β π, π¦ β π β¦ π¦) β ((π½ Γt πΎ) Cn πΎ)) |
20 | 8, 16, 19, 11 | cnmpt21f 22864 |
. . 3
β’ (π β (π₯ β π, π¦ β π β¦ (πΊβπ¦)) β ((π½ Γt πΎ) Cn π)) |
21 | 8, 16, 18, 20 | cnmpt2t 22865 |
. 2
β’ (π β (π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΊβπ¦)β©) β ((π½ Γt πΎ) Cn (πΏ Γt π))) |
22 | | vex 3441 |
. . . . . . . . . . 11
β’ π₯ β V |
23 | | vex 3441 |
. . . . . . . . . . 11
β’ π¦ β V |
24 | 22, 23 | op1std 7869 |
. . . . . . . . . 10
β’ (π’ = β¨π₯, π¦β© β (1st βπ’) = π₯) |
25 | 24 | fveq2d 6804 |
. . . . . . . . 9
β’ (π’ = β¨π₯, π¦β© β (πΉβ(1st βπ’)) = (πΉβπ₯)) |
26 | 22, 23 | op2ndd 7870 |
. . . . . . . . . 10
β’ (π’ = β¨π₯, π¦β© β (2nd βπ’) = π¦) |
27 | 26 | fveq2d 6804 |
. . . . . . . . 9
β’ (π’ = β¨π₯, π¦β© β (πΊβ(2nd βπ’)) = (πΊβπ¦)) |
28 | 25, 27 | opeq12d 4817 |
. . . . . . . 8
β’ (π’ = β¨π₯, π¦β© β β¨(πΉβ(1st βπ’)), (πΊβ(2nd βπ’))β© = β¨(πΉβπ₯), (πΊβπ¦)β©) |
29 | 28 | mpompt 7416 |
. . . . . . 7
β’ (π’ β (π Γ π) β¦ β¨(πΉβ(1st βπ’)), (πΊβ(2nd βπ’))β©) = (π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΊβπ¦)β©) |
30 | 29 | eqcomi 2745 |
. . . . . 6
β’ (π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΊβπ¦)β©) = (π’ β (π Γ π) β¦ β¨(πΉβ(1st βπ’)), (πΊβ(2nd βπ’))β©) |
31 | | eqid 2736 |
. . . . . . . . . 10
β’ βͺ πΏ =
βͺ πΏ |
32 | 6, 31 | cnf 22438 |
. . . . . . . . 9
β’ (πΉ β (π½ Cn πΏ) β πΉ:πβΆβͺ πΏ) |
33 | 3, 32 | syl 17 |
. . . . . . . 8
β’ (π β πΉ:πβΆβͺ πΏ) |
34 | | xp1st 7891 |
. . . . . . . 8
β’ (π’ β (π Γ π) β (1st βπ’) β π) |
35 | | ffvelcdm 6987 |
. . . . . . . 8
β’ ((πΉ:πβΆβͺ πΏ β§ (1st
βπ’) β π) β (πΉβ(1st βπ’)) β βͺ πΏ) |
36 | 33, 34, 35 | syl2an 597 |
. . . . . . 7
β’ ((π β§ π’ β (π Γ π)) β (πΉβ(1st βπ’)) β βͺ πΏ) |
37 | | eqid 2736 |
. . . . . . . . . 10
β’ βͺ π =
βͺ π |
38 | 14, 37 | cnf 22438 |
. . . . . . . . 9
β’ (πΊ β (πΎ Cn π) β πΊ:πβΆβͺ π) |
39 | 11, 38 | syl 17 |
. . . . . . . 8
β’ (π β πΊ:πβΆβͺ π) |
40 | | xp2nd 7892 |
. . . . . . . 8
β’ (π’ β (π Γ π) β (2nd βπ’) β π) |
41 | | ffvelcdm 6987 |
. . . . . . . 8
β’ ((πΊ:πβΆβͺ π β§ (2nd
βπ’) β π) β (πΊβ(2nd βπ’)) β βͺ π) |
42 | 39, 40, 41 | syl2an 597 |
. . . . . . 7
β’ ((π β§ π’ β (π Γ π)) β (πΊβ(2nd βπ’)) β βͺ π) |
43 | 36, 42 | opelxpd 5634 |
. . . . . 6
β’ ((π β§ π’ β (π Γ π)) β β¨(πΉβ(1st βπ’)), (πΊβ(2nd βπ’))β© β (βͺ πΏ
Γ βͺ π)) |
44 | 6, 31 | hmeof1o 22956 |
. . . . . . . . . 10
β’ (πΉ β (π½HomeoπΏ) β πΉ:πβ1-1-ontoββͺ πΏ) |
45 | 1, 44 | syl 17 |
. . . . . . . . 9
β’ (π β πΉ:πβ1-1-ontoββͺ πΏ) |
46 | | f1ocnv 6754 |
. . . . . . . . 9
β’ (πΉ:πβ1-1-ontoββͺ πΏ
β β‘πΉ:βͺ πΏβ1-1-ontoβπ) |
47 | | f1of 6742 |
. . . . . . . . 9
β’ (β‘πΉ:βͺ πΏβ1-1-ontoβπ β β‘πΉ:βͺ πΏβΆπ) |
48 | 45, 46, 47 | 3syl 18 |
. . . . . . . 8
β’ (π β β‘πΉ:βͺ πΏβΆπ) |
49 | | xp1st 7891 |
. . . . . . . 8
β’ (π£ β (βͺ πΏ
Γ βͺ π) β (1st βπ£) β βͺ πΏ) |
50 | | ffvelcdm 6987 |
. . . . . . . 8
β’ ((β‘πΉ:βͺ πΏβΆπ β§ (1st βπ£) β βͺ πΏ)
β (β‘πΉβ(1st βπ£)) β π) |
51 | 48, 49, 50 | syl2an 597 |
. . . . . . 7
β’ ((π β§ π£ β (βͺ πΏ Γ βͺ π))
β (β‘πΉβ(1st βπ£)) β π) |
52 | 14, 37 | hmeof1o 22956 |
. . . . . . . . . 10
β’ (πΊ β (πΎHomeoπ) β πΊ:πβ1-1-ontoββͺ π) |
53 | 9, 52 | syl 17 |
. . . . . . . . 9
β’ (π β πΊ:πβ1-1-ontoββͺ π) |
54 | | f1ocnv 6754 |
. . . . . . . . 9
β’ (πΊ:πβ1-1-ontoββͺ π
β β‘πΊ:βͺ πβ1-1-ontoβπ) |
55 | | f1of 6742 |
. . . . . . . . 9
β’ (β‘πΊ:βͺ πβ1-1-ontoβπ β β‘πΊ:βͺ πβΆπ) |
56 | 53, 54, 55 | 3syl 18 |
. . . . . . . 8
β’ (π β β‘πΊ:βͺ πβΆπ) |
57 | | xp2nd 7892 |
. . . . . . . 8
β’ (π£ β (βͺ πΏ
Γ βͺ π) β (2nd βπ£) β βͺ π) |
58 | | ffvelcdm 6987 |
. . . . . . . 8
β’ ((β‘πΊ:βͺ πβΆπ β§ (2nd βπ£) β βͺ π)
β (β‘πΊβ(2nd βπ£)) β π) |
59 | 56, 57, 58 | syl2an 597 |
. . . . . . 7
β’ ((π β§ π£ β (βͺ πΏ Γ βͺ π))
β (β‘πΊβ(2nd βπ£)) β π) |
60 | 51, 59 | opelxpd 5634 |
. . . . . 6
β’ ((π β§ π£ β (βͺ πΏ Γ βͺ π))
β β¨(β‘πΉβ(1st βπ£)), (β‘πΊβ(2nd βπ£))β© β (π Γ π)) |
61 | 45 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π’ β (π Γ π) β§ π£ β (βͺ πΏ Γ βͺ π)))
β πΉ:πβ1-1-ontoββͺ πΏ) |
62 | 34 | ad2antrl 726 |
. . . . . . . . . 10
β’ ((π β§ (π’ β (π Γ π) β§ π£ β (βͺ πΏ Γ βͺ π)))
β (1st βπ’) β π) |
63 | 49 | ad2antll 727 |
. . . . . . . . . 10
β’ ((π β§ (π’ β (π Γ π) β§ π£ β (βͺ πΏ Γ βͺ π)))
β (1st βπ£) β βͺ πΏ) |
64 | | f1ocnvfvb 7179 |
. . . . . . . . . 10
β’ ((πΉ:πβ1-1-ontoββͺ πΏ
β§ (1st βπ’) β π β§ (1st βπ£) β βͺ πΏ)
β ((πΉβ(1st βπ’)) = (1st
βπ£) β (β‘πΉβ(1st βπ£)) = (1st
βπ’))) |
65 | 61, 62, 63, 64 | syl3anc 1371 |
. . . . . . . . 9
β’ ((π β§ (π’ β (π Γ π) β§ π£ β (βͺ πΏ Γ βͺ π)))
β ((πΉβ(1st βπ’)) = (1st
βπ£) β (β‘πΉβ(1st βπ£)) = (1st
βπ’))) |
66 | | eqcom 2743 |
. . . . . . . . 9
β’
((1st βπ£) = (πΉβ(1st βπ’)) β (πΉβ(1st βπ’)) = (1st
βπ£)) |
67 | | eqcom 2743 |
. . . . . . . . 9
β’
((1st βπ’) = (β‘πΉβ(1st βπ£)) β (β‘πΉβ(1st βπ£)) = (1st
βπ’)) |
68 | 65, 66, 67 | 3bitr4g 315 |
. . . . . . . 8
β’ ((π β§ (π’ β (π Γ π) β§ π£ β (βͺ πΏ Γ βͺ π)))
β ((1st βπ£) = (πΉβ(1st βπ’)) β (1st
βπ’) = (β‘πΉβ(1st βπ£)))) |
69 | 53 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π’ β (π Γ π) β§ π£ β (βͺ πΏ Γ βͺ π)))
β πΊ:πβ1-1-ontoββͺ π) |
70 | 40 | ad2antrl 726 |
. . . . . . . . . 10
β’ ((π β§ (π’ β (π Γ π) β§ π£ β (βͺ πΏ Γ βͺ π)))
β (2nd βπ’) β π) |
71 | 57 | ad2antll 727 |
. . . . . . . . . 10
β’ ((π β§ (π’ β (π Γ π) β§ π£ β (βͺ πΏ Γ βͺ π)))
β (2nd βπ£) β βͺ π) |
72 | | f1ocnvfvb 7179 |
. . . . . . . . . 10
β’ ((πΊ:πβ1-1-ontoββͺ π
β§ (2nd βπ’) β π β§ (2nd βπ£) β βͺ π)
β ((πΊβ(2nd βπ’)) = (2nd
βπ£) β (β‘πΊβ(2nd βπ£)) = (2nd
βπ’))) |
73 | 69, 70, 71, 72 | syl3anc 1371 |
. . . . . . . . 9
β’ ((π β§ (π’ β (π Γ π) β§ π£ β (βͺ πΏ Γ βͺ π)))
β ((πΊβ(2nd βπ’)) = (2nd
βπ£) β (β‘πΊβ(2nd βπ£)) = (2nd
βπ’))) |
74 | | eqcom 2743 |
. . . . . . . . 9
β’
((2nd βπ£) = (πΊβ(2nd βπ’)) β (πΊβ(2nd βπ’)) = (2nd
βπ£)) |
75 | | eqcom 2743 |
. . . . . . . . 9
β’
((2nd βπ’) = (β‘πΊβ(2nd βπ£)) β (β‘πΊβ(2nd βπ£)) = (2nd
βπ’)) |
76 | 73, 74, 75 | 3bitr4g 315 |
. . . . . . . 8
β’ ((π β§ (π’ β (π Γ π) β§ π£ β (βͺ πΏ Γ βͺ π)))
β ((2nd βπ£) = (πΊβ(2nd βπ’)) β (2nd
βπ’) = (β‘πΊβ(2nd βπ£)))) |
77 | 68, 76 | anbi12d 632 |
. . . . . . 7
β’ ((π β§ (π’ β (π Γ π) β§ π£ β (βͺ πΏ Γ βͺ π)))
β (((1st βπ£) = (πΉβ(1st βπ’)) β§ (2nd
βπ£) = (πΊβ(2nd
βπ’))) β
((1st βπ’)
= (β‘πΉβ(1st βπ£)) β§ (2nd
βπ’) = (β‘πΊβ(2nd βπ£))))) |
78 | | eqop 7901 |
. . . . . . . 8
β’ (π£ β (βͺ πΏ
Γ βͺ π) β (π£ = β¨(πΉβ(1st βπ’)), (πΊβ(2nd βπ’))β© β ((1st
βπ£) = (πΉβ(1st
βπ’)) β§
(2nd βπ£) =
(πΊβ(2nd
βπ’))))) |
79 | 78 | ad2antll 727 |
. . . . . . 7
β’ ((π β§ (π’ β (π Γ π) β§ π£ β (βͺ πΏ Γ βͺ π)))
β (π£ = β¨(πΉβ(1st
βπ’)), (πΊβ(2nd
βπ’))β© β
((1st βπ£)
= (πΉβ(1st
βπ’)) β§
(2nd βπ£) =
(πΊβ(2nd
βπ’))))) |
80 | | eqop 7901 |
. . . . . . . 8
β’ (π’ β (π Γ π) β (π’ = β¨(β‘πΉβ(1st βπ£)), (β‘πΊβ(2nd βπ£))β© β ((1st
βπ’) = (β‘πΉβ(1st βπ£)) β§ (2nd
βπ’) = (β‘πΊβ(2nd βπ£))))) |
81 | 80 | ad2antrl 726 |
. . . . . . 7
β’ ((π β§ (π’ β (π Γ π) β§ π£ β (βͺ πΏ Γ βͺ π)))
β (π’ = β¨(β‘πΉβ(1st βπ£)), (β‘πΊβ(2nd βπ£))β© β ((1st
βπ’) = (β‘πΉβ(1st βπ£)) β§ (2nd
βπ’) = (β‘πΊβ(2nd βπ£))))) |
82 | 77, 79, 81 | 3bitr4rd 313 |
. . . . . 6
β’ ((π β§ (π’ β (π Γ π) β§ π£ β (βͺ πΏ Γ βͺ π)))
β (π’ = β¨(β‘πΉβ(1st βπ£)), (β‘πΊβ(2nd βπ£))β© β π£ = β¨(πΉβ(1st βπ’)), (πΊβ(2nd βπ’))β©)) |
83 | 30, 43, 60, 82 | f1ocnv2d 7550 |
. . . . 5
β’ (π β ((π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΊβπ¦)β©):(π Γ π)β1-1-ontoβ(βͺ πΏ Γ βͺ π)
β§ β‘(π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΊβπ¦)β©) = (π£ β (βͺ πΏ Γ βͺ π)
β¦ β¨(β‘πΉβ(1st βπ£)), (β‘πΊβ(2nd βπ£))β©))) |
84 | 83 | simprd 497 |
. . . 4
β’ (π β β‘(π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΊβπ¦)β©) = (π£ β (βͺ πΏ Γ βͺ π)
β¦ β¨(β‘πΉβ(1st βπ£)), (β‘πΊβ(2nd βπ£))β©)) |
85 | | vex 3441 |
. . . . . . . 8
β’ π§ β V |
86 | | vex 3441 |
. . . . . . . 8
β’ π€ β V |
87 | 85, 86 | op1std 7869 |
. . . . . . 7
β’ (π£ = β¨π§, π€β© β (1st βπ£) = π§) |
88 | 87 | fveq2d 6804 |
. . . . . 6
β’ (π£ = β¨π§, π€β© β (β‘πΉβ(1st βπ£)) = (β‘πΉβπ§)) |
89 | 85, 86 | op2ndd 7870 |
. . . . . . 7
β’ (π£ = β¨π§, π€β© β (2nd βπ£) = π€) |
90 | 89 | fveq2d 6804 |
. . . . . 6
β’ (π£ = β¨π§, π€β© β (β‘πΊβ(2nd βπ£)) = (β‘πΊβπ€)) |
91 | 88, 90 | opeq12d 4817 |
. . . . 5
β’ (π£ = β¨π§, π€β© β β¨(β‘πΉβ(1st βπ£)), (β‘πΊβ(2nd βπ£))β© = β¨(β‘πΉβπ§), (β‘πΊβπ€)β©) |
92 | 91 | mpompt 7416 |
. . . 4
β’ (π£ β (βͺ πΏ
Γ βͺ π) β¦ β¨(β‘πΉβ(1st βπ£)), (β‘πΊβ(2nd βπ£))β©) = (π§ β βͺ πΏ, π€ β βͺ π β¦ β¨(β‘πΉβπ§), (β‘πΊβπ€)β©) |
93 | 84, 92 | eqtrdi 2792 |
. . 3
β’ (π β β‘(π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΊβπ¦)β©) = (π§ β βͺ πΏ, π€ β βͺ π β¦ β¨(β‘πΉβπ§), (β‘πΊβπ€)β©)) |
94 | | cntop2 22433 |
. . . . . 6
β’ (πΉ β (π½ Cn πΏ) β πΏ β Top) |
95 | 3, 94 | syl 17 |
. . . . 5
β’ (π β πΏ β Top) |
96 | 31 | toptopon 22107 |
. . . . 5
β’ (πΏ β Top β πΏ β (TopOnββͺ πΏ)) |
97 | 95, 96 | sylib 217 |
. . . 4
β’ (π β πΏ β (TopOnββͺ πΏ)) |
98 | | cntop2 22433 |
. . . . . 6
β’ (πΊ β (πΎ Cn π) β π β Top) |
99 | 11, 98 | syl 17 |
. . . . 5
β’ (π β π β Top) |
100 | 37 | toptopon 22107 |
. . . . 5
β’ (π β Top β π β (TopOnββͺ π)) |
101 | 99, 100 | sylib 217 |
. . . 4
β’ (π β π β (TopOnββͺ π)) |
102 | 97, 101 | cnmpt1st 22860 |
. . . . 5
β’ (π β (π§ β βͺ πΏ, π€ β βͺ π β¦ π§) β ((πΏ Γt π) Cn πΏ)) |
103 | | hmeocnvcn 22953 |
. . . . . 6
β’ (πΉ β (π½HomeoπΏ) β β‘πΉ β (πΏ Cn π½)) |
104 | 1, 103 | syl 17 |
. . . . 5
β’ (π β β‘πΉ β (πΏ Cn π½)) |
105 | 97, 101, 102, 104 | cnmpt21f 22864 |
. . . 4
β’ (π β (π§ β βͺ πΏ, π€ β βͺ π β¦ (β‘πΉβπ§)) β ((πΏ Γt π) Cn π½)) |
106 | 97, 101 | cnmpt2nd 22861 |
. . . . 5
β’ (π β (π§ β βͺ πΏ, π€ β βͺ π β¦ π€) β ((πΏ Γt π) Cn π)) |
107 | | hmeocnvcn 22953 |
. . . . . 6
β’ (πΊ β (πΎHomeoπ) β β‘πΊ β (π Cn πΎ)) |
108 | 9, 107 | syl 17 |
. . . . 5
β’ (π β β‘πΊ β (π Cn πΎ)) |
109 | 97, 101, 106, 108 | cnmpt21f 22864 |
. . . 4
β’ (π β (π§ β βͺ πΏ, π€ β βͺ π β¦ (β‘πΊβπ€)) β ((πΏ Γt π) Cn πΎ)) |
110 | 97, 101, 105, 109 | cnmpt2t 22865 |
. . 3
β’ (π β (π§ β βͺ πΏ, π€ β βͺ π β¦ β¨(β‘πΉβπ§), (β‘πΊβπ€)β©) β ((πΏ Γt π) Cn (π½ Γt πΎ))) |
111 | 93, 110 | eqeltrd 2837 |
. 2
β’ (π β β‘(π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΊβπ¦)β©) β ((πΏ Γt π) Cn (π½ Γt πΎ))) |
112 | | ishmeo 22951 |
. 2
β’ ((π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΊβπ¦)β©) β ((π½ Γt πΎ)Homeo(πΏ Γt π)) β ((π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΊβπ¦)β©) β ((π½ Γt πΎ) Cn (πΏ Γt π)) β§ β‘(π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΊβπ¦)β©) β ((πΏ Γt π) Cn (π½ Γt πΎ)))) |
113 | 21, 111, 112 | sylanbrc 584 |
1
β’ (π β (π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΊβπ¦)β©) β ((π½ Γt πΎ)Homeo(πΏ Γt π))) |