Step | Hyp | Ref
| Expression |
1 | | distop 22297 |
. . . 4
β’ (π΄ β π β π« π΄ β Top) |
2 | | simpl 483 |
. . . 4
β’ ((π
β Top β§ π΄ β π) β π
β Top) |
3 | | unipw 5405 |
. . . . . 6
β’ βͺ π« π΄ = π΄ |
4 | 3 | eqcomi 2746 |
. . . . 5
β’ π΄ = βͺ
π« π΄ |
5 | | eqid 2737 |
. . . . 5
β’ {π₯ β π« π΄ β£ (π« π΄ βΎt π₯) β Comp} = {π₯ β π« π΄ β£ (π« π΄ βΎt π₯) β Comp} |
6 | | eqid 2737 |
. . . . 5
β’ (π β {π₯ β π« π΄ β£ (π« π΄ βΎt π₯) β Comp}, π£ β π
β¦ {π β (π« π΄ Cn π
) β£ (π β π) β π£}) = (π β {π₯ β π« π΄ β£ (π« π΄ βΎt π₯) β Comp}, π£ β π
β¦ {π β (π« π΄ Cn π
) β£ (π β π) β π£}) |
7 | 4, 5, 6 | xkoval 22890 |
. . . 4
β’
((π« π΄ β
Top β§ π
β Top)
β (π
βko π« π΄) = (topGenβ(fiβran (π β {π₯ β π« π΄ β£ (π« π΄ βΎt π₯) β Comp}, π£ β π
β¦ {π β (π« π΄ Cn π
) β£ (π β π) β π£})))) |
8 | 1, 2, 7 | syl2an2 684 |
. . 3
β’ ((π
β Top β§ π΄ β π) β (π
βko π« π΄) = (topGenβ(fiβran
(π β {π₯ β π« π΄ β£ (π« π΄ βΎt π₯) β Comp}, π£ β π
β¦ {π β (π« π΄ Cn π
) β£ (π β π) β π£})))) |
9 | | simpr 485 |
. . . . 5
β’ ((π
β Top β§ π΄ β π) β π΄ β π) |
10 | | fconst6g 6728 |
. . . . . 6
β’ (π
β Top β (π΄ Γ {π
}):π΄βΆTop) |
11 | 10 | adantr 481 |
. . . . 5
β’ ((π
β Top β§ π΄ β π) β (π΄ Γ {π
}):π΄βΆTop) |
12 | | pttop 22885 |
. . . . 5
β’ ((π΄ β π β§ (π΄ Γ {π
}):π΄βΆTop) β
(βtβ(π΄ Γ {π
})) β Top) |
13 | 9, 11, 12 | syl2anc 584 |
. . . 4
β’ ((π
β Top β§ π΄ β π) β (βtβ(π΄ Γ {π
})) β Top) |
14 | | elpwi 4565 |
. . . . . . . . . . . . . 14
β’ (π₯ β π« π΄ β π₯ β π΄) |
15 | | restdis 22481 |
. . . . . . . . . . . . . 14
β’ ((π΄ β π β§ π₯ β π΄) β (π« π΄ βΎt π₯) = π« π₯) |
16 | 14, 15 | sylan2 593 |
. . . . . . . . . . . . 13
β’ ((π΄ β π β§ π₯ β π« π΄) β (π« π΄ βΎt π₯) = π« π₯) |
17 | 16 | adantll 712 |
. . . . . . . . . . . 12
β’ (((π
β Top β§ π΄ β π) β§ π₯ β π« π΄) β (π« π΄ βΎt π₯) = π« π₯) |
18 | 17 | eleq1d 2822 |
. . . . . . . . . . 11
β’ (((π
β Top β§ π΄ β π) β§ π₯ β π« π΄) β ((π« π΄ βΎt π₯) β Comp β π« π₯ β Comp)) |
19 | | discmp 22701 |
. . . . . . . . . . 11
β’ (π₯ β Fin β π«
π₯ β
Comp) |
20 | 18, 19 | bitr4di 288 |
. . . . . . . . . 10
β’ (((π
β Top β§ π΄ β π) β§ π₯ β π« π΄) β ((π« π΄ βΎt π₯) β Comp β π₯ β Fin)) |
21 | 20 | rabbidva 3412 |
. . . . . . . . 9
β’ ((π
β Top β§ π΄ β π) β {π₯ β π« π΄ β£ (π« π΄ βΎt π₯) β Comp} = {π₯ β π« π΄ β£ π₯ β Fin}) |
22 | | dfin5 3916 |
. . . . . . . . 9
β’
(π« π΄ β©
Fin) = {π₯ β π«
π΄ β£ π₯ β Fin} |
23 | 21, 22 | eqtr4di 2795 |
. . . . . . . 8
β’ ((π
β Top β§ π΄ β π) β {π₯ β π« π΄ β£ (π« π΄ βΎt π₯) β Comp} = (π« π΄ β© Fin)) |
24 | | eqidd 2738 |
. . . . . . . 8
β’ ((π
β Top β§ π΄ β π) β π
= π
) |
25 | | toptopon2 22219 |
. . . . . . . . . 10
β’ (π
β Top β π
β (TopOnββͺ π
)) |
26 | | cndis 22594 |
. . . . . . . . . . 11
β’ ((π΄ β π β§ π
β (TopOnββͺ π
))
β (π« π΄ Cn
π
) = (βͺ π
βm π΄)) |
27 | 26 | ancoms 459 |
. . . . . . . . . 10
β’ ((π
β (TopOnββͺ π
)
β§ π΄ β π) β (π« π΄ Cn π
) = (βͺ π
βm π΄)) |
28 | 25, 27 | sylanb 581 |
. . . . . . . . 9
β’ ((π
β Top β§ π΄ β π) β (π« π΄ Cn π
) = (βͺ π
βm π΄)) |
29 | 28 | rabeqdv 3420 |
. . . . . . . 8
β’ ((π
β Top β§ π΄ β π) β {π β (π« π΄ Cn π
) β£ (π β π) β π£} = {π β (βͺ π
βm π΄) β£ (π β π) β π£}) |
30 | 23, 24, 29 | mpoeq123dv 7426 |
. . . . . . 7
β’ ((π
β Top β§ π΄ β π) β (π β {π₯ β π« π΄ β£ (π« π΄ βΎt π₯) β Comp}, π£ β π
β¦ {π β (π« π΄ Cn π
) β£ (π β π) β π£}) = (π β (π« π΄ β© Fin), π£ β π
β¦ {π β (βͺ π
βm π΄) β£ (π β π) β π£})) |
31 | 30 | rneqd 5891 |
. . . . . 6
β’ ((π
β Top β§ π΄ β π) β ran (π β {π₯ β π« π΄ β£ (π« π΄ βΎt π₯) β Comp}, π£ β π
β¦ {π β (π« π΄ Cn π
) β£ (π β π) β π£}) = ran (π β (π« π΄ β© Fin), π£ β π
β¦ {π β (βͺ π
βm π΄) β£ (π β π) β π£})) |
32 | | eqid 2737 |
. . . . . . 7
β’ (π β (π« π΄ β© Fin), π£ β π
β¦ {π β (βͺ π
βm π΄) β£ (π β π) β π£}) = (π β (π« π΄ β© Fin), π£ β π
β¦ {π β (βͺ π
βm π΄) β£ (π β π) β π£}) |
33 | 32 | rnmpo 7483 |
. . . . . 6
β’ ran
(π β (π« π΄ β© Fin), π£ β π
β¦ {π β (βͺ π
βm π΄) β£ (π β π) β π£}) = {π₯ β£ βπ β (π« π΄ β© Fin)βπ£ β π
π₯ = {π β (βͺ π
βm π΄) β£ (π β π) β π£}} |
34 | 31, 33 | eqtrdi 2793 |
. . . . 5
β’ ((π
β Top β§ π΄ β π) β ran (π β {π₯ β π« π΄ β£ (π« π΄ βΎt π₯) β Comp}, π£ β π
β¦ {π β (π« π΄ Cn π
) β£ (π β π) β π£}) = {π₯ β£ βπ β (π« π΄ β© Fin)βπ£ β π
π₯ = {π β (βͺ π
βm π΄) β£ (π β π) β π£}}) |
35 | | elmapi 8745 |
. . . . . . . . . . . 12
β’ (π β (βͺ π
βm π΄)
β π:π΄βΆβͺ π
) |
36 | | eleq2 2826 |
. . . . . . . . . . . . . . . . 17
β’ (π£ = if(π₯ β π, π£, βͺ π
) β ((πβπ₯) β π£ β (πβπ₯) β if(π₯ β π, π£, βͺ π
))) |
37 | 36 | imbi2d 340 |
. . . . . . . . . . . . . . . 16
β’ (π£ = if(π₯ β π, π£, βͺ π
) β ((π₯ β π΄ β (πβπ₯) β π£) β (π₯ β π΄ β (πβπ₯) β if(π₯ β π, π£, βͺ π
)))) |
38 | 37 | bibi1d 343 |
. . . . . . . . . . . . . . 15
β’ (π£ = if(π₯ β π, π£, βͺ π
) β (((π₯ β π΄ β (πβπ₯) β π£) β (π₯ β π β (πβπ₯) β π£)) β ((π₯ β π΄ β (πβπ₯) β if(π₯ β π, π£, βͺ π
)) β (π₯ β π β (πβπ₯) β π£)))) |
39 | | eleq2 2826 |
. . . . . . . . . . . . . . . . 17
β’ (βͺ π
=
if(π₯ β π, π£, βͺ π
) β ((πβπ₯) β βͺ π
β (πβπ₯) β if(π₯ β π, π£, βͺ π
))) |
40 | 39 | imbi2d 340 |
. . . . . . . . . . . . . . . 16
β’ (βͺ π
=
if(π₯ β π, π£, βͺ π
) β ((π₯ β π΄ β (πβπ₯) β βͺ π
) β (π₯ β π΄ β (πβπ₯) β if(π₯ β π, π£, βͺ π
)))) |
41 | 40 | bibi1d 343 |
. . . . . . . . . . . . . . 15
β’ (βͺ π
=
if(π₯ β π, π£, βͺ π
) β (((π₯ β π΄ β (πβπ₯) β βͺ π
) β (π₯ β π β (πβπ₯) β π£)) β ((π₯ β π΄ β (πβπ₯) β if(π₯ β π, π£, βͺ π
)) β (π₯ β π β (πβπ₯) β π£)))) |
42 | | simprl 769 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β π β (π« π΄ β© Fin)) |
43 | 42 | elin1d 4156 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β π β π« π΄) |
44 | 43 | elpwid 4567 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β π β π΄) |
45 | 44 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π:π΄βΆβͺ π
) β π β π΄) |
46 | 45 | sselda 3942 |
. . . . . . . . . . . . . . . . 17
β’
(((((π
β Top
β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π:π΄βΆβͺ π
) β§ π₯ β π) β π₯ β π΄) |
47 | | simpr 485 |
. . . . . . . . . . . . . . . . 17
β’
(((((π
β Top
β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π:π΄βΆβͺ π
) β§ π₯ β π) β π₯ β π) |
48 | 46, 47 | 2thd 264 |
. . . . . . . . . . . . . . . 16
β’
(((((π
β Top
β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π:π΄βΆβͺ π
) β§ π₯ β π) β (π₯ β π΄ β π₯ β π)) |
49 | 48 | imbi1d 341 |
. . . . . . . . . . . . . . 15
β’
(((((π
β Top
β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π:π΄βΆβͺ π
) β§ π₯ β π) β ((π₯ β π΄ β (πβπ₯) β π£) β (π₯ β π β (πβπ₯) β π£))) |
50 | | ffvelcdm 7029 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π:π΄βΆβͺ π
β§ π₯ β π΄) β (πβπ₯) β βͺ π
) |
51 | 50 | ex 413 |
. . . . . . . . . . . . . . . . . 18
β’ (π:π΄βΆβͺ π
β (π₯ β π΄ β (πβπ₯) β βͺ π
)) |
52 | 51 | adantl 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π:π΄βΆβͺ π
) β (π₯ β π΄ β (πβπ₯) β βͺ π
)) |
53 | 52 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’
(((((π
β Top
β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π:π΄βΆβͺ π
) β§ Β¬ π₯ β π) β (π₯ β π΄ β (πβπ₯) β βͺ π
)) |
54 | | pm2.21 123 |
. . . . . . . . . . . . . . . . 17
β’ (Β¬
π₯ β π β (π₯ β π β (πβπ₯) β π£)) |
55 | 54 | adantl 482 |
. . . . . . . . . . . . . . . 16
β’
(((((π
β Top
β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π:π΄βΆβͺ π
) β§ Β¬ π₯ β π) β (π₯ β π β (πβπ₯) β π£)) |
56 | 53, 55 | 2thd 264 |
. . . . . . . . . . . . . . 15
β’
(((((π
β Top
β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π:π΄βΆβͺ π
) β§ Β¬ π₯ β π) β ((π₯ β π΄ β (πβπ₯) β βͺ π
) β (π₯ β π β (πβπ₯) β π£))) |
57 | 38, 41, 49, 56 | ifbothda 4522 |
. . . . . . . . . . . . . 14
β’ ((((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π:π΄βΆβͺ π
) β ((π₯ β π΄ β (πβπ₯) β if(π₯ β π, π£, βͺ π
)) β (π₯ β π β (πβπ₯) β π£))) |
58 | 57 | ralbidv2 3168 |
. . . . . . . . . . . . 13
β’ ((((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π:π΄βΆβͺ π
) β (βπ₯ β π΄ (πβπ₯) β if(π₯ β π, π£, βͺ π
) β βπ₯ β π (πβπ₯) β π£)) |
59 | | ffn 6665 |
. . . . . . . . . . . . . . 15
β’ (π:π΄βΆβͺ π
β π Fn π΄) |
60 | 59 | adantl 482 |
. . . . . . . . . . . . . 14
β’ ((((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π:π΄βΆβͺ π
) β π Fn π΄) |
61 | | vex 3447 |
. . . . . . . . . . . . . . . 16
β’ π β V |
62 | 61 | elixp 8800 |
. . . . . . . . . . . . . . 15
β’ (π β Xπ₯ β
π΄ if(π₯ β π, π£, βͺ π
) β (π Fn π΄ β§ βπ₯ β π΄ (πβπ₯) β if(π₯ β π, π£, βͺ π
))) |
63 | 62 | baib 536 |
. . . . . . . . . . . . . 14
β’ (π Fn π΄ β (π β Xπ₯ β π΄ if(π₯ β π, π£, βͺ π
) β βπ₯ β π΄ (πβπ₯) β if(π₯ β π, π£, βͺ π
))) |
64 | 60, 63 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π:π΄βΆβͺ π
) β (π β Xπ₯ β π΄ if(π₯ β π, π£, βͺ π
) β βπ₯ β π΄ (πβπ₯) β if(π₯ β π, π£, βͺ π
))) |
65 | | ffun 6668 |
. . . . . . . . . . . . . 14
β’ (π:π΄βΆβͺ π
β Fun π) |
66 | | fdm 6674 |
. . . . . . . . . . . . . . . 16
β’ (π:π΄βΆβͺ π
β dom π = π΄) |
67 | 66 | adantl 482 |
. . . . . . . . . . . . . . 15
β’ ((((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π:π΄βΆβͺ π
) β dom π = π΄) |
68 | 45, 67 | sseqtrrd 3983 |
. . . . . . . . . . . . . 14
β’ ((((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π:π΄βΆβͺ π
) β π β dom π) |
69 | | funimass4 6904 |
. . . . . . . . . . . . . 14
β’ ((Fun
π β§ π β dom π) β ((π β π) β π£ β βπ₯ β π (πβπ₯) β π£)) |
70 | 65, 68, 69 | syl2an2 684 |
. . . . . . . . . . . . 13
β’ ((((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π:π΄βΆβͺ π
) β ((π β π) β π£ β βπ₯ β π (πβπ₯) β π£)) |
71 | 58, 64, 70 | 3bitr4d 310 |
. . . . . . . . . . . 12
β’ ((((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π:π΄βΆβͺ π
) β (π β Xπ₯ β π΄ if(π₯ β π, π£, βͺ π
) β (π β π) β π£)) |
72 | 35, 71 | sylan2 593 |
. . . . . . . . . . 11
β’ ((((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π β (βͺ π
βm π΄)) β (π β Xπ₯ β π΄ if(π₯ β π, π£, βͺ π
) β (π β π) β π£)) |
73 | 72 | rabbi2dva 4175 |
. . . . . . . . . 10
β’ (((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β ((βͺ
π
βm π΄) β© Xπ₯ β
π΄ if(π₯ β π, π£, βͺ π
)) = {π β (βͺ π
βm π΄) β£ (π β π) β π£}) |
74 | | elssuni 4896 |
. . . . . . . . . . . . . . . 16
β’ (π£ β π
β π£ β βͺ π
) |
75 | 74 | ad2antll 727 |
. . . . . . . . . . . . . . 15
β’ (((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β π£ β βͺ π
) |
76 | | ssid 3964 |
. . . . . . . . . . . . . . 15
β’ βͺ π
β βͺ π
|
77 | | sseq1 3967 |
. . . . . . . . . . . . . . . 16
β’ (π£ = if(π₯ β π, π£, βͺ π
) β (π£ β βͺ π
β if(π₯ β π, π£, βͺ π
) β βͺ π
)) |
78 | | sseq1 3967 |
. . . . . . . . . . . . . . . 16
β’ (βͺ π
=
if(π₯ β π, π£, βͺ π
) β (βͺ π
β βͺ π
β if(π₯ β π, π£, βͺ π
) β βͺ π
)) |
79 | 77, 78 | ifboth 4523 |
. . . . . . . . . . . . . . 15
β’ ((π£ β βͺ π
β§ βͺ π
β βͺ π
) β if(π₯ β π, π£, βͺ π
) β βͺ π
) |
80 | 75, 76, 79 | sylancl 586 |
. . . . . . . . . . . . . 14
β’ (((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β if(π₯ β π, π£, βͺ π
) β βͺ π
) |
81 | 80 | ralrimivw 3145 |
. . . . . . . . . . . . 13
β’ (((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β βπ₯ β π΄ if(π₯ β π, π£, βͺ π
) β βͺ π
) |
82 | | ss2ixp 8806 |
. . . . . . . . . . . . 13
β’
(βπ₯ β
π΄ if(π₯ β π, π£, βͺ π
) β βͺ π
β Xπ₯ β π΄ if(π₯ β π, π£, βͺ π
) β Xπ₯ β
π΄ βͺ π
) |
83 | 81, 82 | syl 17 |
. . . . . . . . . . . 12
β’ (((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β Xπ₯ β π΄ if(π₯ β π, π£, βͺ π
) β Xπ₯ β
π΄ βͺ π
) |
84 | | simplr 767 |
. . . . . . . . . . . . 13
β’ (((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β π΄ β π) |
85 | | uniexg 7669 |
. . . . . . . . . . . . . 14
β’ (π
β Top β βͺ π
β V) |
86 | 85 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’ (((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β βͺ π
β V) |
87 | | ixpconstg 8802 |
. . . . . . . . . . . . 13
β’ ((π΄ β π β§ βͺ π
β V) β Xπ₯ β
π΄ βͺ π
=
(βͺ π
βm π΄)) |
88 | 84, 86, 87 | syl2anc 584 |
. . . . . . . . . . . 12
β’ (((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β Xπ₯ β π΄ βͺ π
= (βͺ
π
βm π΄)) |
89 | 83, 88 | sseqtrd 3982 |
. . . . . . . . . . 11
β’ (((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β Xπ₯ β π΄ if(π₯ β π, π£, βͺ π
) β (βͺ π
βm π΄)) |
90 | | sseqin2 4173 |
. . . . . . . . . . 11
β’ (Xπ₯ β
π΄ if(π₯ β π, π£, βͺ π
) β (βͺ π
βm π΄)
β ((βͺ π
βm π΄) β© Xπ₯ β π΄ if(π₯ β π, π£, βͺ π
)) = Xπ₯ β
π΄ if(π₯ β π, π£, βͺ π
)) |
91 | 89, 90 | sylib 217 |
. . . . . . . . . 10
β’ (((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β ((βͺ
π
βm π΄) β© Xπ₯ β
π΄ if(π₯ β π, π£, βͺ π
)) = Xπ₯ β
π΄ if(π₯ β π, π£, βͺ π
)) |
92 | 73, 91 | eqtr3d 2779 |
. . . . . . . . 9
β’ (((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β {π β (βͺ π
βm π΄) β£ (π β π) β π£} = Xπ₯ β π΄ if(π₯ β π, π£, βͺ π
)) |
93 | 10 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β (π΄ Γ {π
}):π΄βΆTop) |
94 | 42 | elin2d 4157 |
. . . . . . . . . 10
β’ (((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β π β Fin) |
95 | | simplrr 776 |
. . . . . . . . . . . 12
β’ ((((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π₯ β π΄) β π£ β π
) |
96 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’ βͺ π
=
βͺ π
|
97 | 96 | topopn 22207 |
. . . . . . . . . . . . 13
β’ (π
β Top β βͺ π
β π
) |
98 | 97 | ad3antrrr 728 |
. . . . . . . . . . . 12
β’ ((((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π₯ β π΄) β βͺ π
β π
) |
99 | 95, 98 | ifcld 4530 |
. . . . . . . . . . 11
β’ ((((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π₯ β π΄) β if(π₯ β π, π£, βͺ π
) β π
) |
100 | | fvconst2g 7147 |
. . . . . . . . . . . 12
β’ ((π
β Top β§ π₯ β π΄) β ((π΄ Γ {π
})βπ₯) = π
) |
101 | 100 | ad4ant14 750 |
. . . . . . . . . . 11
β’ ((((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π₯ β π΄) β ((π΄ Γ {π
})βπ₯) = π
) |
102 | 99, 101 | eleqtrrd 2841 |
. . . . . . . . . 10
β’ ((((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π₯ β π΄) β if(π₯ β π, π£, βͺ π
) β ((π΄ Γ {π
})βπ₯)) |
103 | | eldifn 4085 |
. . . . . . . . . . . . 13
β’ (π₯ β (π΄ β π) β Β¬ π₯ β π) |
104 | 103 | iffalsed 4495 |
. . . . . . . . . . . 12
β’ (π₯ β (π΄ β π) β if(π₯ β π, π£, βͺ π
) = βͺ
π
) |
105 | 104 | adantl 482 |
. . . . . . . . . . 11
β’ ((((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π₯ β (π΄ β π)) β if(π₯ β π, π£, βͺ π
) = βͺ
π
) |
106 | | eldifi 4084 |
. . . . . . . . . . . . 13
β’ (π₯ β (π΄ β π) β π₯ β π΄) |
107 | 106, 101 | sylan2 593 |
. . . . . . . . . . . 12
β’ ((((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π₯ β (π΄ β π)) β ((π΄ Γ {π
})βπ₯) = π
) |
108 | 107 | unieqd 4877 |
. . . . . . . . . . 11
β’ ((((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π₯ β (π΄ β π)) β βͺ
((π΄ Γ {π
})βπ₯) = βͺ π
) |
109 | 105, 108 | eqtr4d 2780 |
. . . . . . . . . 10
β’ ((((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β§ π₯ β (π΄ β π)) β if(π₯ β π, π£, βͺ π
) = βͺ
((π΄ Γ {π
})βπ₯)) |
110 | 84, 93, 94, 102, 109 | ptopn 22886 |
. . . . . . . . 9
β’ (((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β Xπ₯ β π΄ if(π₯ β π, π£, βͺ π
) β
(βtβ(π΄ Γ {π
}))) |
111 | 92, 110 | eqeltrd 2838 |
. . . . . . . 8
β’ (((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β {π β (βͺ π
βm π΄) β£ (π β π) β π£} β (βtβ(π΄ Γ {π
}))) |
112 | | eleq1 2825 |
. . . . . . . 8
β’ (π₯ = {π β (βͺ π
βm π΄) β£ (π β π) β π£} β (π₯ β (βtβ(π΄ Γ {π
})) β {π β (βͺ π
βm π΄) β£ (π β π) β π£} β (βtβ(π΄ Γ {π
})))) |
113 | 111, 112 | syl5ibrcom 246 |
. . . . . . 7
β’ (((π
β Top β§ π΄ β π) β§ (π β (π« π΄ β© Fin) β§ π£ β π
)) β (π₯ = {π β (βͺ π
βm π΄) β£ (π β π) β π£} β π₯ β (βtβ(π΄ Γ {π
})))) |
114 | 113 | rexlimdvva 3203 |
. . . . . 6
β’ ((π
β Top β§ π΄ β π) β (βπ β (π« π΄ β© Fin)βπ£ β π
π₯ = {π β (βͺ π
βm π΄) β£ (π β π) β π£} β π₯ β (βtβ(π΄ Γ {π
})))) |
115 | 114 | abssdv 4023 |
. . . . 5
β’ ((π
β Top β§ π΄ β π) β {π₯ β£ βπ β (π« π΄ β© Fin)βπ£ β π
π₯ = {π β (βͺ π
βm π΄) β£ (π β π) β π£}} β (βtβ(π΄ Γ {π
}))) |
116 | 34, 115 | eqsstrd 3980 |
. . . 4
β’ ((π
β Top β§ π΄ β π) β ran (π β {π₯ β π« π΄ β£ (π« π΄ βΎt π₯) β Comp}, π£ β π
β¦ {π β (π« π΄ Cn π
) β£ (π β π) β π£}) β (βtβ(π΄ Γ {π
}))) |
117 | | tgfiss 22293 |
. . . 4
β’
(((βtβ(π΄ Γ {π
})) β Top β§ ran (π β {π₯ β π« π΄ β£ (π« π΄ βΎt π₯) β Comp}, π£ β π
β¦ {π β (π« π΄ Cn π
) β£ (π β π) β π£}) β (βtβ(π΄ Γ {π
}))) β (topGenβ(fiβran
(π β {π₯ β π« π΄ β£ (π« π΄ βΎt π₯) β Comp}, π£ β π
β¦ {π β (π« π΄ Cn π
) β£ (π β π) β π£}))) β (βtβ(π΄ Γ {π
}))) |
118 | 13, 116, 117 | syl2anc 584 |
. . 3
β’ ((π
β Top β§ π΄ β π) β (topGenβ(fiβran (π β {π₯ β π« π΄ β£ (π« π΄ βΎt π₯) β Comp}, π£ β π
β¦ {π β (π« π΄ Cn π
) β£ (π β π) β π£}))) β (βtβ(π΄ Γ {π
}))) |
119 | 8, 118 | eqsstrd 3980 |
. 2
β’ ((π
β Top β§ π΄ β π) β (π
βko π« π΄) β
(βtβ(π΄ Γ {π
}))) |
120 | | eqid 2737 |
. . . . . . . 8
β’
(βtβ(π΄ Γ {π
})) = (βtβ(π΄ Γ {π
})) |
121 | 120, 96 | ptuniconst 22901 |
. . . . . . 7
β’ ((π΄ β π β§ π
β Top) β (βͺ π
βm π΄) =
βͺ (βtβ(π΄ Γ {π
}))) |
122 | 121 | ancoms 459 |
. . . . . 6
β’ ((π
β Top β§ π΄ β π) β (βͺ π
βm π΄) = βͺ
(βtβ(π΄ Γ {π
}))) |
123 | 28, 122 | eqtrd 2777 |
. . . . 5
β’ ((π
β Top β§ π΄ β π) β (π« π΄ Cn π
) = βͺ
(βtβ(π΄ Γ {π
}))) |
124 | 123 | oveq2d 7367 |
. . . 4
β’ ((π
β Top β§ π΄ β π) β ((βtβ(π΄ Γ {π
})) βΎt (π« π΄ Cn π
)) = ((βtβ(π΄ Γ {π
})) βΎt βͺ (βtβ(π΄ Γ {π
})))) |
125 | | eqid 2737 |
. . . . . 6
β’ βͺ (βtβ(π΄ Γ {π
})) = βͺ
(βtβ(π΄ Γ {π
})) |
126 | 125 | restid 17275 |
. . . . 5
β’
((βtβ(π΄ Γ {π
})) β Top β
((βtβ(π΄ Γ {π
})) βΎt βͺ (βtβ(π΄ Γ {π
}))) = (βtβ(π΄ Γ {π
}))) |
127 | 13, 126 | syl 17 |
. . . 4
β’ ((π
β Top β§ π΄ β π) β ((βtβ(π΄ Γ {π
})) βΎt βͺ (βtβ(π΄ Γ {π
}))) = (βtβ(π΄ Γ {π
}))) |
128 | 124, 127 | eqtrd 2777 |
. . 3
β’ ((π
β Top β§ π΄ β π) β ((βtβ(π΄ Γ {π
})) βΎt (π« π΄ Cn π
)) = (βtβ(π΄ Γ {π
}))) |
129 | 4, 120 | xkoptsub 22957 |
. . . 4
β’
((π« π΄ β
Top β§ π
β Top)
β ((βtβ(π΄ Γ {π
})) βΎt (π« π΄ Cn π
)) β (π
βko π« π΄)) |
130 | 1, 2, 129 | syl2an2 684 |
. . 3
β’ ((π
β Top β§ π΄ β π) β ((βtβ(π΄ Γ {π
})) βΎt (π« π΄ Cn π
)) β (π
βko π« π΄)) |
131 | 128, 130 | eqsstrrd 3981 |
. 2
β’ ((π
β Top β§ π΄ β π) β (βtβ(π΄ Γ {π
})) β (π
βko π« π΄)) |
132 | 119, 131 | eqssd 3959 |
1
β’ ((π
β Top β§ π΄ β π) β (π
βko π« π΄) =
(βtβ(π΄ Γ {π
}))) |