Step | Hyp | Ref
| Expression |
1 | | distop 20799 |
. . . . 5
|
2 | 1 | adantl 482 |
. . . 4
|
3 | | simpl 473 |
. . . 4
|
4 | | unipw 4918 |
. . . . . 6
|
5 | 4 | eqcomi 2631 |
. . . . 5
|
6 | | eqid 2622 |
. . . . 5
↾t
↾t |
7 | | eqid 2622 |
. . . . 5
↾t
↾t |
8 | 5, 6, 7 | xkoval 21390 |
. . . 4
↾t |
9 | 2, 3, 8 | syl2anc 693 |
. . 3
↾t |
10 | | simpr 477 |
. . . . 5
|
11 | | fconst6g 6094 |
. . . . . 6
|
12 | 11 | adantr 481 |
. . . . 5
|
13 | | pttop 21385 |
. . . . 5
|
14 | 10, 12, 13 | syl2anc 693 |
. . . 4
|
15 | | elpwi 4168 |
. . . . . . . . . . . . . 14
|
16 | | restdis 20982 |
. . . . . . . . . . . . . 14
↾t |
17 | 15, 16 | sylan2 491 |
. . . . . . . . . . . . 13
↾t |
18 | 17 | adantll 750 |
. . . . . . . . . . . 12
↾t |
19 | 18 | eleq1d 2686 |
. . . . . . . . . . 11
↾t
|
20 | | discmp 21201 |
. . . . . . . . . . 11
|
21 | 19, 20 | syl6bbr 278 |
. . . . . . . . . 10
↾t
|
22 | 21 | rabbidva 3188 |
. . . . . . . . 9
↾t |
23 | | dfin5 3582 |
. . . . . . . . 9
|
24 | 22, 23 | syl6eqr 2674 |
. . . . . . . 8
↾t |
25 | | eqidd 2623 |
. . . . . . . 8
|
26 | | eqid 2622 |
. . . . . . . . . . 11
|
27 | 26 | toptopon 20722 |
. . . . . . . . . 10
TopOn |
28 | | cndis 21095 |
. . . . . . . . . . 11
TopOn |
29 | 28 | ancoms 469 |
. . . . . . . . . 10
TopOn
|
30 | 27, 29 | sylanb 489 |
. . . . . . . . 9
|
31 | | rabeq 3192 |
. . . . . . . . 9
|
32 | 30, 31 | syl 17 |
. . . . . . . 8
|
33 | 24, 25, 32 | mpt2eq123dv 6717 |
. . . . . . 7
↾t
|
34 | 33 | rneqd 5353 |
. . . . . 6
↾t
|
35 | | eqid 2622 |
. . . . . . 7
|
36 | 35 | rnmpt2 6770 |
. . . . . 6
|
37 | 34, 36 | syl6eq 2672 |
. . . . 5
↾t
|
38 | | elmapi 7879 |
. . . . . . . . . . . 12
|
39 | | eleq2 2690 |
. . . . . . . . . . . . . . . . 17
|
40 | 39 | imbi2d 330 |
. . . . . . . . . . . . . . . 16
|
41 | 40 | bibi1d 333 |
. . . . . . . . . . . . . . 15
|
42 | | eleq2 2690 |
. . . . . . . . . . . . . . . . 17
|
43 | 42 | imbi2d 330 |
. . . . . . . . . . . . . . . 16
|
44 | 43 | bibi1d 333 |
. . . . . . . . . . . . . . 15
|
45 | | inss1 3833 |
. . . . . . . . . . . . . . . . . . . . 21
|
46 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . 21
|
47 | 45, 46 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . 20
|
48 | 47 | elpwid 4170 |
. . . . . . . . . . . . . . . . . . 19
|
49 | 48 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
50 | 49 | sselda 3603 |
. . . . . . . . . . . . . . . . 17
|
51 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
52 | 50, 51 | 2thd 255 |
. . . . . . . . . . . . . . . 16
|
53 | 52 | imbi1d 331 |
. . . . . . . . . . . . . . 15
|
54 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . 19
|
55 | 54 | ex 450 |
. . . . . . . . . . . . . . . . . 18
|
56 | 55 | adantl 482 |
. . . . . . . . . . . . . . . . 17
|
57 | 56 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
58 | | pm2.21 120 |
. . . . . . . . . . . . . . . . 17
|
59 | 58 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
60 | 57, 59 | 2thd 255 |
. . . . . . . . . . . . . . 15
|
61 | 41, 44, 53, 60 | ifbothda 4123 |
. . . . . . . . . . . . . 14
|
62 | 61 | ralbidv2 2984 |
. . . . . . . . . . . . 13
|
63 | | ffn 6045 |
. . . . . . . . . . . . . . 15
|
64 | 63 | adantl 482 |
. . . . . . . . . . . . . 14
|
65 | | vex 3203 |
. . . . . . . . . . . . . . . 16
|
66 | 65 | elixp 7915 |
. . . . . . . . . . . . . . 15
|
67 | 66 | baib 944 |
. . . . . . . . . . . . . 14
|
68 | 64, 67 | syl 17 |
. . . . . . . . . . . . 13
|
69 | | ffun 6048 |
. . . . . . . . . . . . . . 15
|
70 | 69 | adantl 482 |
. . . . . . . . . . . . . 14
|
71 | | fdm 6051 |
. . . . . . . . . . . . . . . 16
|
72 | 71 | adantl 482 |
. . . . . . . . . . . . . . 15
|
73 | 49, 72 | sseqtr4d 3642 |
. . . . . . . . . . . . . 14
|
74 | | funimass4 6247 |
. . . . . . . . . . . . . 14
|
75 | 70, 73, 74 | syl2anc 693 |
. . . . . . . . . . . . 13
|
76 | 62, 68, 75 | 3bitr4d 300 |
. . . . . . . . . . . 12
|
77 | 38, 76 | sylan2 491 |
. . . . . . . . . . 11
|
78 | 77 | rabbi2dva 3821 |
. . . . . . . . . 10
|
79 | | elssuni 4467 |
. . . . . . . . . . . . . . . 16
|
80 | 79 | ad2antll 765 |
. . . . . . . . . . . . . . 15
|
81 | | ssid 3624 |
. . . . . . . . . . . . . . 15
|
82 | | sseq1 3626 |
. . . . . . . . . . . . . . . 16
|
83 | | sseq1 3626 |
. . . . . . . . . . . . . . . 16
|
84 | 82, 83 | ifboth 4124 |
. . . . . . . . . . . . . . 15
|
85 | 80, 81, 84 | sylancl 694 |
. . . . . . . . . . . . . 14
|
86 | 85 | ralrimivw 2967 |
. . . . . . . . . . . . 13
|
87 | | ss2ixp 7921 |
. . . . . . . . . . . . 13
|
88 | 86, 87 | syl 17 |
. . . . . . . . . . . 12
|
89 | | simplr 792 |
. . . . . . . . . . . . 13
|
90 | | uniexg 6955 |
. . . . . . . . . . . . . 14
|
91 | 90 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
92 | | ixpconstg 7917 |
. . . . . . . . . . . . 13
|
93 | 89, 91, 92 | syl2anc 693 |
. . . . . . . . . . . 12
|
94 | 88, 93 | sseqtrd 3641 |
. . . . . . . . . . 11
|
95 | | sseqin2 3817 |
. . . . . . . . . . 11
|
96 | 94, 95 | sylib 208 |
. . . . . . . . . 10
|
97 | 78, 96 | eqtr3d 2658 |
. . . . . . . . 9
|
98 | 11 | ad2antrr 762 |
. . . . . . . . . 10
|
99 | | inss2 3834 |
. . . . . . . . . . 11
|
100 | 99, 46 | sseldi 3601 |
. . . . . . . . . 10
|
101 | | simplrr 801 |
. . . . . . . . . . . 12
|
102 | 26 | topopn 20711 |
. . . . . . . . . . . . 13
|
103 | 102 | ad3antrrr 766 |
. . . . . . . . . . . 12
|
104 | 101, 103 | ifcld 4131 |
. . . . . . . . . . 11
|
105 | | simpll 790 |
. . . . . . . . . . . 12
|
106 | | fvconst2g 6467 |
. . . . . . . . . . . 12
|
107 | 105, 106 | sylan 488 |
. . . . . . . . . . 11
|
108 | 104, 107 | eleqtrrd 2704 |
. . . . . . . . . 10
|
109 | | eldifn 3733 |
. . . . . . . . . . . . 13
|
110 | 109 | iffalsed 4097 |
. . . . . . . . . . . 12
|
111 | 110 | adantl 482 |
. . . . . . . . . . 11
|
112 | | eldifi 3732 |
. . . . . . . . . . . . 13
|
113 | 112, 107 | sylan2 491 |
. . . . . . . . . . . 12
|
114 | 113 | unieqd 4446 |
. . . . . . . . . . 11
|
115 | 111, 114 | eqtr4d 2659 |
. . . . . . . . . 10
|
116 | 89, 98, 100, 108, 115 | ptopn 21386 |
. . . . . . . . 9
|
117 | 97, 116 | eqeltrd 2701 |
. . . . . . . 8
|
118 | | eleq1 2689 |
. . . . . . . 8
|
119 | 117, 118 | syl5ibrcom 237 |
. . . . . . 7
|
120 | 119 | rexlimdvva 3038 |
. . . . . 6
|
121 | 120 | abssdv 3676 |
. . . . 5
|
122 | 37, 121 | eqsstrd 3639 |
. . . 4
↾t |
123 | | tgfiss 20795 |
. . . 4
↾t
↾t |
124 | 14, 122, 123 | syl2anc 693 |
. . 3
↾t |
125 | 9, 124 | eqsstrd 3639 |
. 2
|
126 | | eqid 2622 |
. . . . . . . 8
|
127 | 126, 26 | ptuniconst 21401 |
. . . . . . 7
|
128 | 127 | ancoms 469 |
. . . . . 6
|
129 | 30, 128 | eqtrd 2656 |
. . . . 5
|
130 | 129 | oveq2d 6666 |
. . . 4
↾t
↾t |
131 | | eqid 2622 |
. . . . . 6
|
132 | 131 | restid 16094 |
. . . . 5
↾t |
133 | 14, 132 | syl 17 |
. . . 4
↾t |
134 | 130, 133 | eqtrd 2656 |
. . 3
↾t |
135 | 5, 126 | xkoptsub 21457 |
. . . 4
↾t
|
136 | 2, 3, 135 | syl2anc 693 |
. . 3
↾t
|
137 | 134, 136 | eqsstr3d 3640 |
. 2
|
138 | 125, 137 | eqssd 3620 |
1
|