Step Hyp Ref
Expression 1 ssn0 3818 . . . . . . . . 9
2 xpnz 5431 . . . . . . . . . . 11
3 2 biimpri 206 . . . . . . . . . 10
4 3 simprd 463 . . . . . . . . 9
5 1 , 4 syl 16 . . . . . . . 8
6 dmxp 5226 . . . . . . . . . 10
7 dmss 5207 . . . . . . . . . . 11
8 sseq2 3525 . . . . . . . . . . 11
9 7 , 8 syl5ib 219 . . . . . . . . . 10
10 6 , 9 syl 16 . . . . . . . . 9
11 10 impcom 430 . . . . . . . 8
12 5 , 11 syldan 470 . . . . . . 7
13 relxp 5115 . . . . . . . . . . 11
14 relss 5095 . . . . . . . . . . 11
15 13 , 14 mpi 17 . . . . . . . . . 10
16 reldm0 5225 . . . . . . . . . 10
17 15 , 16 syl 16 . . . . . . . . 9
18 17 necon3bid 2715 . . . . . . . 8
19 18 biimpa 484 . . . . . . 7
20 12 , 19 jca 532 . . . . . 6
21 df-fr 4843 . . . . . . 7
22 vex 3112 . . . . . . . . 9
23 22 dmex 6733 . . . . . . . 8
24 sseq1 3524 . . . . . . . . . 10
25 neeq1 2738 . . . . . . . . . 10
26 24 , 25 anbi12d 710 . . . . . . . . 9
27 raleq 3054 . . . . . . . . . 10
28 27 rexeqbi1dv 3063 . . . . . . . . 9
29 26 , 28 imbi12d 320 . . . . . . . 8
30 23 , 29 spcv 3200 . . . . . . 7
31 21 , 30 sylbi 195 . . . . . 6
32 20 , 31 syl5 32 . . . . 5
33 32 adantr 465 . . . 4
34 imassrn 5353 . . . . . . . . . . . . . . 15
35 xpeq0 5432 . . . . . . . . . . . . . . . . . . . 20
36 35 biimpri 206 . . . . . . . . . . . . . . . . . . 19
37 36 orcs 394 . . . . . . . . . . . . . . . . . 18
38 sseq2 3525 . . . . . . . . . . . . . . . . . . 19
39 ss0 3816 . . . . . . . . . . . . . . . . . . 19
40 38 , 39 syl6bi 228 . . . . . . . . . . . . . . . . . 18
41 37 , 40 syl 16 . . . . . . . . . . . . . . . . 17
42 rneq 5233 . . . . . . . . . . . . . . . . . 18
43 rn0 5259 . . . . . . . . . . . . . . . . . . 19
44 0ss 3814 . . . . . . . . . . . . . . . . . . 19
45 43 , 44 eqsstri 3533 . . . . . . . . . . . . . . . . . 18
46 42 , 45 syl6eqss 3553 . . . . . . . . . . . . . . . . 17
47 41 , 46 syl6 33 . . . . . . . . . . . . . . . 16
48 rnxp 5442 . . . . . . . . . . . . . . . . 17
49 rnss 5236 . . . . . . . . . . . . . . . . . 18
50 sseq2 3525 . . . . . . . . . . . . . . . . . 18
51 49 , 50 syl5ib 219 . . . . . . . . . . . . . . . . 17
52 48 , 51 syl 16 . . . . . . . . . . . . . . . 16
53 47 , 52 pm2.61ine 2770 . . . . . . . . . . . . . . 15
54 34 , 53 syl5ss 3514 . . . . . . . . . . . . . 14
55 vex 3112 . . . . . . . . . . . . . . . 16
56 55 eldm 5205 . . . . . . . . . . . . . . 15
57 vex 3112 . . . . . . . . . . . . . . . . . . 19
58 55 , 57 elimasn 5367 . . . . . . . . . . . . . . . . . 18
59 df-br 4453 . . . . . . . . . . . . . . . . . 18
60 58 , 59 bitr4i 252 . . . . . . . . . . . . . . . . 17
61 ne0i 3790 . . . . . . . . . . . . . . . . 17
62 60 , 61 sylbir 213 . . . . . . . . . . . . . . . 16
63 62 exlimiv 1722 . . . . . . . . . . . . . . 15
64 56 , 63 sylbi 195 . . . . . . . . . . . . . 14
65 df-fr 4843 . . . . . . . . . . . . . . 15
66 imaexg 6737 . . . . . . . . . . . . . . . . 17
67 22 , 66 ax-mp 5 . . . . . . . . . . . . . . . 16
68 sseq1 3524 . . . . . . . . . . . . . . . . . 18
69 neeq1 2738 . . . . . . . . . . . . . . . . . 18
70 68 , 69 anbi12d 710 . . . . . . . . . . . . . . . . 17
71 raleq 3054 . . . . . . . . . . . . . . . . . 18
72 71 rexeqbi1dv 3063 . . . . . . . . . . . . . . . . 17
73 70 , 72 imbi12d 320 . . . . . . . . . . . . . . . 16
74 67 , 73 spcv 3200 . . . . . . . . . . . . . . 15
75 65 , 74 sylbi 195 . . . . . . . . . . . . . 14
76 54 , 64 , 75 syl2ani 656 . . . . . . . . . . . . 13
77 1stdm 6847 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
78 breq1 4455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
79 78 notbid 294 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
80 79 rspccv 3207 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
81 77 , 80 syl5 32 . . . . . . . . . . . . . . . . . . . . . . . . . 26
82 81 expd 436 . . . . . . . . . . . . . . . . . . . . . . . . 25
83 82 impcom 430 . . . . . . . . . . . . . . . . . . . . . . . 24
84 83 adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23
85 elrel 5110 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
86 85 ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . 26
87 86 adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25
88 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
89 55 , 88 elimasn 5367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
90 breq1 4455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
91 90 notbid 294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
92 91 rspccv 3207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
93 89 , 92 syl5bir 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
94 93 adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
95 opeq1 4217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
96 95 eleq1d 2526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
97 96 imbi1d 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
98 94 , 97 syl5ibr 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
99 98 com3l 81 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
100 eleq1 2529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
101 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
102 101 , 88 op1std 6810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
103 102 eqeq1d 2459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
104 101 , 88 op2ndd 6811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
105 104 breq1d 4462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
106 105 notbid 294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
107 103 , 106 imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
108 100 , 107 imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
109 99 , 108 syl5ibr 221 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
110 109 exlimivv 1723 . . . . . . . . . . . . . . . . . . . . . . . . . 26
111 110 com3l 81 . . . . . . . . . . . . . . . . . . . . . . . . 25
112 87 , 111 mpdd 40 . . . . . . . . . . . . . . . . . . . . . . . 24
113 112 adantlr 714 . . . . . . . . . . . . . . . . . . . . . . 23
114 84 , 113 jcad 533 . . . . . . . . . . . . . . . . . . . . . 22
115 114 ralrimiv 2869 . . . . . . . . . . . . . . . . . . . . 21
116 115 ex 434 . . . . . . . . . . . . . . . . . . . 20
117 15 , 116 sylan 471 . . . . . . . . . . . . . . . . . . 19
118 olc 384 . . . . . . . . . . . . . . . . . . . 20
119 118 ralimi 2850 . . . . . . . . . . . . . . . . . . 19
120 117 , 119 syl6 33 . . . . . . . . . . . . . . . . . 18
121 ianor 488 . . . . . . . . . . . . . . . . . . . . 21
122 vex 3112 . . . . . . . . . . . . . . . . . . . . . 22
123 opex 4716 . . . . . . . . . . . . . . . . . . . . . 22
124 eleq1 2529 . . . . . . . . . . . . . . . . . . . . . . . 24
125 124 anbi1d 704 . . . . . . . . . . . . . . . . . . . . . . 23
126 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . . 25
127 126 breq1d 4462 . . . . . . . . . . . . . . . . . . . . . . . 24
128 126 eqeq1d 2459 . . . . . . . . . . . . . . . . . . . . . . . . 25
129 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . . . 26
130 129 breq1d 4462 . . . . . . . . . . . . . . . . . . . . . . . . 25
131 128 , 130 anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . 24
132 127 , 131 orbi12d 709 . . . . . . . . . . . . . . . . . . . . . . 23
133 125 , 132 anbi12d 710 . . . . . . . . . . . . . . . . . . . . . 22
134 eleq1 2529 . . . . . . . . . . . . . . . . . . . . . . . 24
135 134 anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . 23
136 55 , 57 op1std 6810 . . . . . . . . . . . . . . . . . . . . . . . . 25
137 136 breq2d 4464 . . . . . . . . . . . . . . . . . . . . . . . 24
138 136 eqeq2d 2471 . . . . . . . . . . . . . . . . . . . . . . . . 25
139 55 , 57 op2ndd 6811 . . . . . . . . . . . . . . . . . . . . . . . . . 26
140 139 breq2d 4464 . . . . . . . . . . . . . . . . . . . . . . . . 25
141 138 , 140 anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . 24
142 137 , 141 orbi12d 709 . . . . . . . . . . . . . . . . . . . . . . 23
143 135 , 142 anbi12d 710 . . . . . . . . . . . . . . . . . . . . . 22
144 frxp.1 . . . . . . . . . . . . . . . . . . . . . 22
145 122 , 123 ,
133 , 143 , 144 brab 4775 . . . . . . . . . . . . . . . . . . . . 21
146 121 , 145 xchnxbir 309 . . . . . . . . . . . . . . . . . . . 20
147 ioran 490 . . . . . . . . . . . . . . . . . . . . . 22
148 ianor 488 . . . . . . . . . . . . . . . . . . . . . . . 24
149 pm4.62 419 . . . . . . . . . . . . . . . . . . . . . . . 24
150 148 , 149 bitr4i 252 . . . . . . . . . . . . . . . . . . . . . . 23
151 150 anbi2i 694 . . . . . . . . . . . . . . . . . . . . . 22
152 147 , 151 bitri 249 . . . . . . . . . . . . . . . . . . . . 21
153 152 orbi2i 519 . . . . . . . . . . . . . . . . . . . 20
154 146 , 153 bitri 249 . . . . . . . . . . . . . . . . . . 19
155 154 ralbii 2888 . . . . . . . . . . . . . . . . . 18
156 120 , 155 syl6ibr 227 . . . . . . . . . . . . . . . . 17
157 156 reximdv 2931 . . . . . . . . . . . . . . . 16
158 157 ex 434 . . . . . . . . . . . . . . 15
159 158 com23 78 . . . . . . . . . . . . . 14
160 159 adantr 465 . . . . . . . . . . . . 13
161 76 , 160 sylcom 29 . . . . . . . . . . . 12
162 161 impl 620 . . . . . . . . . . 11
163 162 expimpd 603 . . . . . . . . . 10
164 163 3adant3 1016 . . . . . . . . 9
165 resss 5302 . . . . . . . . . 10
166 df-rex 2813 . . . . . . . . . . . . 13
167 eqid 2457 . . . . . . . . . . . . . . . 16
168 eqeq1 2461 . . . . . . . . . . . . . . . . . 18
169 breq2 4456 . . . . . . . . . . . . . . . . . . . . 21
170 169 notbid 294 . . . . . . . . . . . . . . . . . . . 20
171 170 ralbidv 2896 . . . . . . . . . . . . . . . . . . 19
172 171 anbi2d 703 . . . . . . . . . . . . . . . . . 18
173 168 , 172 anbi12d 710 . . . . . . . . . . . . . . . . 17
174 123 , 173 spcev 3201 . . . . . . . . . . . . . . . 16
175 167 , 174 mpan 670 . . . . . . . . . . . . . . 15
176 58 , 175 sylanb 472 . . . . . . . . . . . . . 14
177 176 eximi 1656 . . . . . . . . . . . . 13
178 166 , 177 sylbi 195 . . . . . . . . . . . 12
179 excom 1849 . . . . . . . . . . . 12
180 178 , 179 sylib 196 . . . . . . . . . . 11
181 df-rex 2813 . . . . . . . . . . . 12
182 55 elsnres 5315 . . . . . . . . . . . . . . 15
183 182 anbi1i 695 . . . . . . . . . . . . . 14
184 19.41v 1771 . . . . . . . . . . . . . 14
185 anass 649 . . . . . . . . . . . . . . 15
