Step | Hyp | Ref
| Expression |
1 | | simp-4r 807 |
. . . 4
PsMet
PsMet |
2 | | simplr 792 |
. . . . . 6
PsMet
|
3 | 2 | rphalfcld 11884 |
. . . . 5
PsMet
|
4 | | eqidd 2623 |
. . . . 5
PsMet
|
5 | | oveq2 6658 |
. . . . . . . 8
|
6 | 5 | imaeq2d 5466 |
. . . . . . 7
|
7 | 6 | eqeq2d 2632 |
. . . . . 6
|
8 | 7 | rspcev 3309 |
. . . . 5
|
9 | 3, 4, 8 | syl2anc 693 |
. . . 4
PsMet
|
10 | | metust.1 |
. . . . . . 7
|
11 | | oveq2 6658 |
. . . . . . . . . 10
|
12 | 11 | imaeq2d 5466 |
. . . . . . . . 9
|
13 | 12 | cbvmptv 4750 |
. . . . . . . 8
|
14 | 13 | rneqi 5352 |
. . . . . . 7
|
15 | 10, 14 | eqtri 2644 |
. . . . . 6
|
16 | 15 | metustel 22355 |
. . . . 5
PsMet
|
17 | 16 | biimpar 502 |
. . . 4
PsMet
|
18 | 1, 9, 17 | syl2anc 693 |
. . 3
PsMet
|
19 | | relco 5633 |
. . . . 5
|
20 | 19 | a1i 11 |
. . . 4
PsMet
|
21 | | cossxp 5658 |
. . . . . . . . . 10
|
22 | | cnvimass 5485 |
. . . . . . . . . . . . . 14
|
23 | | psmetf 22111 |
. . . . . . . . . . . . . . 15
PsMet
|
24 | | fdm 6051 |
. . . . . . . . . . . . . . 15
|
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . 14
PsMet
|
26 | 22, 25 | syl5sseq 3653 |
. . . . . . . . . . . . 13
PsMet
|
27 | | dmss 5323 |
. . . . . . . . . . . . . 14
|
28 | | rnss 5354 |
. . . . . . . . . . . . . 14
|
29 | | xpss12 5225 |
. . . . . . . . . . . . . 14
|
30 | 27, 28, 29 | syl2anc 693 |
. . . . . . . . . . . . 13
|
31 | 26, 30 | syl 17 |
. . . . . . . . . . . 12
PsMet
|
32 | 31 | adantl 482 |
. . . . . . . . . . 11
PsMet
|
33 | | dmxp 5344 |
. . . . . . . . . . . . 13
|
34 | | rnxp 5564 |
. . . . . . . . . . . . 13
|
35 | 33, 34 | xpeq12d 5140 |
. . . . . . . . . . . 12
|
36 | 35 | adantr 481 |
. . . . . . . . . . 11
PsMet
|
37 | 32, 36 | sseqtrd 3641 |
. . . . . . . . . 10
PsMet
|
38 | 21, 37 | syl5ss 3614 |
. . . . . . . . 9
PsMet
|
39 | 38 | ad3antrrr 766 |
. . . . . . . 8
PsMet
|
40 | 39 | sselda 3603 |
. . . . . . 7
PsMet
|
41 | | opelxp 5146 |
. . . . . . 7
|
42 | 40, 41 | sylib 208 |
. . . . . 6
PsMet
|
43 | | simpll 790 |
. . . . . . 7
PsMet
PsMet
|
44 | | simprl 794 |
. . . . . . 7
PsMet
|
45 | | simprr 796 |
. . . . . . 7
PsMet
|
46 | | simplr 792 |
. . . . . . 7
PsMet
|
47 | | simplll 798 |
. . . . . . . . . . . . . . 15
PsMet
PsMet
|
48 | 47 | simp1d 1073 |
. . . . . . . . . . . . . 14
PsMet
PsMet
|
49 | 48, 1 | syl 17 |
. . . . . . . . . . . . 13
PsMet
PsMet |
50 | 48, 2 | syl 17 |
. . . . . . . . . . . . 13
PsMet
|
51 | 49, 50 | jca 554 |
. . . . . . . . . . . 12
PsMet
PsMet
|
52 | 47 | simp2d 1074 |
. . . . . . . . . . . 12
PsMet
|
53 | 47 | simp3d 1075 |
. . . . . . . . . . . 12
PsMet
|
54 | 51, 52, 53 | 3jca 1242 |
. . . . . . . . . . 11
PsMet
PsMet
|
55 | | simplr 792 |
. . . . . . . . . . 11
PsMet
|
56 | | simprl 794 |
. . . . . . . . . . 11
PsMet
|
57 | | simprr 796 |
. . . . . . . . . . 11
PsMet
|
58 | | simpll 790 |
. . . . . . . . . . . . . . 15
PsMet
PsMet
|
59 | 58 | simp1d 1073 |
. . . . . . . . . . . . . 14
PsMet
PsMet
|
60 | 59 | simpld 475 |
. . . . . . . . . . . . 13
PsMet
PsMet |
61 | | ffun 6048 |
. . . . . . . . . . . . . 14
|
62 | 23, 61 | syl 17 |
. . . . . . . . . . . . 13
PsMet
|
63 | 60, 62 | syl 17 |
. . . . . . . . . . . 12
PsMet
|
64 | 58 | simp2d 1074 |
. . . . . . . . . . . . . 14
PsMet
|
65 | 58 | simp3d 1075 |
. . . . . . . . . . . . . 14
PsMet
|
66 | 64, 65, 41 | sylanbrc 698 |
. . . . . . . . . . . . 13
PsMet
|
67 | 60, 25 | syl 17 |
. . . . . . . . . . . . 13
PsMet
|
68 | 66, 67 | eleqtrrd 2704 |
. . . . . . . . . . . 12
PsMet
|
69 | | 0xr 10086 |
. . . . . . . . . . . . . 14
|
70 | 69 | a1i 11 |
. . . . . . . . . . . . 13
PsMet
|
71 | 59 | simprd 479 |
. . . . . . . . . . . . . 14
PsMet
|
72 | 71 | rpxrd 11873 |
. . . . . . . . . . . . 13
PsMet
|
73 | 60, 23 | syl 17 |
. . . . . . . . . . . . . 14
PsMet
|
74 | 73, 66 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
PsMet
|
75 | | psmetge0 22117 |
. . . . . . . . . . . . . . 15
PsMet
|
76 | 60, 64, 65, 75 | syl3anc 1326 |
. . . . . . . . . . . . . 14
PsMet
|
77 | | df-ov 6653 |
. . . . . . . . . . . . . 14
|
78 | 76, 77 | syl6breq 4694 |
. . . . . . . . . . . . 13
PsMet
|
79 | 77, 74 | syl5eqel 2705 |
. . . . . . . . . . . . . . 15
PsMet
|
80 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . 19
PsMet
|
81 | 71 | rpred 11872 |
. . . . . . . . . . . . . . . . . . . . 21
PsMet
|
82 | 81 | rehalfcld 11279 |
. . . . . . . . . . . . . . . . . . . 20
PsMet
|
83 | 82 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . 19
PsMet
|
84 | | df-ov 6653 |
. . . . . . . . . . . . . . . . . . . 20
|
85 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . . 23
PsMet
|
86 | | opelxp 5146 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
87 | 64, 85, 86 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . . . . 22
PsMet
|
88 | 87, 67 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . . . . . . 21
PsMet
|
89 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . 22
PsMet
|
90 | | df-br 4654 |
. . . . . . . . . . . . . . . . . . . . . 22
|
91 | 89, 90 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . 21
PsMet
|
92 | | fvimacnv 6332 |
. . . . . . . . . . . . . . . . . . . . . 22
|
93 | 92 | biimpar 502 |
. . . . . . . . . . . . . . . . . . . . 21
|
94 | 63, 88, 91, 93 | syl21anc 1325 |
. . . . . . . . . . . . . . . . . . . 20
PsMet
|
95 | 84, 94 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . . . 19
PsMet
|
96 | | elico2 12237 |
. . . . . . . . . . . . . . . . . . . . 21
|
97 | 96 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . 20
|
98 | 97 | simp1d 1073 |
. . . . . . . . . . . . . . . . . . 19
|
99 | 80, 83, 95, 98 | syl21anc 1325 |
. . . . . . . . . . . . . . . . . 18
PsMet
|
100 | | df-ov 6653 |
. . . . . . . . . . . . . . . . . . . 20
|
101 | | opelxp 5146 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
102 | 85, 65, 101 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . . . . 22
PsMet
|
103 | 102, 67 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . . . . . . 21
PsMet
|
104 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . 22
PsMet
|
105 | | df-br 4654 |
. . . . . . . . . . . . . . . . . . . . . 22
|
106 | 104, 105 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . 21
PsMet
|
107 | | fvimacnv 6332 |
. . . . . . . . . . . . . . . . . . . . . 22
|
108 | 107 | biimpar 502 |
. . . . . . . . . . . . . . . . . . . . 21
|
109 | 63, 103, 106, 108 | syl21anc 1325 |
. . . . . . . . . . . . . . . . . . . 20
PsMet
|
110 | 100, 109 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . . . 19
PsMet
|
111 | | elico2 12237 |
. . . . . . . . . . . . . . . . . . . . 21
|
112 | 111 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . 20
|
113 | 112 | simp1d 1073 |
. . . . . . . . . . . . . . . . . . 19
|
114 | 80, 83, 110, 113 | syl21anc 1325 |
. . . . . . . . . . . . . . . . . 18
PsMet
|
115 | | rexadd 12063 |
. . . . . . . . . . . . . . . . . 18
|
116 | 99, 114, 115 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
PsMet
|
117 | 99, 114 | readdcld 10069 |
. . . . . . . . . . . . . . . . 17
PsMet
|
118 | 116, 117 | eqeltrd 2701 |
. . . . . . . . . . . . . . . 16
PsMet
|
119 | 118 | rexrd 10089 |
. . . . . . . . . . . . . . 15
PsMet
|
120 | | psmettri 22116 |
. . . . . . . . . . . . . . . 16
PsMet
|
121 | 60, 64, 65, 85, 120 | syl13anc 1328 |
. . . . . . . . . . . . . . 15
PsMet
|
122 | 97 | simp3d 1075 |
. . . . . . . . . . . . . . . . . 18
|
123 | 80, 83, 95, 122 | syl21anc 1325 |
. . . . . . . . . . . . . . . . 17
PsMet
|
124 | 112 | simp3d 1075 |
. . . . . . . . . . . . . . . . . 18
|
125 | 80, 83, 110, 124 | syl21anc 1325 |
. . . . . . . . . . . . . . . . 17
PsMet
|
126 | 99, 114, 81, 123, 125 | lt2halvesd 11280 |
. . . . . . . . . . . . . . . 16
PsMet
|
127 | 116, 126 | eqbrtrd 4675 |
. . . . . . . . . . . . . . 15
PsMet
|
128 | 79, 119, 72, 121, 127 | xrlelttrd 11991 |
. . . . . . . . . . . . . 14
PsMet
|
129 | 77, 128 | syl5eqbrr 4689 |
. . . . . . . . . . . . 13
PsMet
|
130 | | elico1 12218 |
. . . . . . . . . . . . . 14
|
131 | 130 | biimpar 502 |
. . . . . . . . . . . . 13
|
132 | 70, 72, 74, 78, 129, 131 | syl23anc 1333 |
. . . . . . . . . . . 12
PsMet
|
133 | | fvimacnv 6332 |
. . . . . . . . . . . . . 14
|
134 | 133 | biimpa 501 |
. . . . . . . . . . . . 13
|
135 | | df-br 4654 |
. . . . . . . . . . . . 13
|
136 | 134, 135 | sylibr 224 |
. . . . . . . . . . . 12
|
137 | 63, 68, 132, 136 | syl21anc 1325 |
. . . . . . . . . . 11
PsMet
|
138 | 54, 55, 56, 57, 137 | syl22anc 1327 |
. . . . . . . . . 10
PsMet
|
139 | 48 | simprd 479 |
. . . . . . . . . . 11
PsMet
|
140 | 139 | breqd 4664 |
. . . . . . . . . 10
PsMet
|
141 | 138, 140 | mpbird 247 |
. . . . . . . . 9
PsMet
|
142 | | simpr 477 |
. . . . . . . . . . . . 13
PsMet
|
143 | | df-br 4654 |
. . . . . . . . . . . . 13
|
144 | 142, 143 | sylibr 224 |
. . . . . . . . . . . 12
PsMet
|
145 | | vex 3203 |
. . . . . . . . . . . . 13
|
146 | | vex 3203 |
. . . . . . . . . . . . 13
|
147 | 145, 146 | brco 5292 |
. . . . . . . . . . . 12
|
148 | 144, 147 | sylib 208 |
. . . . . . . . . . 11
PsMet
|
149 | 26 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
PsMet
|
150 | 149, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
PsMet
|
151 | 34 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
PsMet
|
152 | 150, 151 | sseqtrd 3641 |
. . . . . . . . . . . . . . . . . . . 20
PsMet
|
153 | 152 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
PsMet
|
154 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . 21
|
155 | 145, 154 | brelrn 5356 |
. . . . . . . . . . . . . . . . . . . 20
|
156 | 155 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
PsMet
|
157 | 153, 156 | sseldd 3604 |
. . . . . . . . . . . . . . . . . 18
PsMet
|
158 | 157 | adantrr 753 |
. . . . . . . . . . . . . . . . 17
PsMet
|
159 | 158 | ex 450 |
. . . . . . . . . . . . . . . 16
PsMet
|
160 | 159 | ancrd 577 |
. . . . . . . . . . . . . . 15
PsMet
|
161 | 160 | eximdv 1846 |
. . . . . . . . . . . . . 14
PsMet
|
162 | 161 | ad3antrrr 766 |
. . . . . . . . . . . . 13
PsMet
|
163 | 162 | 3ad2ant1 1082 |
. . . . . . . . . . . 12
PsMet
|
164 | 163 | adantr 481 |
. . . . . . . . . . 11
PsMet
|
165 | 148, 164 | mpd 15 |
. . . . . . . . . 10
PsMet
|
166 | | df-rex 2918 |
. . . . . . . . . 10
|
167 | 165, 166 | sylibr 224 |
. . . . . . . . 9
PsMet
|
168 | 141, 167 | r19.29a 3078 |
. . . . . . . 8
PsMet
|
169 | | df-br 4654 |
. . . . . . . 8
|
170 | 168, 169 | sylib 208 |
. . . . . . 7
PsMet
|
171 | 43, 44, 45, 46, 170 | syl31anc 1329 |
. . . . . 6
PsMet
|
172 | 42, 171 | mpdan 702 |
. . . . 5
PsMet
|
173 | 172 | ex 450 |
. . . 4
PsMet
|
174 | 20, 173 | relssdv 5212 |
. . 3
PsMet
|
175 | | id 22 |
. . . . . 6
|
176 | 175, 175 | coeq12d 5286 |
. . . . 5
|
177 | 176 | sseq1d 3632 |
. . . 4
|
178 | 177 | rspcev 3309 |
. . 3
|
179 | 18, 174, 178 | syl2anc 693 |
. 2
PsMet
|
180 | 10 | metustel 22355 |
. . . 4
PsMet
|
181 | 180 | adantl 482 |
. . 3
PsMet
|
182 | 181 | biimpa 501 |
. 2
PsMet
|
183 | 179, 182 | r19.29a 3078 |
1
PsMet
|