Step | Hyp | Ref
| Expression |
1 | | fncld 22376 |
. . . . 5
β’ Clsd Fn
Top |
2 | | fnfun 6603 |
. . . . 5
β’ (Clsd Fn
Top β Fun Clsd) |
3 | 1, 2 | ax-mp 5 |
. . . 4
β’ Fun
Clsd |
4 | | fvelima 6909 |
. . . 4
β’ ((Fun
Clsd β§ πΎ β (Clsd
β (TopOnβπ΅)))
β βπ β
(TopOnβπ΅)(Clsdβπ) = πΎ) |
5 | 3, 4 | mpan 689 |
. . 3
β’ (πΎ β (Clsd β
(TopOnβπ΅)) β
βπ β
(TopOnβπ΅)(Clsdβπ) = πΎ) |
6 | | cldmreon 22448 |
. . . . . 6
β’ (π β (TopOnβπ΅) β (Clsdβπ) β (Mooreβπ΅)) |
7 | | topontop 22265 |
. . . . . . 7
β’ (π β (TopOnβπ΅) β π β Top) |
8 | | 0cld 22392 |
. . . . . . 7
β’ (π β Top β β
β (Clsdβπ)) |
9 | 7, 8 | syl 17 |
. . . . . 6
β’ (π β (TopOnβπ΅) β β
β
(Clsdβπ)) |
10 | | uncld 22395 |
. . . . . . . 8
β’ ((π₯ β (Clsdβπ) β§ π¦ β (Clsdβπ)) β (π₯ βͺ π¦) β (Clsdβπ)) |
11 | 10 | adantl 483 |
. . . . . . 7
β’ ((π β (TopOnβπ΅) β§ (π₯ β (Clsdβπ) β§ π¦ β (Clsdβπ))) β (π₯ βͺ π¦) β (Clsdβπ)) |
12 | 11 | ralrimivva 3198 |
. . . . . 6
β’ (π β (TopOnβπ΅) β βπ₯ β (Clsdβπ)βπ¦ β (Clsdβπ)(π₯ βͺ π¦) β (Clsdβπ)) |
13 | 6, 9, 12 | 3jca 1129 |
. . . . 5
β’ (π β (TopOnβπ΅) β ((Clsdβπ) β (Mooreβπ΅) β§ β
β
(Clsdβπ) β§
βπ₯ β
(Clsdβπ)βπ¦ β (Clsdβπ)(π₯ βͺ π¦) β (Clsdβπ))) |
14 | | eleq1 2826 |
. . . . . 6
β’
((Clsdβπ) =
πΎ β ((Clsdβπ) β (Mooreβπ΅) β πΎ β (Mooreβπ΅))) |
15 | | eleq2 2827 |
. . . . . 6
β’
((Clsdβπ) =
πΎ β (β
β
(Clsdβπ) β
β
β πΎ)) |
16 | | eleq2 2827 |
. . . . . . . 8
β’
((Clsdβπ) =
πΎ β ((π₯ βͺ π¦) β (Clsdβπ) β (π₯ βͺ π¦) β πΎ)) |
17 | 16 | raleqbi1dv 3308 |
. . . . . . 7
β’
((Clsdβπ) =
πΎ β (βπ¦ β (Clsdβπ)(π₯ βͺ π¦) β (Clsdβπ) β βπ¦ β πΎ (π₯ βͺ π¦) β πΎ)) |
18 | 17 | raleqbi1dv 3308 |
. . . . . 6
β’
((Clsdβπ) =
πΎ β (βπ₯ β (Clsdβπ)βπ¦ β (Clsdβπ)(π₯ βͺ π¦) β (Clsdβπ) β βπ₯ β πΎ βπ¦ β πΎ (π₯ βͺ π¦) β πΎ)) |
19 | 14, 15, 18 | 3anbi123d 1437 |
. . . . 5
β’
((Clsdβπ) =
πΎ β
(((Clsdβπ) β
(Mooreβπ΅) β§
β
β (Clsdβπ) β§ βπ₯ β (Clsdβπ)βπ¦ β (Clsdβπ)(π₯ βͺ π¦) β (Clsdβπ)) β (πΎ β (Mooreβπ΅) β§ β
β πΎ β§ βπ₯ β πΎ βπ¦ β πΎ (π₯ βͺ π¦) β πΎ))) |
20 | 13, 19 | syl5ibcom 244 |
. . . 4
β’ (π β (TopOnβπ΅) β ((Clsdβπ) = πΎ β (πΎ β (Mooreβπ΅) β§ β
β πΎ β§ βπ₯ β πΎ βπ¦ β πΎ (π₯ βͺ π¦) β πΎ))) |
21 | 20 | rexlimiv 3146 |
. . 3
β’
(βπ β
(TopOnβπ΅)(Clsdβπ) = πΎ β (πΎ β (Mooreβπ΅) β§ β
β πΎ β§ βπ₯ β πΎ βπ¦ β πΎ (π₯ βͺ π¦) β πΎ)) |
22 | 5, 21 | syl 17 |
. 2
β’ (πΎ β (Clsd β
(TopOnβπ΅)) β
(πΎ β
(Mooreβπ΅) β§
β
β πΎ β§
βπ₯ β πΎ βπ¦ β πΎ (π₯ βͺ π¦) β πΎ)) |
23 | | simp1 1137 |
. . . . 5
β’ ((πΎ β (Mooreβπ΅) β§ β
β πΎ β§ βπ₯ β πΎ βπ¦ β πΎ (π₯ βͺ π¦) β πΎ) β πΎ β (Mooreβπ΅)) |
24 | | simp2 1138 |
. . . . 5
β’ ((πΎ β (Mooreβπ΅) β§ β
β πΎ β§ βπ₯ β πΎ βπ¦ β πΎ (π₯ βͺ π¦) β πΎ) β β
β πΎ) |
25 | | uneq1 4117 |
. . . . . . . . . 10
β’ (π₯ = π β (π₯ βͺ π¦) = (π βͺ π¦)) |
26 | 25 | eleq1d 2823 |
. . . . . . . . 9
β’ (π₯ = π β ((π₯ βͺ π¦) β πΎ β (π βͺ π¦) β πΎ)) |
27 | | uneq2 4118 |
. . . . . . . . . 10
β’ (π¦ = π β (π βͺ π¦) = (π βͺ π)) |
28 | 27 | eleq1d 2823 |
. . . . . . . . 9
β’ (π¦ = π β ((π βͺ π¦) β πΎ β (π βͺ π) β πΎ)) |
29 | 26, 28 | rspc2v 3591 |
. . . . . . . 8
β’ ((π β πΎ β§ π β πΎ) β (βπ₯ β πΎ βπ¦ β πΎ (π₯ βͺ π¦) β πΎ β (π βͺ π) β πΎ)) |
30 | 29 | com12 32 |
. . . . . . 7
β’
(βπ₯ β
πΎ βπ¦ β πΎ (π₯ βͺ π¦) β πΎ β ((π β πΎ β§ π β πΎ) β (π βͺ π) β πΎ)) |
31 | 30 | 3ad2ant3 1136 |
. . . . . 6
β’ ((πΎ β (Mooreβπ΅) β§ β
β πΎ β§ βπ₯ β πΎ βπ¦ β πΎ (π₯ βͺ π¦) β πΎ) β ((π β πΎ β§ π β πΎ) β (π βͺ π) β πΎ)) |
32 | 31 | 3impib 1117 |
. . . . 5
β’ (((πΎ β (Mooreβπ΅) β§ β
β πΎ β§ βπ₯ β πΎ βπ¦ β πΎ (π₯ βͺ π¦) β πΎ) β§ π β πΎ β§ π β πΎ) β (π βͺ π) β πΎ) |
33 | | eqid 2737 |
. . . . 5
β’ {π β π« π΅ β£ (π΅ β π) β πΎ} = {π β π« π΅ β£ (π΅ β π) β πΎ} |
34 | 23, 24, 32, 33 | mretopd 22446 |
. . . 4
β’ ((πΎ β (Mooreβπ΅) β§ β
β πΎ β§ βπ₯ β πΎ βπ¦ β πΎ (π₯ βͺ π¦) β πΎ) β ({π β π« π΅ β£ (π΅ β π) β πΎ} β (TopOnβπ΅) β§ πΎ = (Clsdβ{π β π« π΅ β£ (π΅ β π) β πΎ}))) |
35 | 34 | simprd 497 |
. . 3
β’ ((πΎ β (Mooreβπ΅) β§ β
β πΎ β§ βπ₯ β πΎ βπ¦ β πΎ (π₯ βͺ π¦) β πΎ) β πΎ = (Clsdβ{π β π« π΅ β£ (π΅ β π) β πΎ})) |
36 | 34 | simpld 496 |
. . . 4
β’ ((πΎ β (Mooreβπ΅) β§ β
β πΎ β§ βπ₯ β πΎ βπ¦ β πΎ (π₯ βͺ π¦) β πΎ) β {π β π« π΅ β£ (π΅ β π) β πΎ} β (TopOnβπ΅)) |
37 | 7 | ssriv 3949 |
. . . . . 6
β’
(TopOnβπ΅)
β Top |
38 | 1 | fndmi 6607 |
. . . . . 6
β’ dom Clsd
= Top |
39 | 37, 38 | sseqtrri 3982 |
. . . . 5
β’
(TopOnβπ΅)
β dom Clsd |
40 | | funfvima2 7182 |
. . . . 5
β’ ((Fun
Clsd β§ (TopOnβπ΅)
β dom Clsd) β ({π β π« π΅ β£ (π΅ β π) β πΎ} β (TopOnβπ΅) β (Clsdβ{π β π« π΅ β£ (π΅ β π) β πΎ}) β (Clsd β (TopOnβπ΅)))) |
41 | 3, 39, 40 | mp2an 691 |
. . . 4
β’ ({π β π« π΅ β£ (π΅ β π) β πΎ} β (TopOnβπ΅) β (Clsdβ{π β π« π΅ β£ (π΅ β π) β πΎ}) β (Clsd β (TopOnβπ΅))) |
42 | 36, 41 | syl 17 |
. . 3
β’ ((πΎ β (Mooreβπ΅) β§ β
β πΎ β§ βπ₯ β πΎ βπ¦ β πΎ (π₯ βͺ π¦) β πΎ) β (Clsdβ{π β π« π΅ β£ (π΅ β π) β πΎ}) β (Clsd β (TopOnβπ΅))) |
43 | 35, 42 | eqeltrd 2838 |
. 2
β’ ((πΎ β (Mooreβπ΅) β§ β
β πΎ β§ βπ₯ β πΎ βπ¦ β πΎ (π₯ βͺ π¦) β πΎ) β πΎ β (Clsd β (TopOnβπ΅))) |
44 | 22, 43 | impbii 208 |
1
β’ (πΎ β (Clsd β
(TopOnβπ΅)) β
(πΎ β
(Mooreβπ΅) β§
β
β πΎ β§
βπ₯ β πΎ βπ¦ β πΎ (π₯ βͺ π¦) β πΎ)) |