Step | Hyp | Ref
| Expression |
1 | | ptcnp.3 |
. . . . . . . . 9
β’ (π β π½ β (TopOnβπ)) |
2 | 1 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β πΌ) β π½ β (TopOnβπ)) |
3 | | ptcnp.5 |
. . . . . . . . . 10
β’ (π β πΉ:πΌβΆTop) |
4 | 3 | ffvelcdmda 7036 |
. . . . . . . . 9
β’ ((π β§ π β πΌ) β (πΉβπ) β Top) |
5 | | toptopon2 22283 |
. . . . . . . . 9
β’ ((πΉβπ) β Top β (πΉβπ) β (TopOnββͺ (πΉβπ))) |
6 | 4, 5 | sylib 217 |
. . . . . . . 8
β’ ((π β§ π β πΌ) β (πΉβπ) β (TopOnββͺ (πΉβπ))) |
7 | | ptcnp.7 |
. . . . . . . 8
β’ ((π β§ π β πΌ) β (π₯ β π β¦ π΄) β ((π½ CnP (πΉβπ))βπ·)) |
8 | | cnpf2 22617 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ (πΉβπ) β (TopOnββͺ (πΉβπ)) β§ (π₯ β π β¦ π΄) β ((π½ CnP (πΉβπ))βπ·)) β (π₯ β π β¦ π΄):πβΆβͺ (πΉβπ)) |
9 | 2, 6, 7, 8 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ π β πΌ) β (π₯ β π β¦ π΄):πβΆβͺ (πΉβπ)) |
10 | 9 | fvmptelcdm 7062 |
. . . . . 6
β’ (((π β§ π β πΌ) β§ π₯ β π) β π΄ β βͺ (πΉβπ)) |
11 | 10 | an32s 651 |
. . . . 5
β’ (((π β§ π₯ β π) β§ π β πΌ) β π΄ β βͺ (πΉβπ)) |
12 | 11 | ralrimiva 3140 |
. . . 4
β’ ((π β§ π₯ β π) β βπ β πΌ π΄ β βͺ (πΉβπ)) |
13 | | ptcnp.4 |
. . . . . 6
β’ (π β πΌ β π) |
14 | 13 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π) β πΌ β π) |
15 | | mptelixpg 8876 |
. . . . 5
β’ (πΌ β π β ((π β πΌ β¦ π΄) β Xπ β πΌ βͺ (πΉβπ) β βπ β πΌ π΄ β βͺ (πΉβπ))) |
16 | 14, 15 | syl 17 |
. . . 4
β’ ((π β§ π₯ β π) β ((π β πΌ β¦ π΄) β Xπ β πΌ βͺ (πΉβπ) β βπ β πΌ π΄ β βͺ (πΉβπ))) |
17 | 12, 16 | mpbird 257 |
. . 3
β’ ((π β§ π₯ β π) β (π β πΌ β¦ π΄) β Xπ β πΌ βͺ (πΉβπ)) |
18 | 17 | fmpttd 7064 |
. 2
β’ (π β (π₯ β π β¦ (π β πΌ β¦ π΄)):πβΆXπ β πΌ βͺ (πΉβπ)) |
19 | | df-3an 1090 |
. . . . . . . 8
β’ ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ) β§ βπ€ β Fin βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ)) β§ βπ€ β Fin βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ))) |
20 | | ptcnp.2 |
. . . . . . . . . . . . 13
β’ πΎ =
(βtβπΉ) |
21 | | ptcnp.6 |
. . . . . . . . . . . . 13
β’ (π β π· β π) |
22 | | nfv 1918 |
. . . . . . . . . . . . . 14
β’
β²π(π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ)) |
23 | | nfv 1918 |
. . . . . . . . . . . . . . 15
β’
β²π(π€ β Fin β§ βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) |
24 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . 18
β’
β²ππ |
25 | | nfmpt1 5214 |
. . . . . . . . . . . . . . . . . 18
β’
β²π(π β πΌ β¦ π΄) |
26 | 24, 25 | nfmpt 5213 |
. . . . . . . . . . . . . . . . 17
β’
β²π(π₯ β π β¦ (π β πΌ β¦ π΄)) |
27 | | nfcv 2904 |
. . . . . . . . . . . . . . . . 17
β’
β²ππ· |
28 | 26, 27 | nffv 6853 |
. . . . . . . . . . . . . . . 16
β’
β²π((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) |
29 | 28 | nfel1 2920 |
. . . . . . . . . . . . . . 15
β’
β²π((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β Xπ β πΌ (πβπ) |
30 | 23, 29 | nfan 1903 |
. . . . . . . . . . . . . 14
β’
β²π((π€ β Fin β§ βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β Xπ β πΌ (πβπ)) |
31 | 22, 30 | nfan 1903 |
. . . . . . . . . . . . 13
β’
β²π((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ)) β§ ((π€ β Fin β§ βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β Xπ β πΌ (πβπ))) |
32 | | simprll 778 |
. . . . . . . . . . . . 13
β’ ((π β§ ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ)) β§ ((π€ β Fin β§ βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β Xπ β πΌ (πβπ)))) β π Fn πΌ) |
33 | | simprlr 779 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ)) β§ ((π€ β Fin β§ βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β Xπ β πΌ (πβπ)))) β βπ β πΌ (πβπ) β (πΉβπ)) |
34 | | fveq2 6843 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (πβπ) = (πβπ)) |
35 | | fveq2 6843 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (πΉβπ) = (πΉβπ)) |
36 | 34, 35 | eleq12d 2828 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((πβπ) β (πΉβπ) β (πβπ) β (πΉβπ))) |
37 | 36 | rspccva 3579 |
. . . . . . . . . . . . . 14
β’
((βπ β
πΌ (πβπ) β (πΉβπ) β§ π β πΌ) β (πβπ) β (πΉβπ)) |
38 | 33, 37 | sylan 581 |
. . . . . . . . . . . . 13
β’ (((π β§ ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ)) β§ ((π€ β Fin β§ βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β Xπ β πΌ (πβπ)))) β§ π β πΌ) β (πβπ) β (πΉβπ)) |
39 | | simprrl 780 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ)) β§ ((π€ β Fin β§ βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β Xπ β πΌ (πβπ)))) β (π€ β Fin β§ βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ))) |
40 | 39 | simpld 496 |
. . . . . . . . . . . . 13
β’ ((π β§ ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ)) β§ ((π€ β Fin β§ βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β Xπ β πΌ (πβπ)))) β π€ β Fin) |
41 | 39 | simprd 497 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ)) β§ ((π€ β Fin β§ βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β Xπ β πΌ (πβπ)))) β βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) |
42 | 35 | unieqd 4880 |
. . . . . . . . . . . . . . . 16
β’ (π = π β βͺ (πΉβπ) = βͺ (πΉβπ)) |
43 | 34, 42 | eqeq12d 2749 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((πβπ) = βͺ (πΉβπ) β (πβπ) = βͺ (πΉβπ))) |
44 | 43 | rspccva 3579 |
. . . . . . . . . . . . . 14
β’
((βπ β
(πΌ β π€)(πβπ) = βͺ (πΉβπ) β§ π β (πΌ β π€)) β (πβπ) = βͺ (πΉβπ)) |
45 | 41, 44 | sylan 581 |
. . . . . . . . . . . . 13
β’ (((π β§ ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ)) β§ ((π€ β Fin β§ βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β Xπ β πΌ (πβπ)))) β§ π β (πΌ β π€)) β (πβπ) = βͺ (πΉβπ)) |
46 | | simprrr 781 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ)) β§ ((π€ β Fin β§ βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β Xπ β πΌ (πβπ)))) β ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β Xπ β πΌ (πβπ)) |
47 | 34 | cbvixpv 8856 |
. . . . . . . . . . . . . 14
β’ Xπ β
πΌ (πβπ) = Xπ β πΌ (πβπ) |
48 | 46, 47 | eleqtrdi 2844 |
. . . . . . . . . . . . 13
β’ ((π β§ ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ)) β§ ((π€ β Fin β§ βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β Xπ β πΌ (πβπ)))) β ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β Xπ β πΌ (πβπ)) |
49 | 20, 1, 13, 3, 21, 7, 31, 32, 38, 40, 45, 48 | ptcnplem 22988 |
. . . . . . . . . . . 12
β’ ((π β§ ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ)) β§ ((π€ β Fin β§ βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β Xπ β πΌ (πβπ)))) β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β Xπ β πΌ (πβπ))) |
50 | 49 | anassrs 469 |
. . . . . . . . . . 11
β’ (((π β§ (π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ))) β§ ((π€ β Fin β§ βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β Xπ β πΌ (πβπ))) β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β Xπ β πΌ (πβπ))) |
51 | 50 | expr 458 |
. . . . . . . . . 10
β’ (((π β§ (π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ))) β§ (π€ β Fin β§ βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ))) β (((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β Xπ β πΌ (πβπ) β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β Xπ β πΌ (πβπ)))) |
52 | 51 | rexlimdvaa 3150 |
. . . . . . . . 9
β’ ((π β§ (π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ))) β (βπ€ β Fin βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ) β (((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β Xπ β πΌ (πβπ) β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β Xπ β πΌ (πβπ))))) |
53 | 52 | impr 456 |
. . . . . . . 8
β’ ((π β§ ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ)) β§ βπ€ β Fin βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ))) β (((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β Xπ β πΌ (πβπ) β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β Xπ β πΌ (πβπ)))) |
54 | 19, 53 | sylan2b 595 |
. . . . . . 7
β’ ((π β§ (π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ) β§ βπ€ β Fin βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ))) β (((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β Xπ β πΌ (πβπ) β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β Xπ β πΌ (πβπ)))) |
55 | | eleq2 2823 |
. . . . . . . 8
β’ (π = Xπ β πΌ (πβπ) β (((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β π β ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β Xπ β πΌ (πβπ))) |
56 | 47 | eqeq2i 2746 |
. . . . . . . . . . . 12
β’ (π = Xπ β πΌ (πβπ) β π = Xπ β πΌ (πβπ)) |
57 | 56 | biimpi 215 |
. . . . . . . . . . 11
β’ (π = Xπ β πΌ (πβπ) β π = Xπ β πΌ (πβπ)) |
58 | 57 | sseq2d 3977 |
. . . . . . . . . 10
β’ (π = Xπ β πΌ (πβπ) β (((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β π β ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β Xπ β πΌ (πβπ))) |
59 | 58 | anbi2d 630 |
. . . . . . . . 9
β’ (π = Xπ β πΌ (πβπ) β ((π· β π§ β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β π) β (π· β π§ β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β Xπ β πΌ (πβπ)))) |
60 | 59 | rexbidv 3172 |
. . . . . . . 8
β’ (π = Xπ β πΌ (πβπ) β (βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β π) β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β Xπ β πΌ (πβπ)))) |
61 | 55, 60 | imbi12d 345 |
. . . . . . 7
β’ (π = Xπ β πΌ (πβπ) β ((((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β π β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β π)) β (((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β Xπ β πΌ (πβπ) β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β Xπ β πΌ (πβπ))))) |
62 | 54, 61 | syl5ibrcom 247 |
. . . . . 6
β’ ((π β§ (π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ) β§ βπ€ β Fin βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ))) β (π = Xπ β πΌ (πβπ) β (((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β π β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β π)))) |
63 | 62 | expimpd 455 |
. . . . 5
β’ (π β (((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ) β§ βπ€ β Fin βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ π = Xπ β πΌ (πβπ)) β (((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β π β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β π)))) |
64 | 63 | exlimdv 1937 |
. . . 4
β’ (π β (βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ) β§ βπ€ β Fin βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ π = Xπ β πΌ (πβπ)) β (((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β π β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β π)))) |
65 | 64 | alrimiv 1931 |
. . 3
β’ (π β βπ(βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ) β§ βπ€ β Fin βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ π = Xπ β πΌ (πβπ)) β (((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β π β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β π)))) |
66 | | eqeq1 2737 |
. . . . . 6
β’ (π = π β (π = Xπ β πΌ (πβπ) β π = Xπ β πΌ (πβπ))) |
67 | 66 | anbi2d 630 |
. . . . 5
β’ (π = π β (((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ) β§ βπ€ β Fin βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ π = Xπ β πΌ (πβπ)) β ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ) β§ βπ€ β Fin βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ π = Xπ β πΌ (πβπ)))) |
68 | 67 | exbidv 1925 |
. . . 4
β’ (π = π β (βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ) β§ βπ€ β Fin βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ π = Xπ β πΌ (πβπ)) β βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ) β§ βπ€ β Fin βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ π = Xπ β πΌ (πβπ)))) |
69 | 68 | ralab 3650 |
. . 3
β’
(βπ β
{π β£ βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ) β§ βπ€ β Fin βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ π = Xπ β πΌ (πβπ))} (((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β π β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β π)) β βπ(βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ) β§ βπ€ β Fin βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ π = Xπ β πΌ (πβπ)) β (((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β π β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β π)))) |
70 | 65, 69 | sylibr 233 |
. 2
β’ (π β βπ β {π β£ βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ) β§ βπ€ β Fin βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ π = Xπ β πΌ (πβπ))} (((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β π β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β π))) |
71 | 3 | ffnd 6670 |
. . . . 5
β’ (π β πΉ Fn πΌ) |
72 | | eqid 2733 |
. . . . . 6
β’ {π β£ βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ) β§ βπ€ β Fin βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ π = Xπ β πΌ (πβπ))} = {π β£ βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ) β§ βπ€ β Fin βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ π = Xπ β πΌ (πβπ))} |
73 | 72 | ptval 22937 |
. . . . 5
β’ ((πΌ β π β§ πΉ Fn πΌ) β (βtβπΉ) = (topGenβ{π β£ βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ) β§ βπ€ β Fin βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ π = Xπ β πΌ (πβπ))})) |
74 | 13, 71, 73 | syl2anc 585 |
. . . 4
β’ (π β
(βtβπΉ) = (topGenβ{π β£ βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ) β§ βπ€ β Fin βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ π = Xπ β πΌ (πβπ))})) |
75 | 20, 74 | eqtrid 2785 |
. . 3
β’ (π β πΎ = (topGenβ{π β£ βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ) β§ βπ€ β Fin βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ π = Xπ β πΌ (πβπ))})) |
76 | 3 | feqmptd 6911 |
. . . . . 6
β’ (π β πΉ = (π β πΌ β¦ (πΉβπ))) |
77 | 76 | fveq2d 6847 |
. . . . 5
β’ (π β
(βtβπΉ) = (βtβ(π β πΌ β¦ (πΉβπ)))) |
78 | 20, 77 | eqtrid 2785 |
. . . 4
β’ (π β πΎ = (βtβ(π β πΌ β¦ (πΉβπ)))) |
79 | 6 | ralrimiva 3140 |
. . . . 5
β’ (π β βπ β πΌ (πΉβπ) β (TopOnββͺ (πΉβπ))) |
80 | | eqid 2733 |
. . . . . 6
β’
(βtβ(π β πΌ β¦ (πΉβπ))) = (βtβ(π β πΌ β¦ (πΉβπ))) |
81 | 80 | pttopon 22963 |
. . . . 5
β’ ((πΌ β π β§ βπ β πΌ (πΉβπ) β (TopOnββͺ (πΉβπ))) β (βtβ(π β πΌ β¦ (πΉβπ))) β (TopOnβXπ β
πΌ βͺ (πΉβπ))) |
82 | 13, 79, 81 | syl2anc 585 |
. . . 4
β’ (π β
(βtβ(π β πΌ β¦ (πΉβπ))) β (TopOnβXπ β
πΌ βͺ (πΉβπ))) |
83 | 78, 82 | eqeltrd 2834 |
. . 3
β’ (π β πΎ β (TopOnβXπ β
πΌ βͺ (πΉβπ))) |
84 | 1, 75, 83, 21 | tgcnp 22620 |
. 2
β’ (π β ((π₯ β π β¦ (π β πΌ β¦ π΄)) β ((π½ CnP πΎ)βπ·) β ((π₯ β π β¦ (π β πΌ β¦ π΄)):πβΆXπ β πΌ βͺ (πΉβπ) β§ βπ β {π β£ βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β (πΉβπ) β§ βπ€ β Fin βπ β (πΌ β π€)(πβπ) = βͺ (πΉβπ)) β§ π = Xπ β πΌ (πβπ))} (((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β π β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β π))))) |
85 | 18, 70, 84 | mpbir2and 712 |
1
β’ (π β (π₯ β π β¦ (π β πΌ β¦ π΄)) β ((π½ CnP πΎ)βπ·)) |