Step | Hyp | Ref
| Expression |
1 | | qtoprest.2 |
. . . . . 6
β’ (π β π½ β (TopOnβπ)) |
2 | | qtoprest.3 |
. . . . . . 7
β’ (π β πΉ:πβontoβπ) |
3 | | fofn 6759 |
. . . . . . 7
β’ (πΉ:πβontoβπ β πΉ Fn π) |
4 | 2, 3 | syl 17 |
. . . . . 6
β’ (π β πΉ Fn π) |
5 | | qtopid 23059 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΉ Fn π) β πΉ β (π½ Cn (π½ qTop πΉ))) |
6 | 1, 4, 5 | syl2anc 585 |
. . . . 5
β’ (π β πΉ β (π½ Cn (π½ qTop πΉ))) |
7 | | qtoprest.5 |
. . . . . . 7
β’ (π β π΄ = (β‘πΉ β π)) |
8 | | cnvimass 6034 |
. . . . . . . 8
β’ (β‘πΉ β π) β dom πΉ |
9 | 4 | fndmd 6608 |
. . . . . . . 8
β’ (π β dom πΉ = π) |
10 | 8, 9 | sseqtrid 3997 |
. . . . . . 7
β’ (π β (β‘πΉ β π) β π) |
11 | 7, 10 | eqsstrd 3983 |
. . . . . 6
β’ (π β π΄ β π) |
12 | | toponuni 22266 |
. . . . . . 7
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
13 | 1, 12 | syl 17 |
. . . . . 6
β’ (π β π = βͺ π½) |
14 | 11, 13 | sseqtrd 3985 |
. . . . 5
β’ (π β π΄ β βͺ π½) |
15 | | eqid 2737 |
. . . . . 6
β’ βͺ π½ =
βͺ π½ |
16 | 15 | cnrest 22639 |
. . . . 5
β’ ((πΉ β (π½ Cn (π½ qTop πΉ)) β§ π΄ β βͺ π½) β (πΉ βΎ π΄) β ((π½ βΎt π΄) Cn (π½ qTop πΉ))) |
17 | 6, 14, 16 | syl2anc 585 |
. . . 4
β’ (π β (πΉ βΎ π΄) β ((π½ βΎt π΄) Cn (π½ qTop πΉ))) |
18 | | qtoptopon 23058 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β (π½ qTop πΉ) β (TopOnβπ)) |
19 | 1, 2, 18 | syl2anc 585 |
. . . . 5
β’ (π β (π½ qTop πΉ) β (TopOnβπ)) |
20 | | df-ima 5647 |
. . . . . . 7
β’ (πΉ β π΄) = ran (πΉ βΎ π΄) |
21 | 7 | imaeq2d 6014 |
. . . . . . . 8
β’ (π β (πΉ β π΄) = (πΉ β (β‘πΉ β π))) |
22 | | qtoprest.4 |
. . . . . . . . 9
β’ (π β π β π) |
23 | | foimacnv 6802 |
. . . . . . . . 9
β’ ((πΉ:πβontoβπ β§ π β π) β (πΉ β (β‘πΉ β π)) = π) |
24 | 2, 22, 23 | syl2anc 585 |
. . . . . . . 8
β’ (π β (πΉ β (β‘πΉ β π)) = π) |
25 | 21, 24 | eqtrd 2777 |
. . . . . . 7
β’ (π β (πΉ β π΄) = π) |
26 | 20, 25 | eqtr3id 2791 |
. . . . . 6
β’ (π β ran (πΉ βΎ π΄) = π) |
27 | | eqimss 4001 |
. . . . . 6
β’ (ran
(πΉ βΎ π΄) = π β ran (πΉ βΎ π΄) β π) |
28 | 26, 27 | syl 17 |
. . . . 5
β’ (π β ran (πΉ βΎ π΄) β π) |
29 | | cnrest2 22640 |
. . . . 5
β’ (((π½ qTop πΉ) β (TopOnβπ) β§ ran (πΉ βΎ π΄) β π β§ π β π) β ((πΉ βΎ π΄) β ((π½ βΎt π΄) Cn (π½ qTop πΉ)) β (πΉ βΎ π΄) β ((π½ βΎt π΄) Cn ((π½ qTop πΉ) βΎt π)))) |
30 | 19, 28, 22, 29 | syl3anc 1372 |
. . . 4
β’ (π β ((πΉ βΎ π΄) β ((π½ βΎt π΄) Cn (π½ qTop πΉ)) β (πΉ βΎ π΄) β ((π½ βΎt π΄) Cn ((π½ qTop πΉ) βΎt π)))) |
31 | 17, 30 | mpbid 231 |
. . 3
β’ (π β (πΉ βΎ π΄) β ((π½ βΎt π΄) Cn ((π½ qTop πΉ) βΎt π))) |
32 | | resttopon 22515 |
. . . 4
β’ (((π½ qTop πΉ) β (TopOnβπ) β§ π β π) β ((π½ qTop πΉ) βΎt π) β (TopOnβπ)) |
33 | 19, 22, 32 | syl2anc 585 |
. . 3
β’ (π β ((π½ qTop πΉ) βΎt π) β (TopOnβπ)) |
34 | | qtopss 23069 |
. . 3
β’ (((πΉ βΎ π΄) β ((π½ βΎt π΄) Cn ((π½ qTop πΉ) βΎt π)) β§ ((π½ qTop πΉ) βΎt π) β (TopOnβπ) β§ ran (πΉ βΎ π΄) = π) β ((π½ qTop πΉ) βΎt π) β ((π½ βΎt π΄) qTop (πΉ βΎ π΄))) |
35 | 31, 33, 26, 34 | syl3anc 1372 |
. 2
β’ (π β ((π½ qTop πΉ) βΎt π) β ((π½ βΎt π΄) qTop (πΉ βΎ π΄))) |
36 | | resttopon 22515 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π½ βΎt π΄) β (TopOnβπ΄)) |
37 | 1, 11, 36 | syl2anc 585 |
. . . . 5
β’ (π β (π½ βΎt π΄) β (TopOnβπ΄)) |
38 | | fnfun 6603 |
. . . . . . . 8
β’ (πΉ Fn π β Fun πΉ) |
39 | 4, 38 | syl 17 |
. . . . . . 7
β’ (π β Fun πΉ) |
40 | 11, 9 | sseqtrrd 3986 |
. . . . . . 7
β’ (π β π΄ β dom πΉ) |
41 | | fores 6767 |
. . . . . . 7
β’ ((Fun
πΉ β§ π΄ β dom πΉ) β (πΉ βΎ π΄):π΄βontoβ(πΉ β π΄)) |
42 | 39, 40, 41 | syl2anc 585 |
. . . . . 6
β’ (π β (πΉ βΎ π΄):π΄βontoβ(πΉ β π΄)) |
43 | | foeq3 6755 |
. . . . . . 7
β’ ((πΉ β π΄) = π β ((πΉ βΎ π΄):π΄βontoβ(πΉ β π΄) β (πΉ βΎ π΄):π΄βontoβπ)) |
44 | 25, 43 | syl 17 |
. . . . . 6
β’ (π β ((πΉ βΎ π΄):π΄βontoβ(πΉ β π΄) β (πΉ βΎ π΄):π΄βontoβπ)) |
45 | 42, 44 | mpbid 231 |
. . . . 5
β’ (π β (πΉ βΎ π΄):π΄βontoβπ) |
46 | | elqtop3 23057 |
. . . . 5
β’ (((π½ βΎt π΄) β (TopOnβπ΄) β§ (πΉ βΎ π΄):π΄βontoβπ) β (π₯ β ((π½ βΎt π΄) qTop (πΉ βΎ π΄)) β (π₯ β π β§ (β‘(πΉ βΎ π΄) β π₯) β (π½ βΎt π΄)))) |
47 | 37, 45, 46 | syl2anc 585 |
. . . 4
β’ (π β (π₯ β ((π½ βΎt π΄) qTop (πΉ βΎ π΄)) β (π₯ β π β§ (β‘(πΉ βΎ π΄) β π₯) β (π½ βΎt π΄)))) |
48 | | cnvresima 6183 |
. . . . . . . 8
β’ (β‘(πΉ βΎ π΄) β π₯) = ((β‘πΉ β π₯) β© π΄) |
49 | | imass2 6055 |
. . . . . . . . . . 11
β’ (π₯ β π β (β‘πΉ β π₯) β (β‘πΉ β π)) |
50 | 49 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β (β‘πΉ β π₯) β (β‘πΉ β π)) |
51 | 7 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β π΄ = (β‘πΉ β π)) |
52 | 50, 51 | sseqtrrd 3986 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β (β‘πΉ β π₯) β π΄) |
53 | | df-ss 3928 |
. . . . . . . . 9
β’ ((β‘πΉ β π₯) β π΄ β ((β‘πΉ β π₯) β© π΄) = (β‘πΉ β π₯)) |
54 | 52, 53 | sylib 217 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β ((β‘πΉ β π₯) β© π΄) = (β‘πΉ β π₯)) |
55 | 48, 54 | eqtrid 2789 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (β‘(πΉ βΎ π΄) β π₯) = (β‘πΉ β π₯)) |
56 | 55 | eleq1d 2823 |
. . . . . 6
β’ ((π β§ π₯ β π) β ((β‘(πΉ βΎ π΄) β π₯) β (π½ βΎt π΄) β (β‘πΉ β π₯) β (π½ βΎt π΄))) |
57 | | simplrl 776 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β π½) β π₯ β π) |
58 | | df-ss 3928 |
. . . . . . . . . 10
β’ (π₯ β π β (π₯ β© π) = π₯) |
59 | 57, 58 | sylib 217 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β π½) β (π₯ β© π) = π₯) |
60 | | topontop 22265 |
. . . . . . . . . . . 12
β’ ((π½ qTop πΉ) β (TopOnβπ) β (π½ qTop πΉ) β Top) |
61 | 19, 60 | syl 17 |
. . . . . . . . . . 11
β’ (π β (π½ qTop πΉ) β Top) |
62 | 61 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β π½) β (π½ qTop πΉ) β Top) |
63 | | toponmax 22278 |
. . . . . . . . . . . . . 14
β’ (π½ β (TopOnβπ) β π β π½) |
64 | 1, 63 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π β π½) |
65 | | focdmex 7889 |
. . . . . . . . . . . . 13
β’ (π β π½ β (πΉ:πβontoβπ β π β V)) |
66 | 64, 2, 65 | sylc 65 |
. . . . . . . . . . . 12
β’ (π β π β V) |
67 | 66, 22 | ssexd 5282 |
. . . . . . . . . . 11
β’ (π β π β V) |
68 | 67 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β π½) β π β V) |
69 | 22 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β π½) β π β π) |
70 | 57, 69 | sstrd 3955 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β π½) β π₯ β π) |
71 | | topontop 22265 |
. . . . . . . . . . . . . . . 16
β’ (π½ β (TopOnβπ) β π½ β Top) |
72 | 1, 71 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π½ β Top) |
73 | | restopn2 22531 |
. . . . . . . . . . . . . . 15
β’ ((π½ β Top β§ π΄ β π½) β ((β‘πΉ β π₯) β (π½ βΎt π΄) β ((β‘πΉ β π₯) β π½ β§ (β‘πΉ β π₯) β π΄))) |
74 | 72, 73 | sylan 581 |
. . . . . . . . . . . . . 14
β’ ((π β§ π΄ β π½) β ((β‘πΉ β π₯) β (π½ βΎt π΄) β ((β‘πΉ β π₯) β π½ β§ (β‘πΉ β π₯) β π΄))) |
75 | 74 | simprbda 500 |
. . . . . . . . . . . . 13
β’ (((π β§ π΄ β π½) β§ (β‘πΉ β π₯) β (π½ βΎt π΄)) β (β‘πΉ β π₯) β π½) |
76 | 75 | adantrl 715 |
. . . . . . . . . . . 12
β’ (((π β§ π΄ β π½) β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β (β‘πΉ β π₯) β π½) |
77 | 76 | an32s 651 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β π½) β (β‘πΉ β π₯) β π½) |
78 | | elqtop3 23057 |
. . . . . . . . . . . . 13
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β (π₯ β (π½ qTop πΉ) β (π₯ β π β§ (β‘πΉ β π₯) β π½))) |
79 | 1, 2, 78 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (π₯ β (π½ qTop πΉ) β (π₯ β π β§ (β‘πΉ β π₯) β π½))) |
80 | 79 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β π½) β (π₯ β (π½ qTop πΉ) β (π₯ β π β§ (β‘πΉ β π₯) β π½))) |
81 | 70, 77, 80 | mpbir2and 712 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β π½) β π₯ β (π½ qTop πΉ)) |
82 | | elrestr 17311 |
. . . . . . . . . 10
β’ (((π½ qTop πΉ) β Top β§ π β V β§ π₯ β (π½ qTop πΉ)) β (π₯ β© π) β ((π½ qTop πΉ) βΎt π)) |
83 | 62, 68, 81, 82 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β π½) β (π₯ β© π) β ((π½ qTop πΉ) βΎt π)) |
84 | 59, 83 | eqeltrrd 2839 |
. . . . . . . 8
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β π½) β π₯ β ((π½ qTop πΉ) βΎt π)) |
85 | 33 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β ((π½ qTop πΉ) βΎt π) β (TopOnβπ)) |
86 | | toponuni 22266 |
. . . . . . . . . . . 12
β’ (((π½ qTop πΉ) βΎt π) β (TopOnβπ) β π = βͺ ((π½ qTop πΉ) βΎt π)) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β π = βͺ ((π½ qTop πΉ) βΎt π)) |
88 | 87 | difeq1d 4082 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β (π β π₯) = (βͺ ((π½ qTop πΉ) βΎt π) β π₯)) |
89 | 22 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β π β π) |
90 | 19 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β (π½ qTop πΉ) β (TopOnβπ)) |
91 | | toponuni 22266 |
. . . . . . . . . . . . 13
β’ ((π½ qTop πΉ) β (TopOnβπ) β π = βͺ (π½ qTop πΉ)) |
92 | 90, 91 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β π = βͺ (π½ qTop πΉ)) |
93 | 89, 92 | sseqtrd 3985 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β π β βͺ (π½ qTop πΉ)) |
94 | 89 | ssdifssd 4103 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β (π β π₯) β π) |
95 | 39 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β Fun πΉ) |
96 | | funcnvcnv 6569 |
. . . . . . . . . . . . . . 15
β’ (Fun
πΉ β Fun β‘β‘πΉ) |
97 | | imadif 6586 |
. . . . . . . . . . . . . . 15
β’ (Fun
β‘β‘πΉ β (β‘πΉ β (π β π₯)) = ((β‘πΉ β π) β (β‘πΉ β π₯))) |
98 | 95, 96, 97 | 3syl 18 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β (β‘πΉ β (π β π₯)) = ((β‘πΉ β π) β (β‘πΉ β π₯))) |
99 | 7 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β π΄ = (β‘πΉ β π)) |
100 | 99 | difeq1d 4082 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β (π΄ β (β‘πΉ β π₯)) = ((β‘πΉ β π) β (β‘πΉ β π₯))) |
101 | 98, 100 | eqtr4d 2780 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β (β‘πΉ β (π β π₯)) = (π΄ β (β‘πΉ β π₯))) |
102 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β π΄ β (Clsdβπ½)) |
103 | 37 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β (π½ βΎt π΄) β (TopOnβπ΄)) |
104 | | toponuni 22266 |
. . . . . . . . . . . . . . . . 17
β’ ((π½ βΎt π΄) β (TopOnβπ΄) β π΄ = βͺ (π½ βΎt π΄)) |
105 | 103, 104 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β π΄ = βͺ (π½ βΎt π΄)) |
106 | 105 | difeq1d 4082 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β (π΄ β (β‘πΉ β π₯)) = (βͺ (π½ βΎt π΄) β (β‘πΉ β π₯))) |
107 | | topontop 22265 |
. . . . . . . . . . . . . . . . 17
β’ ((π½ βΎt π΄) β (TopOnβπ΄) β (π½ βΎt π΄) β Top) |
108 | 103, 107 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β (π½ βΎt π΄) β Top) |
109 | | simplrr 777 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β (β‘πΉ β π₯) β (π½ βΎt π΄)) |
110 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’ βͺ (π½
βΎt π΄) =
βͺ (π½ βΎt π΄) |
111 | 110 | opncld 22387 |
. . . . . . . . . . . . . . . 16
β’ (((π½ βΎt π΄) β Top β§ (β‘πΉ β π₯) β (π½ βΎt π΄)) β (βͺ
(π½ βΎt
π΄) β (β‘πΉ β π₯)) β (Clsdβ(π½ βΎt π΄))) |
112 | 108, 109,
111 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β (βͺ
(π½ βΎt
π΄) β (β‘πΉ β π₯)) β (Clsdβ(π½ βΎt π΄))) |
113 | 106, 112 | eqeltrd 2838 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β (π΄ β (β‘πΉ β π₯)) β (Clsdβ(π½ βΎt π΄))) |
114 | | restcldr 22528 |
. . . . . . . . . . . . . 14
β’ ((π΄ β (Clsdβπ½) β§ (π΄ β (β‘πΉ β π₯)) β (Clsdβ(π½ βΎt π΄))) β (π΄ β (β‘πΉ β π₯)) β (Clsdβπ½)) |
115 | 102, 113,
114 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β (π΄ β (β‘πΉ β π₯)) β (Clsdβπ½)) |
116 | 101, 115 | eqeltrd 2838 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β (β‘πΉ β (π β π₯)) β (Clsdβπ½)) |
117 | | qtopcld 23067 |
. . . . . . . . . . . . . 14
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β ((π β π₯) β (Clsdβ(π½ qTop πΉ)) β ((π β π₯) β π β§ (β‘πΉ β (π β π₯)) β (Clsdβπ½)))) |
118 | 1, 2, 117 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β ((π β π₯) β (Clsdβ(π½ qTop πΉ)) β ((π β π₯) β π β§ (β‘πΉ β (π β π₯)) β (Clsdβπ½)))) |
119 | 118 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β ((π β π₯) β (Clsdβ(π½ qTop πΉ)) β ((π β π₯) β π β§ (β‘πΉ β (π β π₯)) β (Clsdβπ½)))) |
120 | 94, 116, 119 | mpbir2and 712 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β (π β π₯) β (Clsdβ(π½ qTop πΉ))) |
121 | | difssd 4093 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β (π β π₯) β π) |
122 | | eqid 2737 |
. . . . . . . . . . . 12
β’ βͺ (π½
qTop πΉ) = βͺ (π½
qTop πΉ) |
123 | 122 | restcldi 22527 |
. . . . . . . . . . 11
β’ ((π β βͺ (π½
qTop πΉ) β§ (π β π₯) β (Clsdβ(π½ qTop πΉ)) β§ (π β π₯) β π) β (π β π₯) β (Clsdβ((π½ qTop πΉ) βΎt π))) |
124 | 93, 120, 121, 123 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β (π β π₯) β (Clsdβ((π½ qTop πΉ) βΎt π))) |
125 | 88, 124 | eqeltrrd 2839 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β (βͺ
((π½ qTop πΉ) βΎt π) β π₯) β (Clsdβ((π½ qTop πΉ) βΎt π))) |
126 | | topontop 22265 |
. . . . . . . . . . 11
β’ (((π½ qTop πΉ) βΎt π) β (TopOnβπ) β ((π½ qTop πΉ) βΎt π) β Top) |
127 | 85, 126 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β ((π½ qTop πΉ) βΎt π) β Top) |
128 | | simplrl 776 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β π₯ β π) |
129 | 128, 87 | sseqtrd 3985 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β π₯ β βͺ ((π½ qTop πΉ) βΎt π)) |
130 | | eqid 2737 |
. . . . . . . . . . 11
β’ βͺ ((π½
qTop πΉ) βΎt
π) = βͺ ((π½
qTop πΉ) βΎt
π) |
131 | 130 | isopn2 22386 |
. . . . . . . . . 10
β’ ((((π½ qTop πΉ) βΎt π) β Top β§ π₯ β βͺ ((π½ qTop πΉ) βΎt π)) β (π₯ β ((π½ qTop πΉ) βΎt π) β (βͺ
((π½ qTop πΉ) βΎt π) β π₯) β (Clsdβ((π½ qTop πΉ) βΎt π)))) |
132 | 127, 129,
131 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β (π₯ β ((π½ qTop πΉ) βΎt π) β (βͺ
((π½ qTop πΉ) βΎt π) β π₯) β (Clsdβ((π½ qTop πΉ) βΎt π)))) |
133 | 125, 132 | mpbird 257 |
. . . . . . . 8
β’ (((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β§ π΄ β (Clsdβπ½)) β π₯ β ((π½ qTop πΉ) βΎt π)) |
134 | | qtoprest.6 |
. . . . . . . . 9
β’ (π β (π΄ β π½ β¨ π΄ β (Clsdβπ½))) |
135 | 134 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β (π΄ β π½ β¨ π΄ β (Clsdβπ½))) |
136 | 84, 133, 135 | mpjaodan 958 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ (β‘πΉ β π₯) β (π½ βΎt π΄))) β π₯ β ((π½ qTop πΉ) βΎt π)) |
137 | 136 | expr 458 |
. . . . . 6
β’ ((π β§ π₯ β π) β ((β‘πΉ β π₯) β (π½ βΎt π΄) β π₯ β ((π½ qTop πΉ) βΎt π))) |
138 | 56, 137 | sylbid 239 |
. . . . 5
β’ ((π β§ π₯ β π) β ((β‘(πΉ βΎ π΄) β π₯) β (π½ βΎt π΄) β π₯ β ((π½ qTop πΉ) βΎt π))) |
139 | 138 | expimpd 455 |
. . . 4
β’ (π β ((π₯ β π β§ (β‘(πΉ βΎ π΄) β π₯) β (π½ βΎt π΄)) β π₯ β ((π½ qTop πΉ) βΎt π))) |
140 | 47, 139 | sylbid 239 |
. . 3
β’ (π β (π₯ β ((π½ βΎt π΄) qTop (πΉ βΎ π΄)) β π₯ β ((π½ qTop πΉ) βΎt π))) |
141 | 140 | ssrdv 3951 |
. 2
β’ (π β ((π½ βΎt π΄) qTop (πΉ βΎ π΄)) β ((π½ qTop πΉ) βΎt π)) |
142 | 35, 141 | eqssd 3962 |
1
β’ (π β ((π½ qTop πΉ) βΎt π) = ((π½ βΎt π΄) qTop (πΉ βΎ π΄))) |