Step | Hyp | Ref
| Expression |
1 | | istopclsd.j |
. . . 4
β’ π½ = {π§ β π« π΅ β£ (πΉβ(π΅ β π§)) = (π΅ β π§)} |
2 | | istopclsd.f |
. . . . . . . . 9
β’ (π β πΉ:π« π΅βΆπ« π΅) |
3 | 2 | ffnd 6716 |
. . . . . . . 8
β’ (π β πΉ Fn π« π΅) |
4 | 3 | adantr 482 |
. . . . . . 7
β’ ((π β§ π§ β π« π΅) β πΉ Fn π« π΅) |
5 | | difss 4131 |
. . . . . . . . 9
β’ (π΅ β π§) β π΅ |
6 | | istopclsd.b |
. . . . . . . . . 10
β’ (π β π΅ β π) |
7 | | elpw2g 5344 |
. . . . . . . . . 10
β’ (π΅ β π β ((π΅ β π§) β π« π΅ β (π΅ β π§) β π΅)) |
8 | 6, 7 | syl 17 |
. . . . . . . . 9
β’ (π β ((π΅ β π§) β π« π΅ β (π΅ β π§) β π΅)) |
9 | 5, 8 | mpbiri 258 |
. . . . . . . 8
β’ (π β (π΅ β π§) β π« π΅) |
10 | 9 | adantr 482 |
. . . . . . 7
β’ ((π β§ π§ β π« π΅) β (π΅ β π§) β π« π΅) |
11 | | fnelfp 7170 |
. . . . . . 7
β’ ((πΉ Fn π« π΅ β§ (π΅ β π§) β π« π΅) β ((π΅ β π§) β dom (πΉ β© I ) β (πΉβ(π΅ β π§)) = (π΅ β π§))) |
12 | 4, 10, 11 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π§ β π« π΅) β ((π΅ β π§) β dom (πΉ β© I ) β (πΉβ(π΅ β π§)) = (π΅ β π§))) |
13 | 12 | bicomd 222 |
. . . . 5
β’ ((π β§ π§ β π« π΅) β ((πΉβ(π΅ β π§)) = (π΅ β π§) β (π΅ β π§) β dom (πΉ β© I ))) |
14 | 13 | rabbidva 3440 |
. . . 4
β’ (π β {π§ β π« π΅ β£ (πΉβ(π΅ β π§)) = (π΅ β π§)} = {π§ β π« π΅ β£ (π΅ β π§) β dom (πΉ β© I )}) |
15 | 1, 14 | eqtrid 2785 |
. . 3
β’ (π β π½ = {π§ β π« π΅ β£ (π΅ β π§) β dom (πΉ β© I )}) |
16 | | istopclsd.e |
. . . . . 6
β’ ((π β§ π₯ β π΅) β π₯ β (πΉβπ₯)) |
17 | | simp1 1137 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΅ β§ π¦ β π₯) β π) |
18 | | simp2 1138 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΅ β§ π¦ β π₯) β π₯ β π΅) |
19 | | simp3 1139 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΅ β§ π¦ β π₯) β π¦ β π₯) |
20 | 19, 18 | sstrd 3992 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΅ β§ π¦ β π₯) β π¦ β π΅) |
21 | | istopclsd.u |
. . . . . . . . 9
β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β (πΉβ(π₯ βͺ π¦)) = ((πΉβπ₯) βͺ (πΉβπ¦))) |
22 | 17, 18, 20, 21 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ π₯ β π΅ β§ π¦ β π₯) β (πΉβ(π₯ βͺ π¦)) = ((πΉβπ₯) βͺ (πΉβπ¦))) |
23 | | ssequn2 4183 |
. . . . . . . . . . 11
β’ (π¦ β π₯ β (π₯ βͺ π¦) = π₯) |
24 | 23 | biimpi 215 |
. . . . . . . . . 10
β’ (π¦ β π₯ β (π₯ βͺ π¦) = π₯) |
25 | 24 | 3ad2ant3 1136 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΅ β§ π¦ β π₯) β (π₯ βͺ π¦) = π₯) |
26 | 25 | fveq2d 6893 |
. . . . . . . 8
β’ ((π β§ π₯ β π΅ β§ π¦ β π₯) β (πΉβ(π₯ βͺ π¦)) = (πΉβπ₯)) |
27 | 22, 26 | eqtr3d 2775 |
. . . . . . 7
β’ ((π β§ π₯ β π΅ β§ π¦ β π₯) β ((πΉβπ₯) βͺ (πΉβπ¦)) = (πΉβπ₯)) |
28 | | ssequn2 4183 |
. . . . . . 7
β’ ((πΉβπ¦) β (πΉβπ₯) β ((πΉβπ₯) βͺ (πΉβπ¦)) = (πΉβπ₯)) |
29 | 27, 28 | sylibr 233 |
. . . . . 6
β’ ((π β§ π₯ β π΅ β§ π¦ β π₯) β (πΉβπ¦) β (πΉβπ₯)) |
30 | | istopclsd.i |
. . . . . 6
β’ ((π β§ π₯ β π΅) β (πΉβ(πΉβπ₯)) = (πΉβπ₯)) |
31 | 6, 2, 16, 29, 30 | ismrcd1 41422 |
. . . . 5
β’ (π β dom (πΉ β© I ) β (Mooreβπ΅)) |
32 | | istopclsd.z |
. . . . . 6
β’ (π β (πΉββ
) = β
) |
33 | | 0elpw 5354 |
. . . . . . 7
β’ β
β π« π΅ |
34 | | fnelfp 7170 |
. . . . . . 7
β’ ((πΉ Fn π« π΅ β§ β
β π« π΅) β (β
β dom
(πΉ β© I ) β (πΉββ
) =
β
)) |
35 | 3, 33, 34 | sylancl 587 |
. . . . . 6
β’ (π β (β
β dom (πΉ β© I ) β (πΉββ
) =
β
)) |
36 | 32, 35 | mpbird 257 |
. . . . 5
β’ (π β β
β dom (πΉ β© I )) |
37 | | simp1 1137 |
. . . . . . . 8
β’ ((π β§ π₯ β dom (πΉ β© I ) β§ π¦ β dom (πΉ β© I )) β π) |
38 | | inss1 4228 |
. . . . . . . . . . . . 13
β’ (πΉ β© I ) β πΉ |
39 | | dmss 5901 |
. . . . . . . . . . . . 13
β’ ((πΉ β© I ) β πΉ β dom (πΉ β© I ) β dom πΉ) |
40 | 38, 39 | ax-mp 5 |
. . . . . . . . . . . 12
β’ dom
(πΉ β© I ) β dom
πΉ |
41 | 40, 2 | fssdm 6735 |
. . . . . . . . . . 11
β’ (π β dom (πΉ β© I ) β π« π΅) |
42 | 41 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((π β§ π₯ β dom (πΉ β© I ) β§ π¦ β dom (πΉ β© I )) β dom (πΉ β© I ) β π« π΅) |
43 | | simp2 1138 |
. . . . . . . . . 10
β’ ((π β§ π₯ β dom (πΉ β© I ) β§ π¦ β dom (πΉ β© I )) β π₯ β dom (πΉ β© I )) |
44 | 42, 43 | sseldd 3983 |
. . . . . . . . 9
β’ ((π β§ π₯ β dom (πΉ β© I ) β§ π¦ β dom (πΉ β© I )) β π₯ β π« π΅) |
45 | 44 | elpwid 4611 |
. . . . . . . 8
β’ ((π β§ π₯ β dom (πΉ β© I ) β§ π¦ β dom (πΉ β© I )) β π₯ β π΅) |
46 | | simp3 1139 |
. . . . . . . . . 10
β’ ((π β§ π₯ β dom (πΉ β© I ) β§ π¦ β dom (πΉ β© I )) β π¦ β dom (πΉ β© I )) |
47 | 42, 46 | sseldd 3983 |
. . . . . . . . 9
β’ ((π β§ π₯ β dom (πΉ β© I ) β§ π¦ β dom (πΉ β© I )) β π¦ β π« π΅) |
48 | 47 | elpwid 4611 |
. . . . . . . 8
β’ ((π β§ π₯ β dom (πΉ β© I ) β§ π¦ β dom (πΉ β© I )) β π¦ β π΅) |
49 | 37, 45, 48, 21 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ π₯ β dom (πΉ β© I ) β§ π¦ β dom (πΉ β© I )) β (πΉβ(π₯ βͺ π¦)) = ((πΉβπ₯) βͺ (πΉβπ¦))) |
50 | 3 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((π β§ π₯ β dom (πΉ β© I ) β§ π¦ β dom (πΉ β© I )) β πΉ Fn π« π΅) |
51 | | fnelfp 7170 |
. . . . . . . . . 10
β’ ((πΉ Fn π« π΅ β§ π₯ β π« π΅) β (π₯ β dom (πΉ β© I ) β (πΉβπ₯) = π₯)) |
52 | 50, 44, 51 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π₯ β dom (πΉ β© I ) β§ π¦ β dom (πΉ β© I )) β (π₯ β dom (πΉ β© I ) β (πΉβπ₯) = π₯)) |
53 | 43, 52 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π₯ β dom (πΉ β© I ) β§ π¦ β dom (πΉ β© I )) β (πΉβπ₯) = π₯) |
54 | | fnelfp 7170 |
. . . . . . . . . 10
β’ ((πΉ Fn π« π΅ β§ π¦ β π« π΅) β (π¦ β dom (πΉ β© I ) β (πΉβπ¦) = π¦)) |
55 | 50, 47, 54 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π₯ β dom (πΉ β© I ) β§ π¦ β dom (πΉ β© I )) β (π¦ β dom (πΉ β© I ) β (πΉβπ¦) = π¦)) |
56 | 46, 55 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π₯ β dom (πΉ β© I ) β§ π¦ β dom (πΉ β© I )) β (πΉβπ¦) = π¦) |
57 | 53, 56 | uneq12d 4164 |
. . . . . . 7
β’ ((π β§ π₯ β dom (πΉ β© I ) β§ π¦ β dom (πΉ β© I )) β ((πΉβπ₯) βͺ (πΉβπ¦)) = (π₯ βͺ π¦)) |
58 | 49, 57 | eqtrd 2773 |
. . . . . 6
β’ ((π β§ π₯ β dom (πΉ β© I ) β§ π¦ β dom (πΉ β© I )) β (πΉβ(π₯ βͺ π¦)) = (π₯ βͺ π¦)) |
59 | 45, 48 | unssd 4186 |
. . . . . . . 8
β’ ((π β§ π₯ β dom (πΉ β© I ) β§ π¦ β dom (πΉ β© I )) β (π₯ βͺ π¦) β π΅) |
60 | | vex 3479 |
. . . . . . . . . 10
β’ π₯ β V |
61 | | vex 3479 |
. . . . . . . . . 10
β’ π¦ β V |
62 | 60, 61 | unex 7730 |
. . . . . . . . 9
β’ (π₯ βͺ π¦) β V |
63 | 62 | elpw 4606 |
. . . . . . . 8
β’ ((π₯ βͺ π¦) β π« π΅ β (π₯ βͺ π¦) β π΅) |
64 | 59, 63 | sylibr 233 |
. . . . . . 7
β’ ((π β§ π₯ β dom (πΉ β© I ) β§ π¦ β dom (πΉ β© I )) β (π₯ βͺ π¦) β π« π΅) |
65 | | fnelfp 7170 |
. . . . . . 7
β’ ((πΉ Fn π« π΅ β§ (π₯ βͺ π¦) β π« π΅) β ((π₯ βͺ π¦) β dom (πΉ β© I ) β (πΉβ(π₯ βͺ π¦)) = (π₯ βͺ π¦))) |
66 | 50, 64, 65 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π₯ β dom (πΉ β© I ) β§ π¦ β dom (πΉ β© I )) β ((π₯ βͺ π¦) β dom (πΉ β© I ) β (πΉβ(π₯ βͺ π¦)) = (π₯ βͺ π¦))) |
67 | 58, 66 | mpbird 257 |
. . . . 5
β’ ((π β§ π₯ β dom (πΉ β© I ) β§ π¦ β dom (πΉ β© I )) β (π₯ βͺ π¦) β dom (πΉ β© I )) |
68 | | eqid 2733 |
. . . . 5
β’ {π§ β π« π΅ β£ (π΅ β π§) β dom (πΉ β© I )} = {π§ β π« π΅ β£ (π΅ β π§) β dom (πΉ β© I )} |
69 | 31, 36, 67, 68 | mretopd 22588 |
. . . 4
β’ (π β ({π§ β π« π΅ β£ (π΅ β π§) β dom (πΉ β© I )} β (TopOnβπ΅) β§ dom (πΉ β© I ) = (Clsdβ{π§ β π« π΅ β£ (π΅ β π§) β dom (πΉ β© I )}))) |
70 | 69 | simpld 496 |
. . 3
β’ (π β {π§ β π« π΅ β£ (π΅ β π§) β dom (πΉ β© I )} β (TopOnβπ΅)) |
71 | 15, 70 | eqeltrd 2834 |
. 2
β’ (π β π½ β (TopOnβπ΅)) |
72 | | topontop 22407 |
. . . . . 6
β’ (π½ β (TopOnβπ΅) β π½ β Top) |
73 | 71, 72 | syl 17 |
. . . . 5
β’ (π β π½ β Top) |
74 | | eqid 2733 |
. . . . . 6
β’
(mrClsβ(Clsdβπ½)) = (mrClsβ(Clsdβπ½)) |
75 | 74 | mrccls 22575 |
. . . . 5
β’ (π½ β Top β
(clsβπ½) =
(mrClsβ(Clsdβπ½))) |
76 | 73, 75 | syl 17 |
. . . 4
β’ (π β (clsβπ½) =
(mrClsβ(Clsdβπ½))) |
77 | 69 | simprd 497 |
. . . . . 6
β’ (π β dom (πΉ β© I ) = (Clsdβ{π§ β π« π΅ β£ (π΅ β π§) β dom (πΉ β© I )})) |
78 | 15 | fveq2d 6893 |
. . . . . 6
β’ (π β (Clsdβπ½) = (Clsdβ{π§ β π« π΅ β£ (π΅ β π§) β dom (πΉ β© I )})) |
79 | 77, 78 | eqtr4d 2776 |
. . . . 5
β’ (π β dom (πΉ β© I ) = (Clsdβπ½)) |
80 | 79 | fveq2d 6893 |
. . . 4
β’ (π β (mrClsβdom (πΉ β© I )) =
(mrClsβ(Clsdβπ½))) |
81 | 76, 80 | eqtr4d 2776 |
. . 3
β’ (π β (clsβπ½) = (mrClsβdom (πΉ β© I ))) |
82 | 6, 2, 16, 29, 30 | ismrcd2 41423 |
. . 3
β’ (π β πΉ = (mrClsβdom (πΉ β© I ))) |
83 | 81, 82 | eqtr4d 2776 |
. 2
β’ (π β (clsβπ½) = πΉ) |
84 | 71, 83 | jca 513 |
1
β’ (π β (π½ β (TopOnβπ΅) β§ (clsβπ½) = πΉ)) |