Step | Hyp | Ref
| Expression |
1 | | simp1 1061 |
. . . 4
PsMet
|
2 | | psmetres2 22119 |
. . . . 5
PsMet PsMet |
3 | 2 | 3adant1 1079 |
. . . 4
PsMet
PsMet |
4 | | oveq2 6658 |
. . . . . . . 8
|
5 | 4 | imaeq2d 5466 |
. . . . . . 7
|
6 | 5 | cbvmptv 4750 |
. . . . . 6
|
7 | 6 | rneqi 5352 |
. . . . 5
|
8 | 7 | metustfbas 22362 |
. . . 4
PsMet
|
9 | 1, 3, 8 | syl2anc 693 |
. . 3
PsMet
|
10 | | fgval 21674 |
. . 3
|
11 | 9, 10 | syl 17 |
. 2
PsMet
|
12 | | metuval 22354 |
. . 3
PsMet metUnif |
13 | 3, 12 | syl 17 |
. 2
PsMet
metUnif |
14 | | fvex 6201 |
. . . 4
metUnif |
15 | 3 | elfvexd 6222 |
. . . . 5
PsMet
|
16 | | xpexg 6960 |
. . . . 5
|
17 | 15, 15, 16 | syl2anc 693 |
. . . 4
PsMet
|
18 | | restval 16087 |
. . . 4
metUnif metUnif ↾t metUnif |
19 | 14, 17, 18 | sylancr 695 |
. . 3
PsMet
metUnif ↾t metUnif |
20 | | inss2 3834 |
. . . . . . . . . . 11
|
21 | | sseq1 3626 |
. . . . . . . . . . 11
|
22 | 20, 21 | mpbiri 248 |
. . . . . . . . . 10
|
23 | | vex 3203 |
. . . . . . . . . . 11
|
24 | 23 | elpw 4164 |
. . . . . . . . . 10
|
25 | 22, 24 | sylibr 224 |
. . . . . . . . 9
|
26 | 25 | rexlimivw 3029 |
. . . . . . . 8
metUnif
|
27 | 26 | adantl 482 |
. . . . . . 7
PsMet
metUnif
|
28 | | nfv 1843 |
. . . . . . . . . . . 12
PsMet
metUnif
|
29 | | nfmpt1 4747 |
. . . . . . . . . . . . . 14
|
30 | 29 | nfrn 5368 |
. . . . . . . . . . . . 13
|
31 | 30 | nfcri 2758 |
. . . . . . . . . . . 12
|
32 | 28, 31 | nfan 1828 |
. . . . . . . . . . 11
PsMet
metUnif
|
33 | | nfv 1843 |
. . . . . . . . . . 11
|
34 | 32, 33 | nfan 1828 |
. . . . . . . . . 10
PsMet
metUnif
|
35 | | nfmpt1 4747 |
. . . . . . . . . . . . 13
|
36 | 35 | nfrn 5368 |
. . . . . . . . . . . 12
|
37 | | nfcv 2764 |
. . . . . . . . . . . 12
|
38 | 36, 37 | nfin 3820 |
. . . . . . . . . . 11
|
39 | | nfcv 2764 |
. . . . . . . . . . 11
|
40 | 38, 39 | nfne 2894 |
. . . . . . . . . 10
|
41 | | simplr 792 |
. . . . . . . . . . . . 13
PsMet metUnif
|
42 | | ineq1 3807 |
. . . . . . . . . . . . . . 15
|
43 | 42 | adantl 482 |
. . . . . . . . . . . . . 14
PsMet metUnif
|
44 | | simp2 1062 |
. . . . . . . . . . . . . . . 16
PsMet
PsMet |
45 | | psmetf 22111 |
. . . . . . . . . . . . . . . 16
PsMet
|
46 | | ffun 6048 |
. . . . . . . . . . . . . . . 16
|
47 | | respreima 6344 |
. . . . . . . . . . . . . . . 16
|
48 | 44, 45, 46, 47 | 4syl 19 |
. . . . . . . . . . . . . . 15
PsMet
|
49 | 48 | ad6antr 772 |
. . . . . . . . . . . . . 14
PsMet metUnif
|
50 | 43, 49 | eqtr4d 2659 |
. . . . . . . . . . . . 13
PsMet metUnif
|
51 | | rspe 3003 |
. . . . . . . . . . . . 13
|
52 | 41, 50, 51 | syl2anc 693 |
. . . . . . . . . . . 12
PsMet metUnif
|
53 | | vex 3203 |
. . . . . . . . . . . . . 14
|
54 | 53 | inex1 4799 |
. . . . . . . . . . . . 13
|
55 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
56 | 55 | elrnmpt 5372 |
. . . . . . . . . . . . 13
|
57 | 54, 56 | ax-mp 5 |
. . . . . . . . . . . 12
|
58 | 52, 57 | sylibr 224 |
. . . . . . . . . . 11
PsMet metUnif
|
59 | | simpllr 799 |
. . . . . . . . . . . . 13
PsMet metUnif
|
60 | | ssinss1 3841 |
. . . . . . . . . . . . 13
|
61 | 59, 60 | syl 17 |
. . . . . . . . . . . 12
PsMet metUnif
|
62 | | inss2 3834 |
. . . . . . . . . . . . 13
|
63 | 62 | a1i 11 |
. . . . . . . . . . . 12
PsMet metUnif
|
64 | | pweq 4161 |
. . . . . . . . . . . . . . . 16
|
65 | 64 | eleq2d 2687 |
. . . . . . . . . . . . . . 15
|
66 | 54 | elpw 4164 |
. . . . . . . . . . . . . . 15
|
67 | 65, 66 | syl6bb 276 |
. . . . . . . . . . . . . 14
|
68 | | ssin 3835 |
. . . . . . . . . . . . . 14
|
69 | 67, 68 | syl6bbr 278 |
. . . . . . . . . . . . 13
|
70 | 69 | ad5antlr 771 |
. . . . . . . . . . . 12
PsMet metUnif
|
71 | 61, 63, 70 | mpbir2and 957 |
. . . . . . . . . . 11
PsMet metUnif
|
72 | | inelcm 4032 |
. . . . . . . . . . 11
|
73 | 58, 71, 72 | syl2anc 693 |
. . . . . . . . . 10
PsMet metUnif
|
74 | | simplr 792 |
. . . . . . . . . . 11
PsMet
metUnif
|
75 | | eqid 2622 |
. . . . . . . . . . . . 13
|
76 | 75 | elrnmpt 5372 |
. . . . . . . . . . . 12
|
77 | 53, 76 | ax-mp 5 |
. . . . . . . . . . 11
|
78 | 74, 77 | sylib 208 |
. . . . . . . . . 10
PsMet
metUnif
|
79 | 34, 40, 73, 78 | r19.29af2 3075 |
. . . . . . . . 9
PsMet
metUnif
|
80 | | ssn0 3976 |
. . . . . . . . . . . . . 14
|
81 | 80 | ancoms 469 |
. . . . . . . . . . . . 13
|
82 | 81 | 3adant2 1080 |
. . . . . . . . . . . 12
PsMet
|
83 | | metuel 22369 |
. . . . . . . . . . . 12
PsMet
metUnif
|
84 | 82, 44, 83 | syl2anc 693 |
. . . . . . . . . . 11
PsMet
metUnif
|
85 | 84 | simplbda 654 |
. . . . . . . . . 10
PsMet
metUnif
|
86 | 85 | adantr 481 |
. . . . . . . . 9
PsMet metUnif
|
87 | 79, 86 | r19.29a 3078 |
. . . . . . . 8
PsMet metUnif
|
88 | 87 | r19.29an 3077 |
. . . . . . 7
PsMet
metUnif |
89 | 27, 88 | jca 554 |
. . . . . 6
PsMet
metUnif
|
90 | | simprl 794 |
. . . . . . . . . . 11
PsMet
|
91 | 90 | elpwid 4170 |
. . . . . . . . . 10
PsMet
|
92 | | simpl3 1066 |
. . . . . . . . . . 11
PsMet
|
93 | | xpss12 5225 |
. . . . . . . . . . 11
|
94 | 92, 92, 93 | syl2anc 693 |
. . . . . . . . . 10
PsMet
|
95 | 91, 94 | sstrd 3613 |
. . . . . . . . 9
PsMet
|
96 | | difssd 3738 |
. . . . . . . . 9
PsMet
|
97 | 95, 96 | unssd 3789 |
. . . . . . . 8
PsMet
|
98 | | simplr 792 |
. . . . . . . . . . . 12
PsMet
|
99 | | eqidd 2623 |
. . . . . . . . . . . 12
PsMet
|
100 | 4 | imaeq2d 5466 |
. . . . . . . . . . . . . 14
|
101 | 100 | eqeq2d 2632 |
. . . . . . . . . . . . 13
|
102 | 101 | rspcev 3309 |
. . . . . . . . . . . 12
|
103 | 98, 99, 102 | syl2anc 693 |
. . . . . . . . . . 11
PsMet
|
104 | 44 | ad4antr 768 |
. . . . . . . . . . . 12
PsMet
PsMet |
105 | | cnvexg 7112 |
. . . . . . . . . . . 12
PsMet
|
106 | | imaexg 7103 |
. . . . . . . . . . . 12
|
107 | 75 | elrnmpt 5372 |
. . . . . . . . . . . 12
|
108 | 104, 105,
106, 107 | 4syl 19 |
. . . . . . . . . . 11
PsMet
|
109 | 103, 108 | mpbird 247 |
. . . . . . . . . 10
PsMet
|
110 | | cnvimass 5485 |
. . . . . . . . . . . . . . . 16
|
111 | | fdm 6051 |
. . . . . . . . . . . . . . . . 17
|
112 | 45, 111 | syl 17 |
. . . . . . . . . . . . . . . 16
PsMet
|
113 | 110, 112 | syl5sseq 3653 |
. . . . . . . . . . . . . . 15
PsMet
|
114 | 104, 113 | syl 17 |
. . . . . . . . . . . . . 14
PsMet
|
115 | | ssdif0 3942 |
. . . . . . . . . . . . . 14
|
116 | 114, 115 | sylib 208 |
. . . . . . . . . . . . 13
PsMet
|
117 | | 0ss 3972 |
. . . . . . . . . . . . 13
|
118 | 116, 117 | syl6eqss 3655 |
. . . . . . . . . . . 12
PsMet
|
119 | | respreima 6344 |
. . . . . . . . . . . . . 14
|
120 | 104, 45, 46, 119 | 4syl 19 |
. . . . . . . . . . . . 13
PsMet
|
121 | | simpr 477 |
. . . . . . . . . . . . . 14
PsMet
|
122 | | simpllr 799 |
. . . . . . . . . . . . . . 15
PsMet
|
123 | 122 | elpwid 4170 |
. . . . . . . . . . . . . 14
PsMet
|
124 | 121, 123 | eqsstr3d 3640 |
. . . . . . . . . . . . 13
PsMet
|
125 | 120, 124 | eqsstr3d 3640 |
. . . . . . . . . . . 12
PsMet
|
126 | 118, 125 | unssd 3789 |
. . . . . . . . . . 11
PsMet
|
127 | | ssundif 4052 |
. . . . . . . . . . . 12
|
128 | | difcom 4053 |
. . . . . . . . . . . 12
|
129 | | difdif2 3884 |
. . . . . . . . . . . . 13
|
130 | 129 | sseq1i 3629 |
. . . . . . . . . . . 12
|
131 | 127, 128,
130 | 3bitri 286 |
. . . . . . . . . . 11
|
132 | 126, 131 | sylibr 224 |
. . . . . . . . . 10
PsMet
|
133 | | sseq1 3626 |
. . . . . . . . . . 11
|
134 | 133 | rspcev 3309 |
. . . . . . . . . 10
|
135 | 109, 132,
134 | syl2anc 693 |
. . . . . . . . 9
PsMet
|
136 | | elin 3796 |
. . . . . . . . . . . . . 14
|
137 | | vex 3203 |
. . . . . . . . . . . . . . . 16
|
138 | 6 | elrnmpt 5372 |
. . . . . . . . . . . . . . . 16
|
139 | 137, 138 | ax-mp 5 |
. . . . . . . . . . . . . . 15
|
140 | 139 | anbi1i 731 |
. . . . . . . . . . . . . 14
|
141 | | ancom 466 |
. . . . . . . . . . . . . 14
|
142 | 136, 140,
141 | 3bitri 286 |
. . . . . . . . . . . . 13
|
143 | 142 | exbii 1774 |
. . . . . . . . . . . 12
|
144 | | n0 3931 |
. . . . . . . . . . . 12
|
145 | | df-rex 2918 |
. . . . . . . . . . . 12
|
146 | 143, 144,
145 | 3bitr4i 292 |
. . . . . . . . . . 11
|
147 | 146 | biimpi 206 |
. . . . . . . . . 10
|
148 | 147 | ad2antll 765 |
. . . . . . . . 9
PsMet
|
149 | 135, 148 | r19.29vva 3081 |
. . . . . . . 8
PsMet
|
150 | 82 | adantr 481 |
. . . . . . . . 9
PsMet
|
151 | 44 | adantr 481 |
. . . . . . . . 9
PsMet
PsMet |
152 | | metuel 22369 |
. . . . . . . . 9
PsMet
metUnif
|
153 | 150, 151,
152 | syl2anc 693 |
. . . . . . . 8
PsMet
metUnif
|
154 | 97, 149, 153 | mpbir2and 957 |
. . . . . . 7
PsMet
metUnif |
155 | | indir 3875 |
. . . . . . . . 9
|
156 | | incom 3805 |
. . . . . . . . . . 11
|
157 | | disjdif 4040 |
. . . . . . . . . . 11
|
158 | 156, 157 | eqtr3i 2646 |
. . . . . . . . . 10
|
159 | 158 | uneq2i 3764 |
. . . . . . . . 9
|
160 | | un0 3967 |
. . . . . . . . 9
|
161 | 155, 159,
160 | 3eqtri 2648 |
. . . . . . . 8
|
162 | | df-ss 3588 |
. . . . . . . . 9
|
163 | 91, 162 | sylib 208 |
. . . . . . . 8
PsMet
|
164 | 161, 163 | syl5req 2669 |
. . . . . . 7
PsMet
|
165 | | ineq1 3807 |
. . . . . . . . 9
|
166 | 165 | eqeq2d 2632 |
. . . . . . . 8
|
167 | 166 | rspcev 3309 |
. . . . . . 7
metUnif
metUnif |
168 | 154, 164,
167 | syl2anc 693 |
. . . . . 6
PsMet
metUnif |
169 | 89, 168 | impbida 877 |
. . . . 5
PsMet
metUnif
|
170 | | eqid 2622 |
. . . . . . 7
metUnif metUnif |
171 | 170 | elrnmpt 5372 |
. . . . . 6
metUnif
metUnif |
172 | 23, 171 | ax-mp 5 |
. . . . 5
metUnif
metUnif |
173 | | pweq 4161 |
. . . . . . . 8
|
174 | 173 | ineq2d 3814 |
. . . . . . 7
|
175 | 174 | neeq1d 2853 |
. . . . . 6
|
176 | 175 | elrab 3363 |
. . . . 5
|
177 | 169, 172,
176 | 3bitr4g 303 |
. . . 4
PsMet
metUnif
|
178 | 177 | eqrdv 2620 |
. . 3
PsMet
metUnif
|
179 | 19, 178 | eqtrd 2656 |
. 2
PsMet
metUnif ↾t
|
180 | 11, 13, 179 | 3eqtr4rd 2667 |
1
PsMet
metUnif ↾t metUnif |