Step | Hyp | Ref
| Expression |
1 | | nffvmpt1 6857 |
. . . . 5
β’
β²π₯((π₯ β π β¦ (π¦ β π β¦ π΄))βπ€) |
2 | | nfcv 2904 |
. . . . 5
β’
β²π₯π |
3 | 1, 2 | nffv 6856 |
. . . 4
β’
β²π₯(((π₯ β π β¦ (π¦ β π β¦ π΄))βπ€)βπ) |
4 | | nfcv 2904 |
. . . . . . 7
β’
β²π¦π |
5 | | nfmpt1 5217 |
. . . . . . 7
β’
β²π¦(π¦ β π β¦ π΄) |
6 | 4, 5 | nfmpt 5216 |
. . . . . 6
β’
β²π¦(π₯ β π β¦ (π¦ β π β¦ π΄)) |
7 | | nfcv 2904 |
. . . . . 6
β’
β²π¦π€ |
8 | 6, 7 | nffv 6856 |
. . . . 5
β’
β²π¦((π₯ β π β¦ (π¦ β π β¦ π΄))βπ€) |
9 | | nfcv 2904 |
. . . . 5
β’
β²π¦π |
10 | 8, 9 | nffv 6856 |
. . . 4
β’
β²π¦(((π₯ β π β¦ (π¦ β π β¦ π΄))βπ€)βπ) |
11 | | nfcv 2904 |
. . . 4
β’
β²π€(((π₯ β π β¦ (π¦ β π β¦ π΄))βπ₯)βπ¦) |
12 | | nfcv 2904 |
. . . 4
β’
β²π(((π₯ β π β¦ (π¦ β π β¦ π΄))βπ₯)βπ¦) |
13 | | fveq2 6846 |
. . . . . 6
β’ (π€ = π₯ β ((π₯ β π β¦ (π¦ β π β¦ π΄))βπ€) = ((π₯ β π β¦ (π¦ β π β¦ π΄))βπ₯)) |
14 | 13 | fveq1d 6848 |
. . . . 5
β’ (π€ = π₯ β (((π₯ β π β¦ (π¦ β π β¦ π΄))βπ€)βπ) = (((π₯ β π β¦ (π¦ β π β¦ π΄))βπ₯)βπ)) |
15 | | fveq2 6846 |
. . . . 5
β’ (π = π¦ β (((π₯ β π β¦ (π¦ β π β¦ π΄))βπ₯)βπ) = (((π₯ β π β¦ (π¦ β π β¦ π΄))βπ₯)βπ¦)) |
16 | 14, 15 | sylan9eq 2793 |
. . . 4
β’ ((π€ = π₯ β§ π = π¦) β (((π₯ β π β¦ (π¦ β π β¦ π΄))βπ€)βπ) = (((π₯ β π β¦ (π¦ β π β¦ π΄))βπ₯)βπ¦)) |
17 | 3, 10, 11, 12, 16 | cbvmpo 7455 |
. . 3
β’ (π€ β π, π β π β¦ (((π₯ β π β¦ (π¦ β π β¦ π΄))βπ€)βπ)) = (π₯ β π, π¦ β π β¦ (((π₯ β π β¦ (π¦ β π β¦ π΄))βπ₯)βπ¦)) |
18 | | simplr 768 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ π¦ β π) β π₯ β π) |
19 | | cnmptk1p.j |
. . . . . . . . . . 11
β’ (π β π½ β (TopOnβπ)) |
20 | | cnmptk1p.n |
. . . . . . . . . . . . 13
β’ (π β πΎ β π-Locally
Comp) |
21 | | nllytop 22847 |
. . . . . . . . . . . . 13
β’ (πΎ β π-Locally Comp
β πΎ β
Top) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . 12
β’ (π β πΎ β Top) |
23 | | cnmptk1p.l |
. . . . . . . . . . . . 13
β’ (π β πΏ β (TopOnβπ)) |
24 | | topontop 22285 |
. . . . . . . . . . . . 13
β’ (πΏ β (TopOnβπ) β πΏ β Top) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . 12
β’ (π β πΏ β Top) |
26 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (πΏ βko πΎ) = (πΏ βko πΎ) |
27 | 26 | xkotopon 22974 |
. . . . . . . . . . . 12
β’ ((πΎ β Top β§ πΏ β Top) β (πΏ βko πΎ) β (TopOnβ(πΎ Cn πΏ))) |
28 | 22, 25, 27 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (πΏ βko πΎ) β (TopOnβ(πΎ Cn πΏ))) |
29 | | cnmptk2.a |
. . . . . . . . . . 11
β’ (π β (π₯ β π β¦ (π¦ β π β¦ π΄)) β (π½ Cn (πΏ βko πΎ))) |
30 | | cnf2 22623 |
. . . . . . . . . . 11
β’ ((π½ β (TopOnβπ) β§ (πΏ βko πΎ) β (TopOnβ(πΎ Cn πΏ)) β§ (π₯ β π β¦ (π¦ β π β¦ π΄)) β (π½ Cn (πΏ βko πΎ))) β (π₯ β π β¦ (π¦ β π β¦ π΄)):πβΆ(πΎ Cn πΏ)) |
31 | 19, 28, 29, 30 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β (π₯ β π β¦ (π¦ β π β¦ π΄)):πβΆ(πΎ Cn πΏ)) |
32 | 31 | fvmptelcdm 7065 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β (π¦ β π β¦ π΄) β (πΎ Cn πΏ)) |
33 | 32 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ π¦ β π) β (π¦ β π β¦ π΄) β (πΎ Cn πΏ)) |
34 | | eqid 2733 |
. . . . . . . . 9
β’ (π₯ β π β¦ (π¦ β π β¦ π΄)) = (π₯ β π β¦ (π¦ β π β¦ π΄)) |
35 | 34 | fvmpt2 6963 |
. . . . . . . 8
β’ ((π₯ β π β§ (π¦ β π β¦ π΄) β (πΎ Cn πΏ)) β ((π₯ β π β¦ (π¦ β π β¦ π΄))βπ₯) = (π¦ β π β¦ π΄)) |
36 | 18, 33, 35 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ π₯ β π) β§ π¦ β π) β ((π₯ β π β¦ (π¦ β π β¦ π΄))βπ₯) = (π¦ β π β¦ π΄)) |
37 | 36 | fveq1d 6848 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ π¦ β π) β (((π₯ β π β¦ (π¦ β π β¦ π΄))βπ₯)βπ¦) = ((π¦ β π β¦ π΄)βπ¦)) |
38 | | simpr 486 |
. . . . . . 7
β’ (((π β§ π₯ β π) β§ π¦ β π) β π¦ β π) |
39 | | cnmptk1p.k |
. . . . . . . . . 10
β’ (π β πΎ β (TopOnβπ)) |
40 | 39 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β πΎ β (TopOnβπ)) |
41 | 23 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β πΏ β (TopOnβπ)) |
42 | | cnf2 22623 |
. . . . . . . . 9
β’ ((πΎ β (TopOnβπ) β§ πΏ β (TopOnβπ) β§ (π¦ β π β¦ π΄) β (πΎ Cn πΏ)) β (π¦ β π β¦ π΄):πβΆπ) |
43 | 40, 41, 32, 42 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β (π¦ β π β¦ π΄):πβΆπ) |
44 | 43 | fvmptelcdm 7065 |
. . . . . . 7
β’ (((π β§ π₯ β π) β§ π¦ β π) β π΄ β π) |
45 | | eqid 2733 |
. . . . . . . 8
β’ (π¦ β π β¦ π΄) = (π¦ β π β¦ π΄) |
46 | 45 | fvmpt2 6963 |
. . . . . . 7
β’ ((π¦ β π β§ π΄ β π) β ((π¦ β π β¦ π΄)βπ¦) = π΄) |
47 | 38, 44, 46 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ π¦ β π) β ((π¦ β π β¦ π΄)βπ¦) = π΄) |
48 | 37, 47 | eqtrd 2773 |
. . . . 5
β’ (((π β§ π₯ β π) β§ π¦ β π) β (((π₯ β π β¦ (π¦ β π β¦ π΄))βπ₯)βπ¦) = π΄) |
49 | 48 | 3impa 1111 |
. . . 4
β’ ((π β§ π₯ β π β§ π¦ β π) β (((π₯ β π β¦ (π¦ β π β¦ π΄))βπ₯)βπ¦) = π΄) |
50 | 49 | mpoeq3dva 7438 |
. . 3
β’ (π β (π₯ β π, π¦ β π β¦ (((π₯ β π β¦ (π¦ β π β¦ π΄))βπ₯)βπ¦)) = (π₯ β π, π¦ β π β¦ π΄)) |
51 | 17, 50 | eqtrid 2785 |
. 2
β’ (π β (π€ β π, π β π β¦ (((π₯ β π β¦ (π¦ β π β¦ π΄))βπ€)βπ)) = (π₯ β π, π¦ β π β¦ π΄)) |
52 | 19, 39 | cnmpt1st 23042 |
. . . 4
β’ (π β (π€ β π, π β π β¦ π€) β ((π½ Γt πΎ) Cn π½)) |
53 | 19, 39, 52, 29 | cnmpt21f 23046 |
. . 3
β’ (π β (π€ β π, π β π β¦ ((π₯ β π β¦ (π¦ β π β¦ π΄))βπ€)) β ((π½ Γt πΎ) Cn (πΏ βko πΎ))) |
54 | 19, 39 | cnmpt2nd 23043 |
. . 3
β’ (π β (π€ β π, π β π β¦ π) β ((π½ Γt πΎ) Cn πΎ)) |
55 | | eqid 2733 |
. . . . 5
β’ (πΎ Cn πΏ) = (πΎ Cn πΏ) |
56 | | toponuni 22286 |
. . . . . 6
β’ (πΎ β (TopOnβπ) β π = βͺ πΎ) |
57 | 39, 56 | syl 17 |
. . . . 5
β’ (π β π = βͺ πΎ) |
58 | | mpoeq12 7434 |
. . . . 5
β’ (((πΎ Cn πΏ) = (πΎ Cn πΏ) β§ π = βͺ πΎ) β (π β (πΎ Cn πΏ), π§ β π β¦ (πβπ§)) = (π β (πΎ Cn πΏ), π§ β βͺ πΎ β¦ (πβπ§))) |
59 | 55, 57, 58 | sylancr 588 |
. . . 4
β’ (π β (π β (πΎ Cn πΏ), π§ β π β¦ (πβπ§)) = (π β (πΎ Cn πΏ), π§ β βͺ πΎ β¦ (πβπ§))) |
60 | | eqid 2733 |
. . . . . 6
β’ βͺ πΎ =
βͺ πΎ |
61 | | eqid 2733 |
. . . . . 6
β’ (π β (πΎ Cn πΏ), π§ β βͺ πΎ β¦ (πβπ§)) = (π β (πΎ Cn πΏ), π§ β βͺ πΎ β¦ (πβπ§)) |
62 | 60, 61 | xkofvcn 23058 |
. . . . 5
β’ ((πΎ β π-Locally Comp
β§ πΏ β Top) β
(π β (πΎ Cn πΏ), π§ β βͺ πΎ β¦ (πβπ§)) β (((πΏ βko πΎ) Γt πΎ) Cn πΏ)) |
63 | 20, 25, 62 | syl2anc 585 |
. . . 4
β’ (π β (π β (πΎ Cn πΏ), π§ β βͺ πΎ β¦ (πβπ§)) β (((πΏ βko πΎ) Γt πΎ) Cn πΏ)) |
64 | 59, 63 | eqeltrd 2834 |
. . 3
β’ (π β (π β (πΎ Cn πΏ), π§ β π β¦ (πβπ§)) β (((πΏ βko πΎ) Γt πΎ) Cn πΏ)) |
65 | | fveq1 6845 |
. . . 4
β’ (π = ((π₯ β π β¦ (π¦ β π β¦ π΄))βπ€) β (πβπ§) = (((π₯ β π β¦ (π¦ β π β¦ π΄))βπ€)βπ§)) |
66 | | fveq2 6846 |
. . . 4
β’ (π§ = π β (((π₯ β π β¦ (π¦ β π β¦ π΄))βπ€)βπ§) = (((π₯ β π β¦ (π¦ β π β¦ π΄))βπ€)βπ)) |
67 | 65, 66 | sylan9eq 2793 |
. . 3
β’ ((π = ((π₯ β π β¦ (π¦ β π β¦ π΄))βπ€) β§ π§ = π) β (πβπ§) = (((π₯ β π β¦ (π¦ β π β¦ π΄))βπ€)βπ)) |
68 | 19, 39, 53, 54, 28, 39, 64, 67 | cnmpt22 23048 |
. 2
β’ (π β (π€ β π, π β π β¦ (((π₯ β π β¦ (π¦ β π β¦ π΄))βπ€)βπ)) β ((π½ Γt πΎ) Cn πΏ)) |
69 | 51, 68 | eqeltrrd 2835 |
1
β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((π½ Γt πΎ) Cn πΏ)) |