Step | Hyp | Ref
| Expression |
1 | | sdc.8 |
. 2
|
2 | | sdc.10 |
. . . . . 6
|
3 | | sdc.1 |
. . . . . . . 8
|
4 | | fvex 6201 |
. . . . . . . 8
|
5 | 3, 4 | eqeltri 2697 |
. . . . . . 7
|
6 | | simpl 473 |
. . . . . . . . . . 11
|
7 | | sdc.6 |
. . . . . . . . . . . 12
|
8 | | ovex 6678 |
. . . . . . . . . . . 12
|
9 | | elmapg 7870 |
. . . . . . . . . . . 12
|
10 | 7, 8, 9 | sylancl 694 |
. . . . . . . . . . 11
|
11 | 6, 10 | syl5ibr 236 |
. . . . . . . . . 10
|
12 | 11 | abssdv 3676 |
. . . . . . . . 9
|
13 | | ovex 6678 |
. . . . . . . . 9
|
14 | | ssexg 4804 |
. . . . . . . . 9
|
15 | 12, 13, 14 | sylancl 694 |
. . . . . . . 8
|
16 | 15 | ralrimivw 2967 |
. . . . . . 7
|
17 | | abrexex2g 7144 |
. . . . . . 7
|
18 | 5, 16, 17 | sylancr 695 |
. . . . . 6
|
19 | 2, 18 | syl5eqel 2705 |
. . . . 5
|
20 | 19 | adantr 481 |
. . . 4
|
21 | | sdc.7 |
. . . . . . . . 9
|
22 | 21 | adantr 481 |
. . . . . . . 8
|
23 | | uzid 11702 |
. . . . . . . 8
|
24 | 22, 23 | syl 17 |
. . . . . . 7
|
25 | 24, 3 | syl6eleqr 2712 |
. . . . . 6
|
26 | | simprl 794 |
. . . . . . 7
|
27 | | fzsn 12383 |
. . . . . . . . 9
|
28 | 22, 27 | syl 17 |
. . . . . . . 8
|
29 | 28 | feq2d 6031 |
. . . . . . 7
|
30 | 26, 29 | mpbird 247 |
. . . . . 6
|
31 | | simprr 796 |
. . . . . 6
|
32 | | oveq2 6658 |
. . . . . . . . 9
|
33 | 32 | feq2d 6031 |
. . . . . . . 8
|
34 | | sdc.3 |
. . . . . . . 8
|
35 | 33, 34 | anbi12d 747 |
. . . . . . 7
|
36 | 35 | rspcev 3309 |
. . . . . 6
|
37 | 25, 30, 31, 36 | syl12anc 1324 |
. . . . 5
|
38 | 2 | abeq2i 2735 |
. . . . 5
|
39 | 37, 38 | sylibr 224 |
. . . 4
|
40 | 3 | peano2uzs 11742 |
. . . . . . . . . . . . . . . . 17
|
41 | 40 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
|
42 | | simpr1 1067 |
. . . . . . . . . . . . . . . 16
|
43 | | simpr3 1069 |
. . . . . . . . . . . . . . . . 17
|
44 | | vex 3203 |
. . . . . . . . . . . . . . . . . . 19
|
45 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . 19
|
46 | | sdc.5 |
. . . . . . . . . . . . . . . . . . . 20
|
47 | 46 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
48 | 44, 45, 47 | sbc2iedv 3506 |
. . . . . . . . . . . . . . . . . 18
|
49 | 48 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
50 | 43, 49 | mpbird 247 |
. . . . . . . . . . . . . . . 16
|
51 | | nfv 1843 |
. . . . . . . . . . . . . . . . . 18
|
52 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . 19
|
53 | | nfsbc1v 3455 |
. . . . . . . . . . . . . . . . . . 19
|
54 | 52, 53 | nfsbc 3457 |
. . . . . . . . . . . . . . . . . 18
|
55 | 51, 54 | nfan 1828 |
. . . . . . . . . . . . . . . . 17
|
56 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
|
57 | 56 | feq2d 6031 |
. . . . . . . . . . . . . . . . . 18
|
58 | | sbceq1a 3446 |
. . . . . . . . . . . . . . . . . . 19
|
59 | 58 | sbcbidv 3490 |
. . . . . . . . . . . . . . . . . 18
|
60 | 57, 59 | anbi12d 747 |
. . . . . . . . . . . . . . . . 17
|
61 | 55, 60 | rspce 3304 |
. . . . . . . . . . . . . . . 16
|
62 | 41, 42, 50, 61 | syl12anc 1324 |
. . . . . . . . . . . . . . 15
|
63 | 2 | eleq2i 2693 |
. . . . . . . . . . . . . . . 16
|
64 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . 18
|
65 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . 19
|
66 | | nfsbc1v 3455 |
. . . . . . . . . . . . . . . . . . 19
|
67 | 65, 66 | nfan 1828 |
. . . . . . . . . . . . . . . . . 18
|
68 | 64, 67 | nfrex 3007 |
. . . . . . . . . . . . . . . . 17
|
69 | | feq1 6026 |
. . . . . . . . . . . . . . . . . . 19
|
70 | | sbceq1a 3446 |
. . . . . . . . . . . . . . . . . . 19
|
71 | 69, 70 | anbi12d 747 |
. . . . . . . . . . . . . . . . . 18
|
72 | 71 | rexbidv 3052 |
. . . . . . . . . . . . . . . . 17
|
73 | 68, 44, 72 | elabf 3349 |
. . . . . . . . . . . . . . . 16
|
74 | 63, 73 | bitri 264 |
. . . . . . . . . . . . . . 15
|
75 | 62, 74 | sylibr 224 |
. . . . . . . . . . . . . 14
|
76 | 75 | ex 450 |
. . . . . . . . . . . . 13
|
77 | 76 | rexlimdva 3031 |
. . . . . . . . . . . 12
|
78 | 77 | abssdv 3676 |
. . . . . . . . . . 11
|
79 | 78 | ad2antrr 762 |
. . . . . . . . . 10
|
80 | 19 | ad2antrr 762 |
. . . . . . . . . . 11
|
81 | | elpw2g 4827 |
. . . . . . . . . . 11
|
82 | 80, 81 | syl 17 |
. . . . . . . . . 10
|
83 | 79, 82 | mpbird 247 |
. . . . . . . . 9
|
84 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
|
85 | 84 | feq2d 6031 |
. . . . . . . . . . . . . . . . . 18
|
86 | | sdc.4 |
. . . . . . . . . . . . . . . . . 18
|
87 | 85, 86 | anbi12d 747 |
. . . . . . . . . . . . . . . . 17
|
88 | 87 | cbvrexv 3172 |
. . . . . . . . . . . . . . . 16
|
89 | | sdc.9 |
. . . . . . . . . . . . . . . . . 18
|
90 | 89 | reximdva 3017 |
. . . . . . . . . . . . . . . . 17
|
91 | | rexcom4 3225 |
. . . . . . . . . . . . . . . . 17
|
92 | 90, 91 | syl6ib 241 |
. . . . . . . . . . . . . . . 16
|
93 | 88, 92 | syl5bi 232 |
. . . . . . . . . . . . . . 15
|
94 | 93 | ss2abdv 3675 |
. . . . . . . . . . . . . 14
|
95 | 2, 94 | syl5eqss 3649 |
. . . . . . . . . . . . 13
|
96 | 95 | sselda 3603 |
. . . . . . . . . . . 12
|
97 | | vex 3203 |
. . . . . . . . . . . . 13
|
98 | | eqeq1 2626 |
. . . . . . . . . . . . . . . 16
|
99 | 98 | 3anbi2d 1404 |
. . . . . . . . . . . . . . 15
|
100 | 99 | rexbidv 3052 |
. . . . . . . . . . . . . 14
|
101 | 100 | exbidv 1850 |
. . . . . . . . . . . . 13
|
102 | 97, 101 | elab 3350 |
. . . . . . . . . . . 12
|
103 | 96, 102 | sylib 208 |
. . . . . . . . . . 11
|
104 | | abn0 3954 |
. . . . . . . . . . 11
|
105 | 103, 104 | sylibr 224 |
. . . . . . . . . 10
|
106 | 105 | adantlr 751 |
. . . . . . . . 9
|
107 | | eldifsn 4317 |
. . . . . . . . 9
|
108 | 83, 106, 107 | sylanbrc 698 |
. . . . . . . 8
|
109 | 108 | adantrl 752 |
. . . . . . 7
|
110 | 109 | ralrimivva 2971 |
. . . . . 6
|
111 | | sdc.11 |
. . . . . . 7
|
112 | 111 | fmpt2 7237 |
. . . . . 6
|
113 | 110, 112 | sylib 208 |
. . . . 5
|
114 | 21 | iftrued 4094 |
. . . . . . . . . 10
|
115 | 114 | fveq2d 6195 |
. . . . . . . . 9
|
116 | 115, 3 | syl6eqr 2674 |
. . . . . . . 8
|
117 | 116 | xpeq1d 5138 |
. . . . . . 7
|
118 | 117 | feq2d 6031 |
. . . . . 6
|
119 | 118 | biimpar 502 |
. . . . 5
|
120 | 113, 119 | syldan 487 |
. . . 4
|
121 | | 0z 11388 |
. . . . . 6
|
122 | 121 | elimel 4150 |
. . . . 5
|
123 | | eqid 2622 |
. . . . 5
|
124 | 122, 123 | axdc4uz 12783 |
. . . 4
|
125 | 20, 39, 120, 124 | syl3anc 1326 |
. . 3
|
126 | 22 | iftrued 4094 |
. . . . . . . . . 10
|
127 | 126 | fveq2d 6195 |
. . . . . . . . 9
|
128 | 127, 3 | syl6eqr 2674 |
. . . . . . . 8
|
129 | 128 | feq2d 6031 |
. . . . . . 7
|
130 | 88 | abbii 2739 |
. . . . . . . . 9
|
131 | 2, 130 | eqtri 2644 |
. . . . . . . 8
|
132 | | feq3 6028 |
. . . . . . . 8
|
133 | 131, 132 | ax-mp 5 |
. . . . . . 7
|
134 | 129, 133 | syl6bb 276 |
. . . . . 6
|
135 | 126 | fveq2d 6195 |
. . . . . . 7
|
136 | 135 | eqeq1d 2624 |
. . . . . 6
|
137 | 128 | raleqdv 3144 |
. . . . . 6
|
138 | 134, 136,
137 | 3anbi123d 1399 |
. . . . 5
|
139 | | sdc.2 |
. . . . . . 7
|
140 | 7 | ad2antrr 762 |
. . . . . . 7
|
141 | 21 | ad2antrr 762 |
. . . . . . 7
|
142 | 1 | ad2antrr 762 |
. . . . . . 7
|
143 | | simpll 790 |
. . . . . . . 8
|
144 | 143, 89 | sylan 488 |
. . . . . . 7
|
145 | | nfv 1843 |
. . . . . . . 8
|
146 | | nfcv 2764 |
. . . . . . . . . 10
|
147 | | nfcv 2764 |
. . . . . . . . . 10
|
148 | | nfre1 3005 |
. . . . . . . . . . 11
|
149 | 148 | nfab 2769 |
. . . . . . . . . 10
|
150 | 146, 147,
149 | nff 6041 |
. . . . . . . . 9
|
151 | | nfv 1843 |
. . . . . . . . 9
|
152 | | nfcv 2764 |
. . . . . . . . . . . 12
|
153 | 131, 149 | nfcxfr 2762 |
. . . . . . . . . . . . . 14
|
154 | | nfre1 3005 |
. . . . . . . . . . . . . . 15
|
155 | 154 | nfab 2769 |
. . . . . . . . . . . . . 14
|
156 | 147, 153,
155 | nfmpt2 6724 |
. . . . . . . . . . . . 13
|
157 | 111, 156 | nfcxfr 2762 |
. . . . . . . . . . . 12
|
158 | | nfcv 2764 |
. . . . . . . . . . . 12
|
159 | 152, 157,
158 | nfov 6676 |
. . . . . . . . . . 11
|
160 | 159 | nfel2 2781 |
. . . . . . . . . 10
|
161 | 147, 160 | nfral 2945 |
. . . . . . . . 9
|
162 | 150, 151,
161 | nf3an 1831 |
. . . . . . . 8
|
163 | 145, 162 | nfan 1828 |
. . . . . . 7
|
164 | | simpr1 1067 |
. . . . . . . 8
|
165 | 164, 133 | sylibr 224 |
. . . . . . 7
|
166 | 26 | adantr 481 |
. . . . . . . 8
|
167 | | simpr2 1068 |
. . . . . . . . 9
|
168 | 141, 27 | syl 17 |
. . . . . . . . 9
|
169 | 167, 168 | feq12d 6033 |
. . . . . . . 8
|
170 | 166, 169 | mpbird 247 |
. . . . . . 7
|
171 | | simpr3 1069 |
. . . . . . . 8
|
172 | | oveq1 6657 |
. . . . . . . . . . 11
|
173 | 172 | fveq2d 6195 |
. . . . . . . . . 10
|
174 | | id 22 |
. . . . . . . . . . 11
|
175 | | fveq2 6191 |
. . . . . . . . . . 11
|
176 | 174, 175 | oveq12d 6668 |
. . . . . . . . . 10
|
177 | 173, 176 | eleq12d 2695 |
. . . . . . . . 9
|
178 | 177 | rspccva 3308 |
. . . . . . . 8
|
179 | 171, 178 | sylan 488 |
. . . . . . 7
|
180 | 3, 139, 34, 86, 46, 140, 141, 142, 144, 2, 111, 163, 165, 170, 179 | sdclem2 33538 |
. . . . . 6
|
181 | 180 | ex 450 |
. . . . 5
|
182 | 138, 181 | sylbid 230 |
. . . 4
|
183 | 182 | exlimdv 1861 |
. . 3
|
184 | 125, 183 | mpd 15 |
. 2
|
185 | 1, 184 | exlimddv 1863 |
1
|