Step | Hyp | Ref
| Expression |
1 | | xkohmeo.f |
. . 3
β’ πΉ = (π β ((π½ Γt πΎ) Cn πΏ) β¦ (π₯ β π β¦ (π¦ β π β¦ (π₯ππ¦)))) |
2 | | xkohmeo.x |
. . . . . . 7
β’ (π β π½ β (TopOnβπ)) |
3 | | xkohmeo.y |
. . . . . . 7
β’ (π β πΎ β (TopOnβπ)) |
4 | | txtopon 23095 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π½ Γt πΎ) β (TopOnβ(π Γ π))) |
5 | 2, 3, 4 | syl2anc 585 |
. . . . . 6
β’ (π β (π½ Γt πΎ) β (TopOnβ(π Γ π))) |
6 | | topontop 22415 |
. . . . . 6
β’ ((π½ Γt πΎ) β (TopOnβ(π Γ π)) β (π½ Γt πΎ) β Top) |
7 | 5, 6 | syl 17 |
. . . . 5
β’ (π β (π½ Γt πΎ) β Top) |
8 | | xkohmeo.l |
. . . . 5
β’ (π β πΏ β Top) |
9 | | eqid 2733 |
. . . . . 6
β’ (πΏ βko (π½ Γt πΎ)) = (πΏ βko (π½ Γt πΎ)) |
10 | 9 | xkotopon 23104 |
. . . . 5
β’ (((π½ Γt πΎ) β Top β§ πΏ β Top) β (πΏ βko (π½ Γt πΎ)) β (TopOnβ((π½ Γt πΎ) Cn πΏ))) |
11 | 7, 8, 10 | syl2anc 585 |
. . . 4
β’ (π β (πΏ βko (π½ Γt πΎ)) β (TopOnβ((π½ Γt πΎ) Cn πΏ))) |
12 | | vex 3479 |
. . . . . . . . 9
β’ π β V |
13 | | vex 3479 |
. . . . . . . . 9
β’ π₯ β V |
14 | 12, 13 | op1std 7985 |
. . . . . . . 8
β’ (π§ = β¨π, π₯β© β (1st βπ§) = π) |
15 | 12, 13 | op2ndd 7986 |
. . . . . . . 8
β’ (π§ = β¨π, π₯β© β (2nd βπ§) = π₯) |
16 | | eqidd 2734 |
. . . . . . . 8
β’ (π§ = β¨π, π₯β© β π¦ = π¦) |
17 | 14, 15, 16 | oveq123d 7430 |
. . . . . . 7
β’ (π§ = β¨π, π₯β© β ((2nd βπ§)(1st βπ§)π¦) = (π₯ππ¦)) |
18 | 17 | mpteq2dv 5251 |
. . . . . 6
β’ (π§ = β¨π, π₯β© β (π¦ β π β¦ ((2nd βπ§)(1st βπ§)π¦)) = (π¦ β π β¦ (π₯ππ¦))) |
19 | 18 | mpompt 7522 |
. . . . 5
β’ (π§ β (((π½ Γt πΎ) Cn πΏ) Γ π) β¦ (π¦ β π β¦ ((2nd βπ§)(1st βπ§)π¦))) = (π β ((π½ Γt πΎ) Cn πΏ), π₯ β π β¦ (π¦ β π β¦ (π₯ππ¦))) |
20 | | txtopon 23095 |
. . . . . . 7
β’ (((πΏ βko (π½ Γt πΎ)) β (TopOnβ((π½ Γt πΎ) Cn πΏ)) β§ π½ β (TopOnβπ)) β ((πΏ βko (π½ Γt πΎ)) Γt π½) β (TopOnβ(((π½ Γt πΎ) Cn πΏ) Γ π))) |
21 | 11, 2, 20 | syl2anc 585 |
. . . . . 6
β’ (π β ((πΏ βko (π½ Γt πΎ)) Γt π½) β (TopOnβ(((π½ Γt πΎ) Cn πΏ) Γ π))) |
22 | | vex 3479 |
. . . . . . . . . . 11
β’ π§ β V |
23 | | vex 3479 |
. . . . . . . . . . 11
β’ π¦ β V |
24 | 22, 23 | op1std 7985 |
. . . . . . . . . 10
β’ (π€ = β¨π§, π¦β© β (1st βπ€) = π§) |
25 | 24 | fveq2d 6896 |
. . . . . . . . 9
β’ (π€ = β¨π§, π¦β© β (1st
β(1st βπ€)) = (1st βπ§)) |
26 | 24 | fveq2d 6896 |
. . . . . . . . 9
β’ (π€ = β¨π§, π¦β© β (2nd
β(1st βπ€)) = (2nd βπ§)) |
27 | 22, 23 | op2ndd 7986 |
. . . . . . . . 9
β’ (π€ = β¨π§, π¦β© β (2nd βπ€) = π¦) |
28 | 25, 26, 27 | oveq123d 7430 |
. . . . . . . 8
β’ (π€ = β¨π§, π¦β© β ((2nd
β(1st βπ€))(1st β(1st
βπ€))(2nd
βπ€)) =
((2nd βπ§)(1st βπ§)π¦)) |
29 | 28 | mpompt 7522 |
. . . . . . 7
β’ (π€ β ((((π½ Γt πΎ) Cn πΏ) Γ π) Γ π) β¦ ((2nd
β(1st βπ€))(1st β(1st
βπ€))(2nd
βπ€))) = (π§ β (((π½ Γt πΎ) Cn πΏ) Γ π), π¦ β π β¦ ((2nd βπ§)(1st βπ§)π¦)) |
30 | | txtopon 23095 |
. . . . . . . . 9
β’ ((((πΏ βko (π½ Γt πΎ)) Γt π½) β (TopOnβ(((π½ Γt πΎ) Cn πΏ) Γ π)) β§ πΎ β (TopOnβπ)) β (((πΏ βko (π½ Γt πΎ)) Γt π½) Γt πΎ) β (TopOnβ((((π½ Γt πΎ) Cn πΏ) Γ π) Γ π))) |
31 | 21, 3, 30 | syl2anc 585 |
. . . . . . . 8
β’ (π β (((πΏ βko (π½ Γt πΎ)) Γt π½) Γt πΎ) β (TopOnβ((((π½ Γt πΎ) Cn πΏ) Γ π) Γ π))) |
32 | | toptopon2 22420 |
. . . . . . . . 9
β’ (πΏ β Top β πΏ β (TopOnββͺ πΏ)) |
33 | 8, 32 | sylib 217 |
. . . . . . . 8
β’ (π β πΏ β (TopOnββͺ πΏ)) |
34 | | xkohmeo.j |
. . . . . . . . 9
β’ (π β π½ β π-Locally
Comp) |
35 | | xkohmeo.k |
. . . . . . . . 9
β’ (π β πΎ β π-Locally
Comp) |
36 | | txcmp 23147 |
. . . . . . . . . 10
β’ ((π₯ β Comp β§ π¦ β Comp) β (π₯ Γt π¦) β Comp) |
37 | 36 | txnlly 23141 |
. . . . . . . . 9
β’ ((π½ β π-Locally Comp
β§ πΎ β
π-Locally Comp) β (π½ Γt πΎ) β π-Locally
Comp) |
38 | 34, 35, 37 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π½ Γt πΎ) β π-Locally
Comp) |
39 | 25 | mpompt 7522 |
. . . . . . . . . 10
β’ (π€ β ((((π½ Γt πΎ) Cn πΏ) Γ π) Γ π) β¦ (1st
β(1st βπ€))) = (π§ β (((π½ Γt πΎ) Cn πΏ) Γ π), π¦ β π β¦ (1st βπ§)) |
40 | 5 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π€ β ((((π½ Γt πΎ) Cn πΏ) Γ π) Γ π)) β (π½ Γt πΎ) β (TopOnβ(π Γ π))) |
41 | 33 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π€ β ((((π½ Γt πΎ) Cn πΏ) Γ π) Γ π)) β πΏ β (TopOnββͺ πΏ)) |
42 | | xp1st 8007 |
. . . . . . . . . . . . . . 15
β’ (π€ β ((((π½ Γt πΎ) Cn πΏ) Γ π) Γ π) β (1st βπ€) β (((π½ Γt πΎ) Cn πΏ) Γ π)) |
43 | 42 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π€ β ((((π½ Γt πΎ) Cn πΏ) Γ π) Γ π)) β (1st βπ€) β (((π½ Γt πΎ) Cn πΏ) Γ π)) |
44 | | xp1st 8007 |
. . . . . . . . . . . . . 14
β’
((1st βπ€) β (((π½ Γt πΎ) Cn πΏ) Γ π) β (1st
β(1st βπ€)) β ((π½ Γt πΎ) Cn πΏ)) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π€ β ((((π½ Γt πΎ) Cn πΏ) Γ π) Γ π)) β (1st
β(1st βπ€)) β ((π½ Γt πΎ) Cn πΏ)) |
46 | | cnf2 22753 |
. . . . . . . . . . . . 13
β’ (((π½ Γt πΎ) β (TopOnβ(π Γ π)) β§ πΏ β (TopOnββͺ πΏ)
β§ (1st β(1st βπ€)) β ((π½ Γt πΎ) Cn πΏ)) β (1st
β(1st βπ€)):(π Γ π)βΆβͺ πΏ) |
47 | 40, 41, 45, 46 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π β§ π€ β ((((π½ Γt πΎ) Cn πΏ) Γ π) Γ π)) β (1st
β(1st βπ€)):(π Γ π)βΆβͺ πΏ) |
48 | 47 | feqmptd 6961 |
. . . . . . . . . . 11
β’ ((π β§ π€ β ((((π½ Γt πΎ) Cn πΏ) Γ π) Γ π)) β (1st
β(1st βπ€)) = (π’ β (π Γ π) β¦ ((1st
β(1st βπ€))βπ’))) |
49 | 48 | mpteq2dva 5249 |
. . . . . . . . . 10
β’ (π β (π€ β ((((π½ Γt πΎ) Cn πΏ) Γ π) Γ π) β¦ (1st
β(1st βπ€))) = (π€ β ((((π½ Γt πΎ) Cn πΏ) Γ π) Γ π) β¦ (π’ β (π Γ π) β¦ ((1st
β(1st βπ€))βπ’)))) |
50 | 39, 49 | eqtr3id 2787 |
. . . . . . . . 9
β’ (π β (π§ β (((π½ Γt πΎ) Cn πΏ) Γ π), π¦ β π β¦ (1st βπ§)) = (π€ β ((((π½ Γt πΎ) Cn πΏ) Γ π) Γ π) β¦ (π’ β (π Γ π) β¦ ((1st
β(1st βπ€))βπ’)))) |
51 | 21, 3 | cnmpt1st 23172 |
. . . . . . . . . 10
β’ (π β (π§ β (((π½ Γt πΎ) Cn πΏ) Γ π), π¦ β π β¦ π§) β ((((πΏ βko (π½ Γt πΎ)) Γt π½) Γt πΎ) Cn ((πΏ βko (π½ Γt πΎ)) Γt π½))) |
52 | | fveq2 6892 |
. . . . . . . . . . . 12
β’ (π‘ = π§ β (1st βπ‘) = (1st βπ§)) |
53 | 52 | cbvmptv 5262 |
. . . . . . . . . . 11
β’ (π‘ β (((π½ Γt πΎ) Cn πΏ) Γ π) β¦ (1st βπ‘)) = (π§ β (((π½ Γt πΎ) Cn πΏ) Γ π) β¦ (1st βπ§)) |
54 | 14 | mpompt 7522 |
. . . . . . . . . . . 12
β’ (π§ β (((π½ Γt πΎ) Cn πΏ) Γ π) β¦ (1st βπ§)) = (π β ((π½ Γt πΎ) Cn πΏ), π₯ β π β¦ π) |
55 | 11, 2 | cnmpt1st 23172 |
. . . . . . . . . . . 12
β’ (π β (π β ((π½ Γt πΎ) Cn πΏ), π₯ β π β¦ π) β (((πΏ βko (π½ Γt πΎ)) Γt π½) Cn (πΏ βko (π½ Γt πΎ)))) |
56 | 54, 55 | eqeltrid 2838 |
. . . . . . . . . . 11
β’ (π β (π§ β (((π½ Γt πΎ) Cn πΏ) Γ π) β¦ (1st βπ§)) β (((πΏ βko (π½ Γt πΎ)) Γt π½) Cn (πΏ βko (π½ Γt πΎ)))) |
57 | 53, 56 | eqeltrid 2838 |
. . . . . . . . . 10
β’ (π β (π‘ β (((π½ Γt πΎ) Cn πΏ) Γ π) β¦ (1st βπ‘)) β (((πΏ βko (π½ Γt πΎ)) Γt π½) Cn (πΏ βko (π½ Γt πΎ)))) |
58 | 21, 3, 51, 21, 57, 52 | cnmpt21 23175 |
. . . . . . . . 9
β’ (π β (π§ β (((π½ Γt πΎ) Cn πΏ) Γ π), π¦ β π β¦ (1st βπ§)) β ((((πΏ βko (π½ Γt πΎ)) Γt π½) Γt πΎ) Cn (πΏ βko (π½ Γt πΎ)))) |
59 | 50, 58 | eqeltrrd 2835 |
. . . . . . . 8
β’ (π β (π€ β ((((π½ Γt πΎ) Cn πΏ) Γ π) Γ π) β¦ (π’ β (π Γ π) β¦ ((1st
β(1st βπ€))βπ’))) β ((((πΏ βko (π½ Γt πΎ)) Γt π½) Γt πΎ) Cn (πΏ βko (π½ Γt πΎ)))) |
60 | 26 | mpompt 7522 |
. . . . . . . . . 10
β’ (π€ β ((((π½ Γt πΎ) Cn πΏ) Γ π) Γ π) β¦ (2nd
β(1st βπ€))) = (π§ β (((π½ Γt πΎ) Cn πΏ) Γ π), π¦ β π β¦ (2nd βπ§)) |
61 | | fveq2 6892 |
. . . . . . . . . . . . 13
β’ (π‘ = π§ β (2nd βπ‘) = (2nd βπ§)) |
62 | 61 | cbvmptv 5262 |
. . . . . . . . . . . 12
β’ (π‘ β (((π½ Γt πΎ) Cn πΏ) Γ π) β¦ (2nd βπ‘)) = (π§ β (((π½ Γt πΎ) Cn πΏ) Γ π) β¦ (2nd βπ§)) |
63 | 15 | mpompt 7522 |
. . . . . . . . . . . . 13
β’ (π§ β (((π½ Γt πΎ) Cn πΏ) Γ π) β¦ (2nd βπ§)) = (π β ((π½ Γt πΎ) Cn πΏ), π₯ β π β¦ π₯) |
64 | 11, 2 | cnmpt2nd 23173 |
. . . . . . . . . . . . 13
β’ (π β (π β ((π½ Γt πΎ) Cn πΏ), π₯ β π β¦ π₯) β (((πΏ βko (π½ Γt πΎ)) Γt π½) Cn π½)) |
65 | 63, 64 | eqeltrid 2838 |
. . . . . . . . . . . 12
β’ (π β (π§ β (((π½ Γt πΎ) Cn πΏ) Γ π) β¦ (2nd βπ§)) β (((πΏ βko (π½ Γt πΎ)) Γt π½) Cn π½)) |
66 | 62, 65 | eqeltrid 2838 |
. . . . . . . . . . 11
β’ (π β (π‘ β (((π½ Γt πΎ) Cn πΏ) Γ π) β¦ (2nd βπ‘)) β (((πΏ βko (π½ Γt πΎ)) Γt π½) Cn π½)) |
67 | 21, 3, 51, 21, 66, 61 | cnmpt21 23175 |
. . . . . . . . . 10
β’ (π β (π§ β (((π½ Γt πΎ) Cn πΏ) Γ π), π¦ β π β¦ (2nd βπ§)) β ((((πΏ βko (π½ Γt πΎ)) Γt π½) Γt πΎ) Cn π½)) |
68 | 60, 67 | eqeltrid 2838 |
. . . . . . . . 9
β’ (π β (π€ β ((((π½ Γt πΎ) Cn πΏ) Γ π) Γ π) β¦ (2nd
β(1st βπ€))) β ((((πΏ βko (π½ Γt πΎ)) Γt π½) Γt πΎ) Cn π½)) |
69 | 27 | mpompt 7522 |
. . . . . . . . . 10
β’ (π€ β ((((π½ Γt πΎ) Cn πΏ) Γ π) Γ π) β¦ (2nd βπ€)) = (π§ β (((π½ Γt πΎ) Cn πΏ) Γ π), π¦ β π β¦ π¦) |
70 | 21, 3 | cnmpt2nd 23173 |
. . . . . . . . . 10
β’ (π β (π§ β (((π½ Γt πΎ) Cn πΏ) Γ π), π¦ β π β¦ π¦) β ((((πΏ βko (π½ Γt πΎ)) Γt π½) Γt πΎ) Cn πΎ)) |
71 | 69, 70 | eqeltrid 2838 |
. . . . . . . . 9
β’ (π β (π€ β ((((π½ Γt πΎ) Cn πΏ) Γ π) Γ π) β¦ (2nd βπ€)) β ((((πΏ βko (π½ Γt πΎ)) Γt π½) Γt πΎ) Cn πΎ)) |
72 | 31, 68, 71 | cnmpt1t 23169 |
. . . . . . . 8
β’ (π β (π€ β ((((π½ Γt πΎ) Cn πΏ) Γ π) Γ π) β¦ β¨(2nd
β(1st βπ€)), (2nd βπ€)β©) β ((((πΏ βko (π½ Γt πΎ)) Γt π½) Γt πΎ) Cn (π½ Γt πΎ))) |
73 | | fveq2 6892 |
. . . . . . . . 9
β’ (π’ = β¨(2nd
β(1st βπ€)), (2nd βπ€)β© β ((1st
β(1st βπ€))βπ’) = ((1st β(1st
βπ€))ββ¨(2nd
β(1st βπ€)), (2nd βπ€)β©)) |
74 | | df-ov 7412 |
. . . . . . . . 9
β’
((2nd β(1st βπ€))(1st β(1st
βπ€))(2nd
βπ€)) =
((1st β(1st βπ€))ββ¨(2nd
β(1st βπ€)), (2nd βπ€)β©) |
75 | 73, 74 | eqtr4di 2791 |
. . . . . . . 8
β’ (π’ = β¨(2nd
β(1st βπ€)), (2nd βπ€)β© β ((1st
β(1st βπ€))βπ’) = ((2nd β(1st
βπ€))(1st
β(1st βπ€))(2nd βπ€))) |
76 | 31, 5, 33, 38, 59, 72, 75 | cnmptk1p 23189 |
. . . . . . 7
β’ (π β (π€ β ((((π½ Γt πΎ) Cn πΏ) Γ π) Γ π) β¦ ((2nd
β(1st βπ€))(1st β(1st
βπ€))(2nd
βπ€))) β
((((πΏ βko
(π½ Γt
πΎ)) Γt
π½) Γt
πΎ) Cn πΏ)) |
77 | 29, 76 | eqeltrrid 2839 |
. . . . . 6
β’ (π β (π§ β (((π½ Γt πΎ) Cn πΏ) Γ π), π¦ β π β¦ ((2nd βπ§)(1st βπ§)π¦)) β ((((πΏ βko (π½ Γt πΎ)) Γt π½) Γt πΎ) Cn πΏ)) |
78 | 21, 3, 77 | cnmpt2k 23192 |
. . . . 5
β’ (π β (π§ β (((π½ Γt πΎ) Cn πΏ) Γ π) β¦ (π¦ β π β¦ ((2nd βπ§)(1st βπ§)π¦))) β (((πΏ βko (π½ Γt πΎ)) Γt π½) Cn (πΏ βko πΎ))) |
79 | 19, 78 | eqeltrrid 2839 |
. . . 4
β’ (π β (π β ((π½ Γt πΎ) Cn πΏ), π₯ β π β¦ (π¦ β π β¦ (π₯ππ¦))) β (((πΏ βko (π½ Γt πΎ)) Γt π½) Cn (πΏ βko πΎ))) |
80 | 11, 2, 79 | cnmpt2k 23192 |
. . 3
β’ (π β (π β ((π½ Γt πΎ) Cn πΏ) β¦ (π₯ β π β¦ (π¦ β π β¦ (π₯ππ¦)))) β ((πΏ βko (π½ Γt πΎ)) Cn ((πΏ βko πΎ) βko π½))) |
81 | 1, 80 | eqeltrid 2838 |
. 2
β’ (π β πΉ β ((πΏ βko (π½ Γt πΎ)) Cn ((πΏ βko πΎ) βko π½))) |
82 | 2, 3, 1, 34, 35, 8 | xkocnv 23318 |
. . . 4
β’ (π β β‘πΉ = (π β (π½ Cn (πΏ βko πΎ)) β¦ (π₯ β π, π¦ β π β¦ ((πβπ₯)βπ¦)))) |
83 | 13, 23 | op1std 7985 |
. . . . . . . 8
β’ (π§ = β¨π₯, π¦β© β (1st βπ§) = π₯) |
84 | 83 | fveq2d 6896 |
. . . . . . 7
β’ (π§ = β¨π₯, π¦β© β (πβ(1st βπ§)) = (πβπ₯)) |
85 | 13, 23 | op2ndd 7986 |
. . . . . . 7
β’ (π§ = β¨π₯, π¦β© β (2nd βπ§) = π¦) |
86 | 84, 85 | fveq12d 6899 |
. . . . . 6
β’ (π§ = β¨π₯, π¦β© β ((πβ(1st βπ§))β(2nd
βπ§)) = ((πβπ₯)βπ¦)) |
87 | 86 | mpompt 7522 |
. . . . 5
β’ (π§ β (π Γ π) β¦ ((πβ(1st βπ§))β(2nd
βπ§))) = (π₯ β π, π¦ β π β¦ ((πβπ₯)βπ¦)) |
88 | 87 | mpteq2i 5254 |
. . . 4
β’ (π β (π½ Cn (πΏ βko πΎ)) β¦ (π§ β (π Γ π) β¦ ((πβ(1st βπ§))β(2nd
βπ§)))) = (π β (π½ Cn (πΏ βko πΎ)) β¦ (π₯ β π, π¦ β π β¦ ((πβπ₯)βπ¦))) |
89 | 82, 88 | eqtr4di 2791 |
. . 3
β’ (π β β‘πΉ = (π β (π½ Cn (πΏ βko πΎ)) β¦ (π§ β (π Γ π) β¦ ((πβ(1st βπ§))β(2nd
βπ§))))) |
90 | | nllytop 22977 |
. . . . . 6
β’ (π½ β π-Locally Comp
β π½ β
Top) |
91 | 34, 90 | syl 17 |
. . . . 5
β’ (π β π½ β Top) |
92 | | nllytop 22977 |
. . . . . . 7
β’ (πΎ β π-Locally Comp
β πΎ β
Top) |
93 | 35, 92 | syl 17 |
. . . . . 6
β’ (π β πΎ β Top) |
94 | | xkotop 23092 |
. . . . . 6
β’ ((πΎ β Top β§ πΏ β Top) β (πΏ βko πΎ) β Top) |
95 | 93, 8, 94 | syl2anc 585 |
. . . . 5
β’ (π β (πΏ βko πΎ) β Top) |
96 | | eqid 2733 |
. . . . . 6
β’ ((πΏ βko πΎ) βko π½) = ((πΏ βko πΎ) βko π½) |
97 | 96 | xkotopon 23104 |
. . . . 5
β’ ((π½ β Top β§ (πΏ βko πΎ) β Top) β ((πΏ βko πΎ) βko π½) β (TopOnβ(π½ Cn (πΏ βko πΎ)))) |
98 | 91, 95, 97 | syl2anc 585 |
. . . 4
β’ (π β ((πΏ βko πΎ) βko π½) β (TopOnβ(π½ Cn (πΏ βko πΎ)))) |
99 | | vex 3479 |
. . . . . . . . 9
β’ π β V |
100 | 99, 22 | op1std 7985 |
. . . . . . . 8
β’ (π€ = β¨π, π§β© β (1st βπ€) = π) |
101 | 99, 22 | op2ndd 7986 |
. . . . . . . . 9
β’ (π€ = β¨π, π§β© β (2nd βπ€) = π§) |
102 | 101 | fveq2d 6896 |
. . . . . . . 8
β’ (π€ = β¨π, π§β© β (1st
β(2nd βπ€)) = (1st βπ§)) |
103 | 100, 102 | fveq12d 6899 |
. . . . . . 7
β’ (π€ = β¨π, π§β© β ((1st βπ€)β(1st
β(2nd βπ€))) = (πβ(1st βπ§))) |
104 | 101 | fveq2d 6896 |
. . . . . . 7
β’ (π€ = β¨π, π§β© β (2nd
β(2nd βπ€)) = (2nd βπ§)) |
105 | 103, 104 | fveq12d 6899 |
. . . . . 6
β’ (π€ = β¨π, π§β© β (((1st βπ€)β(1st
β(2nd βπ€)))β(2nd
β(2nd βπ€))) = ((πβ(1st βπ§))β(2nd
βπ§))) |
106 | 105 | mpompt 7522 |
. . . . 5
β’ (π€ β ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π)) β¦ (((1st βπ€)β(1st
β(2nd βπ€)))β(2nd
β(2nd βπ€)))) = (π β (π½ Cn (πΏ βko πΎ)), π§ β (π Γ π) β¦ ((πβ(1st βπ§))β(2nd
βπ§))) |
107 | | txtopon 23095 |
. . . . . . 7
β’ ((((πΏ βko πΎ) βko π½) β (TopOnβ(π½ Cn (πΏ βko πΎ))) β§ (π½ Γt πΎ) β (TopOnβ(π Γ π))) β (((πΏ βko πΎ) βko π½) Γt (π½ Γt πΎ)) β (TopOnβ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π)))) |
108 | 98, 5, 107 | syl2anc 585 |
. . . . . 6
β’ (π β (((πΏ βko πΎ) βko π½) Γt (π½ Γt πΎ)) β (TopOnβ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π)))) |
109 | 3 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π€ β ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π))) β πΎ β (TopOnβπ)) |
110 | 33 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π€ β ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π))) β πΏ β (TopOnββͺ πΏ)) |
111 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ (πΏ βko πΎ) = (πΏ βko πΎ) |
112 | 111 | xkotopon 23104 |
. . . . . . . . . . . . 13
β’ ((πΎ β Top β§ πΏ β Top) β (πΏ βko πΎ) β (TopOnβ(πΎ Cn πΏ))) |
113 | 93, 8, 112 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (πΏ βko πΎ) β (TopOnβ(πΎ Cn πΏ))) |
114 | | xp1st 8007 |
. . . . . . . . . . . 12
β’ (π€ β ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π)) β (1st βπ€) β (π½ Cn (πΏ βko πΎ))) |
115 | | cnf2 22753 |
. . . . . . . . . . . 12
β’ ((π½ β (TopOnβπ) β§ (πΏ βko πΎ) β (TopOnβ(πΎ Cn πΏ)) β§ (1st βπ€) β (π½ Cn (πΏ βko πΎ))) β (1st βπ€):πβΆ(πΎ Cn πΏ)) |
116 | 2, 113, 114, 115 | syl2an3an 1423 |
. . . . . . . . . . 11
β’ ((π β§ π€ β ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π))) β (1st βπ€):πβΆ(πΎ Cn πΏ)) |
117 | | xp2nd 8008 |
. . . . . . . . . . . . 13
β’ (π€ β ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π)) β (2nd βπ€) β (π Γ π)) |
118 | 117 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π€ β ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π))) β (2nd βπ€) β (π Γ π)) |
119 | | xp1st 8007 |
. . . . . . . . . . . 12
β’
((2nd βπ€) β (π Γ π) β (1st
β(2nd βπ€)) β π) |
120 | 118, 119 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π€ β ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π))) β (1st
β(2nd βπ€)) β π) |
121 | 116, 120 | ffvelcdmd 7088 |
. . . . . . . . . 10
β’ ((π β§ π€ β ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π))) β ((1st βπ€)β(1st
β(2nd βπ€))) β (πΎ Cn πΏ)) |
122 | | cnf2 22753 |
. . . . . . . . . 10
β’ ((πΎ β (TopOnβπ) β§ πΏ β (TopOnββͺ πΏ)
β§ ((1st βπ€)β(1st
β(2nd βπ€))) β (πΎ Cn πΏ)) β ((1st βπ€)β(1st
β(2nd βπ€))):πβΆβͺ πΏ) |
123 | 109, 110,
121, 122 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π€ β ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π))) β ((1st βπ€)β(1st
β(2nd βπ€))):πβΆβͺ πΏ) |
124 | 123 | feqmptd 6961 |
. . . . . . . 8
β’ ((π β§ π€ β ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π))) β ((1st βπ€)β(1st
β(2nd βπ€))) = (π¦ β π β¦ (((1st βπ€)β(1st
β(2nd βπ€)))βπ¦))) |
125 | 124 | mpteq2dva 5249 |
. . . . . . 7
β’ (π β (π€ β ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π)) β¦ ((1st βπ€)β(1st
β(2nd βπ€)))) = (π€ β ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π)) β¦ (π¦ β π β¦ (((1st βπ€)β(1st
β(2nd βπ€)))βπ¦)))) |
126 | 100 | mpompt 7522 |
. . . . . . . . . 10
β’ (π€ β ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π)) β¦ (1st βπ€)) = (π β (π½ Cn (πΏ βko πΎ)), π§ β (π Γ π) β¦ π) |
127 | 116 | feqmptd 6961 |
. . . . . . . . . . 11
β’ ((π β§ π€ β ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π))) β (1st βπ€) = (π₯ β π β¦ ((1st βπ€)βπ₯))) |
128 | 127 | mpteq2dva 5249 |
. . . . . . . . . 10
β’ (π β (π€ β ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π)) β¦ (1st βπ€)) = (π€ β ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π)) β¦ (π₯ β π β¦ ((1st βπ€)βπ₯)))) |
129 | 126, 128 | eqtr3id 2787 |
. . . . . . . . 9
β’ (π β (π β (π½ Cn (πΏ βko πΎ)), π§ β (π Γ π) β¦ π) = (π€ β ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π)) β¦ (π₯ β π β¦ ((1st βπ€)βπ₯)))) |
130 | 98, 5 | cnmpt1st 23172 |
. . . . . . . . 9
β’ (π β (π β (π½ Cn (πΏ βko πΎ)), π§ β (π Γ π) β¦ π) β ((((πΏ βko πΎ) βko π½) Γt (π½ Γt πΎ)) Cn ((πΏ βko πΎ) βko π½))) |
131 | 129, 130 | eqeltrrd 2835 |
. . . . . . . 8
β’ (π β (π€ β ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π)) β¦ (π₯ β π β¦ ((1st βπ€)βπ₯))) β ((((πΏ βko πΎ) βko π½) Γt (π½ Γt πΎ)) Cn ((πΏ βko πΎ) βko π½))) |
132 | 102 | mpompt 7522 |
. . . . . . . . 9
β’ (π€ β ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π)) β¦ (1st
β(2nd βπ€))) = (π β (π½ Cn (πΏ βko πΎ)), π§ β (π Γ π) β¦ (1st βπ§)) |
133 | 98, 5 | cnmpt2nd 23173 |
. . . . . . . . . 10
β’ (π β (π β (π½ Cn (πΏ βko πΎ)), π§ β (π Γ π) β¦ π§) β ((((πΏ βko πΎ) βko π½) Γt (π½ Γt πΎ)) Cn (π½ Γt πΎ))) |
134 | 52 | cbvmptv 5262 |
. . . . . . . . . . 11
β’ (π‘ β (π Γ π) β¦ (1st βπ‘)) = (π§ β (π Γ π) β¦ (1st βπ§)) |
135 | 83 | mpompt 7522 |
. . . . . . . . . . . 12
β’ (π§ β (π Γ π) β¦ (1st βπ§)) = (π₯ β π, π¦ β π β¦ π₯) |
136 | 2, 3 | cnmpt1st 23172 |
. . . . . . . . . . . 12
β’ (π β (π₯ β π, π¦ β π β¦ π₯) β ((π½ Γt πΎ) Cn π½)) |
137 | 135, 136 | eqeltrid 2838 |
. . . . . . . . . . 11
β’ (π β (π§ β (π Γ π) β¦ (1st βπ§)) β ((π½ Γt πΎ) Cn π½)) |
138 | 134, 137 | eqeltrid 2838 |
. . . . . . . . . 10
β’ (π β (π‘ β (π Γ π) β¦ (1st βπ‘)) β ((π½ Γt πΎ) Cn π½)) |
139 | 98, 5, 133, 5, 138, 52 | cnmpt21 23175 |
. . . . . . . . 9
β’ (π β (π β (π½ Cn (πΏ βko πΎ)), π§ β (π Γ π) β¦ (1st βπ§)) β ((((πΏ βko πΎ) βko π½) Γt (π½ Γt πΎ)) Cn π½)) |
140 | 132, 139 | eqeltrid 2838 |
. . . . . . . 8
β’ (π β (π€ β ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π)) β¦ (1st
β(2nd βπ€))) β ((((πΏ βko πΎ) βko π½) Γt (π½ Γt πΎ)) Cn π½)) |
141 | | fveq2 6892 |
. . . . . . . 8
β’ (π₯ = (1st
β(2nd βπ€)) β ((1st βπ€)βπ₯) = ((1st βπ€)β(1st
β(2nd βπ€)))) |
142 | 108, 2, 113, 34, 131, 140, 141 | cnmptk1p 23189 |
. . . . . . 7
β’ (π β (π€ β ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π)) β¦ ((1st βπ€)β(1st
β(2nd βπ€)))) β ((((πΏ βko πΎ) βko π½) Γt (π½ Γt πΎ)) Cn (πΏ βko πΎ))) |
143 | 125, 142 | eqeltrrd 2835 |
. . . . . 6
β’ (π β (π€ β ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π)) β¦ (π¦ β π β¦ (((1st βπ€)β(1st
β(2nd βπ€)))βπ¦))) β ((((πΏ βko πΎ) βko π½) Γt (π½ Γt πΎ)) Cn (πΏ βko πΎ))) |
144 | 104 | mpompt 7522 |
. . . . . . 7
β’ (π€ β ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π)) β¦ (2nd
β(2nd βπ€))) = (π β (π½ Cn (πΏ βko πΎ)), π§ β (π Γ π) β¦ (2nd βπ§)) |
145 | 61 | cbvmptv 5262 |
. . . . . . . . 9
β’ (π‘ β (π Γ π) β¦ (2nd βπ‘)) = (π§ β (π Γ π) β¦ (2nd βπ§)) |
146 | 85 | mpompt 7522 |
. . . . . . . . . 10
β’ (π§ β (π Γ π) β¦ (2nd βπ§)) = (π₯ β π, π¦ β π β¦ π¦) |
147 | 2, 3 | cnmpt2nd 23173 |
. . . . . . . . . 10
β’ (π β (π₯ β π, π¦ β π β¦ π¦) β ((π½ Γt πΎ) Cn πΎ)) |
148 | 146, 147 | eqeltrid 2838 |
. . . . . . . . 9
β’ (π β (π§ β (π Γ π) β¦ (2nd βπ§)) β ((π½ Γt πΎ) Cn πΎ)) |
149 | 145, 148 | eqeltrid 2838 |
. . . . . . . 8
β’ (π β (π‘ β (π Γ π) β¦ (2nd βπ‘)) β ((π½ Γt πΎ) Cn πΎ)) |
150 | 98, 5, 133, 5, 149, 61 | cnmpt21 23175 |
. . . . . . 7
β’ (π β (π β (π½ Cn (πΏ βko πΎ)), π§ β (π Γ π) β¦ (2nd βπ§)) β ((((πΏ βko πΎ) βko π½) Γt (π½ Γt πΎ)) Cn πΎ)) |
151 | 144, 150 | eqeltrid 2838 |
. . . . . 6
β’ (π β (π€ β ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π)) β¦ (2nd
β(2nd βπ€))) β ((((πΏ βko πΎ) βko π½) Γt (π½ Γt πΎ)) Cn πΎ)) |
152 | | fveq2 6892 |
. . . . . 6
β’ (π¦ = (2nd
β(2nd βπ€)) β (((1st βπ€)β(1st
β(2nd βπ€)))βπ¦) = (((1st βπ€)β(1st
β(2nd βπ€)))β(2nd
β(2nd βπ€)))) |
153 | 108, 3, 33, 35, 143, 151, 152 | cnmptk1p 23189 |
. . . . 5
β’ (π β (π€ β ((π½ Cn (πΏ βko πΎ)) Γ (π Γ π)) β¦ (((1st βπ€)β(1st
β(2nd βπ€)))β(2nd
β(2nd βπ€)))) β ((((πΏ βko πΎ) βko π½) Γt (π½ Γt πΎ)) Cn πΏ)) |
154 | 106, 153 | eqeltrrid 2839 |
. . . 4
β’ (π β (π β (π½ Cn (πΏ βko πΎ)), π§ β (π Γ π) β¦ ((πβ(1st βπ§))β(2nd
βπ§))) β
((((πΏ βko
πΎ) βko
π½) Γt
(π½ Γt
πΎ)) Cn πΏ)) |
155 | 98, 5, 154 | cnmpt2k 23192 |
. . 3
β’ (π β (π β (π½ Cn (πΏ βko πΎ)) β¦ (π§ β (π Γ π) β¦ ((πβ(1st βπ§))β(2nd
βπ§)))) β
(((πΏ βko
πΎ) βko
π½) Cn (πΏ βko (π½ Γt πΎ)))) |
156 | 89, 155 | eqeltrd 2834 |
. 2
β’ (π β β‘πΉ β (((πΏ βko πΎ) βko π½) Cn (πΏ βko (π½ Γt πΎ)))) |
157 | | ishmeo 23263 |
. 2
β’ (πΉ β ((πΏ βko (π½ Γt πΎ))Homeo((πΏ βko πΎ) βko π½)) β (πΉ β ((πΏ βko (π½ Γt πΎ)) Cn ((πΏ βko πΎ) βko π½)) β§ β‘πΉ β (((πΏ βko πΎ) βko π½) Cn (πΏ βko (π½ Γt πΎ))))) |
158 | 81, 156, 157 | sylanbrc 584 |
1
β’ (π β πΉ β ((πΏ βko (π½ Γt πΎ))Homeo((πΏ βko πΎ) βko π½))) |