Step | Hyp | Ref
| Expression |
1 | | stoweidlem31.14 |
. . 3
|
2 | | fnchoice 39188 |
. . 3
|
3 | 1, 2 | syl 17 |
. 2
|
4 | | vex 3203 |
. . . . 5
|
5 | | stoweidlem31.6 |
. . . . . . 7
|
6 | | stoweidlem31.12 |
. . . . . . . . 9
|
7 | | stoweidlem31.7 |
. . . . . . . . 9
|
8 | 6, 7 | ssexd 4805 |
. . . . . . . 8
|
9 | | mptexg 6484 |
. . . . . . . 8
|
10 | 8, 9 | syl 17 |
. . . . . . 7
|
11 | 5, 10 | syl5eqel 2705 |
. . . . . 6
|
12 | | vex 3203 |
. . . . . 6
|
13 | | coexg 7117 |
. . . . . 6
|
14 | 11, 12, 13 | sylancl 694 |
. . . . 5
|
15 | | coexg 7117 |
. . . . 5
|
16 | 4, 14, 15 | sylancr 695 |
. . . 4
|
17 | 16 | adantr 481 |
. . 3
|
18 | | simprl 794 |
. . . . . 6
|
19 | | stoweidlem31.1 |
. . . . . . . . 9
|
20 | | nfcv 2764 |
. . . . . . . . . . 11
|
21 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
22 | | nfrab1 3122 |
. . . . . . . . . . . . . 14
|
23 | 21, 22 | nfmpt 4746 |
. . . . . . . . . . . . 13
|
24 | 5, 23 | nfcxfr 2762 |
. . . . . . . . . . . 12
|
25 | 24 | nfrn 5368 |
. . . . . . . . . . 11
|
26 | 20, 25 | nffn 5987 |
. . . . . . . . . 10
|
27 | | nfv 1843 |
. . . . . . . . . . 11
|
28 | 25, 27 | nfral 2945 |
. . . . . . . . . 10
|
29 | 26, 28 | nfan 1828 |
. . . . . . . . 9
|
30 | 19, 29 | nfan 1828 |
. . . . . . . 8
|
31 | | fvelrnb 6243 |
. . . . . . . . . . . . 13
|
32 | 18, 31 | syl 17 |
. . . . . . . . . . . 12
|
33 | 32 | biimpa 501 |
. . . . . . . . . . 11
|
34 | | nfv 1843 |
. . . . . . . . . . . . . 14
|
35 | | nfv 1843 |
. . . . . . . . . . . . . . 15
|
36 | | nfra1 2941 |
. . . . . . . . . . . . . . 15
|
37 | 35, 36 | nfan 1828 |
. . . . . . . . . . . . . 14
|
38 | 34, 37 | nfan 1828 |
. . . . . . . . . . . . 13
|
39 | | nfv 1843 |
. . . . . . . . . . . . 13
|
40 | 38, 39 | nfan 1828 |
. . . . . . . . . . . 12
|
41 | | simp3 1063 |
. . . . . . . . . . . . . 14
|
42 | | simp1ll 1124 |
. . . . . . . . . . . . . . 15
|
43 | | simplrr 801 |
. . . . . . . . . . . . . . . 16
|
44 | 43 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . 15
|
45 | | simp2 1062 |
. . . . . . . . . . . . . . 15
|
46 | | simp3 1063 |
. . . . . . . . . . . . . . . . 17
|
47 | | 3simpc 1060 |
. . . . . . . . . . . . . . . . . 18
|
48 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . 21
|
49 | | stoweidlem31.3 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
50 | | stoweidlem31.13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
51 | | rabexg 4812 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
53 | 52 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
54 | 49, 53 | ralrimi 2957 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
55 | 5 | fnmpt 6020 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
57 | 56 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
58 | | fvelrnb 6243 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
59 | | nfmpt1 4747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
60 | 5, 59 | nfcxfr 2762 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
61 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
62 | 60, 61 | nffv 6198 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
63 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
64 | 62, 63 | nfeq 2776 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
65 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
66 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
67 | 66 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
68 | 64, 65, 67 | cbvrex 3168 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
69 | 58, 68 | syl6bb 276 |
. . . . . . . . . . . . . . . . . . . . . 22
|
70 | 57, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
71 | 48, 70 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . 20
|
72 | 60 | nfrn 5368 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
73 | 72 | nfcri 2758 |
. . . . . . . . . . . . . . . . . . . . . 22
|
74 | 49, 73 | nfan 1828 |
. . . . . . . . . . . . . . . . . . . . 21
|
75 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . . 21
|
76 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
77 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
78 | 50 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
79 | 78, 51 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
80 | 5 | fvmpt2 6291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
81 | 77, 79, 80 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
82 | 7 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
83 | | stoweidlem31.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
84 | 83 | rabeq2i 3197 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
85 | 82, 84 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
86 | 85 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
87 | | stoweidlem31.10 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
88 | | stoweidlem31.8 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
89 | 88 | nnrpd 11870 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
90 | 87, 89 | rpdivcld 11889 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
91 | 90 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
92 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
93 | 92 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
94 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
95 | 94 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
96 | 95 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
97 | 93, 96 | 3anbi23d 1402 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
98 | 97 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
99 | 98 | rspccva 3308 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
100 | 86, 91, 99 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
101 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
102 | 19, 101 | nfan 1828 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
103 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
104 | 22, 103 | nfne 2894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
105 | | 3simpc 1060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
106 | | rabid 3116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
107 | 105, 106 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
108 | | ne0i 3921 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
109 | 107, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
110 | 109 | 3exp 1264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
111 | 102, 104,
110 | rexlimd 3026 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
112 | 100, 111 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
113 | 81, 112 | eqnetrd 2861 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
114 | 113 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
115 | 76, 114 | eqnetrrd 2862 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
116 | 115 | 3adant1r 1319 |
. . . . . . . . . . . . . . . . . . . . . 22
|
117 | 116 | 3exp 1264 |
. . . . . . . . . . . . . . . . . . . . 21
|
118 | 74, 75, 117 | rexlimd 3026 |
. . . . . . . . . . . . . . . . . . . 20
|
119 | 71, 118 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
|
120 | 119 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . 18
|
121 | | rspa 2930 |
. . . . . . . . . . . . . . . . . 18
|
122 | 47, 120, 121 | sylc 65 |
. . . . . . . . . . . . . . . . 17
|
123 | 46, 122 | jca 554 |
. . . . . . . . . . . . . . . 16
|
124 | | vex 3203 |
. . . . . . . . . . . . . . . . . 18
|
125 | 5 | elrnmpt 5372 |
. . . . . . . . . . . . . . . . . 18
|
126 | 124, 125 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
|
127 | 46, 126 | sylib 208 |
. . . . . . . . . . . . . . . 16
|
128 | | nfv 1843 |
. . . . . . . . . . . . . . . . . 18
|
129 | 73, 128 | nfan 1828 |
. . . . . . . . . . . . . . . . 17
|
130 | | nfv 1843 |
. . . . . . . . . . . . . . . . 17
|
131 | | simp1r 1086 |
. . . . . . . . . . . . . . . . . . 19
|
132 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . 19
|
133 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . 22
|
134 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . 22
|
135 | 133, 134 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . 21
|
136 | | elrabi 3359 |
. . . . . . . . . . . . . . . . . . . . . 22
|
137 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
138 | 137 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
139 | 137 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
140 | 138, 139 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
141 | 140 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
142 | 137 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
143 | 142 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
144 | 137 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
145 | 144 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
146 | 141, 143,
145 | 3anbi123d 1399 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
147 | 146 | elrab 3363 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
148 | 147 | simprbi 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
149 | 148 | simp1d 1073 |
. . . . . . . . . . . . . . . . . . . . . 22
|
150 | 141 | elrab 3363 |
. . . . . . . . . . . . . . . . . . . . . 22
|
151 | 136, 149,
150 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . . . 21
|
152 | 135, 151 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
153 | | stoweidlem31.4 |
. . . . . . . . . . . . . . . . . . . 20
|
154 | 152, 153 | syl6eleqr 2712 |
. . . . . . . . . . . . . . . . . . 19
|
155 | 131, 132,
154 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
156 | 155 | 3exp 1264 |
. . . . . . . . . . . . . . . . 17
|
157 | 129, 130,
156 | rexlimd 3026 |
. . . . . . . . . . . . . . . 16
|
158 | 123, 127,
157 | sylc 65 |
. . . . . . . . . . . . . . 15
|
159 | 42, 44, 45, 158 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
160 | 41, 159 | eqeltrrd 2702 |
. . . . . . . . . . . . 13
|
161 | 160 | 3exp 1264 |
. . . . . . . . . . . 12
|
162 | 40, 161 | reximdai 3012 |
. . . . . . . . . . 11
|
163 | 33, 162 | mpd 15 |
. . . . . . . . . 10
|
164 | | nfv 1843 |
. . . . . . . . . . 11
|
165 | | idd 24 |
. . . . . . . . . . . 12
|
166 | 165 | a1i 11 |
. . . . . . . . . . 11
|
167 | 40, 164, 166 | rexlimd 3026 |
. . . . . . . . . 10
|
168 | 163, 167 | mpd 15 |
. . . . . . . . 9
|
169 | 168 | ex 450 |
. . . . . . . 8
|
170 | 30, 169 | ralrimi 2957 |
. . . . . . 7
|
171 | | dfss3 3592 |
. . . . . . . 8
|
172 | | nfrab1 3122 |
. . . . . . . . . . 11
|
173 | 153, 172 | nfcxfr 2762 |
. . . . . . . . . 10
|
174 | 173 | nfcri 2758 |
. . . . . . . . 9
|
175 | | nfv 1843 |
. . . . . . . . 9
|
176 | | eleq1 2689 |
. . . . . . . . 9
|
177 | 174, 175,
176 | cbvral 3167 |
. . . . . . . 8
|
178 | 171, 177 | bitri 264 |
. . . . . . 7
|
179 | 170, 178 | sylibr 224 |
. . . . . 6
|
180 | | df-f 5892 |
. . . . . 6
|
181 | 18, 179, 180 | sylanbrc 698 |
. . . . 5
|
182 | | dffn3 6054 |
. . . . . . . 8
|
183 | 56, 182 | sylib 208 |
. . . . . . 7
|
184 | 183 | adantr 481 |
. . . . . 6
|
185 | | stoweidlem31.9 |
. . . . . . . 8
|
186 | | f1of 6137 |
. . . . . . . 8
|
187 | 185, 186 | syl 17 |
. . . . . . 7
|
188 | 187 | adantr 481 |
. . . . . 6
|
189 | | fco 6058 |
. . . . . 6
|
190 | 184, 188,
189 | syl2anc 693 |
. . . . 5
|
191 | | fco 6058 |
. . . . 5
|
192 | 181, 190,
191 | syl2anc 693 |
. . . 4
|
193 | | fvco3 6275 |
. . . . . . . . 9
|
194 | 190, 193 | sylan 488 |
. . . . . . . 8
|
195 | | simpll 790 |
. . . . . . . . 9
|
196 | | simplrr 801 |
. . . . . . . . 9
|
197 | 190 | ffvelrnda 6359 |
. . . . . . . . 9
|
198 | | simp3 1063 |
. . . . . . . . . 10
|
199 | | nfv 1843 |
. . . . . . . . . . . . 13
|
200 | 34, 36, 199 | nf3an 1831 |
. . . . . . . . . . . 12
|
201 | | nfv 1843 |
. . . . . . . . . . . 12
|
202 | 200, 201 | nfim 1825 |
. . . . . . . . . . 11
|
203 | | eleq1 2689 |
. . . . . . . . . . . . 13
|
204 | 203 | 3anbi3d 1405 |
. . . . . . . . . . . 12
|
205 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
206 | | id 22 |
. . . . . . . . . . . . 13
|
207 | 205, 206 | eleq12d 2695 |
. . . . . . . . . . . 12
|
208 | 204, 207 | imbi12d 334 |
. . . . . . . . . . 11
|
209 | 202, 208,
122 | vtoclg1f 3265 |
. . . . . . . . . 10
|
210 | 198, 209 | mpcom 38 |
. . . . . . . . 9
|
211 | 195, 196,
197, 210 | syl3anc 1326 |
. . . . . . . 8
|
212 | 194, 211 | eqeltrd 2701 |
. . . . . . 7
|
213 | | fvco3 6275 |
. . . . . . . . . . . 12
|
214 | 187, 213 | sylan 488 |
. . . . . . . . . . 11
|
215 | 187 | ffvelrnda 6359 |
. . . . . . . . . . . 12
|
216 | 50 | adantr 481 |
. . . . . . . . . . . . 13
|
217 | | rabexg 4812 |
. . . . . . . . . . . . 13
|
218 | 216, 217 | syl 17 |
. . . . . . . . . . . 12
|
219 | | raleq 3138 |
. . . . . . . . . . . . . . 15
|
220 | 219 | 3anbi2d 1404 |
. . . . . . . . . . . . . 14
|
221 | 220 | rabbidv 3189 |
. . . . . . . . . . . . 13
|
222 | 221, 5 | fvmptg 6280 |
. . . . . . . . . . . 12
|
223 | 215, 218,
222 | syl2anc 693 |
. . . . . . . . . . 11
|
224 | 214, 223 | eqtrd 2656 |
. . . . . . . . . 10
|
225 | 224 | adantlr 751 |
. . . . . . . . 9
|
226 | 225 | eleq2d 2687 |
. . . . . . . 8
|
227 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
228 | 24, 227 | nfco 5287 |
. . . . . . . . . . . . 13
|
229 | 20, 228 | nfco 5287 |
. . . . . . . . . . . 12
|
230 | | nfcv 2764 |
. . . . . . . . . . . 12
|
231 | 229, 230 | nffv 6198 |
. . . . . . . . . . 11
|
232 | | nfcv 2764 |
. . . . . . . . . . 11
|
233 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
234 | | nfcv 2764 |
. . . . . . . . . . . . . . 15
|
235 | | nfcv 2764 |
. . . . . . . . . . . . . . 15
|
236 | | nfcv 2764 |
. . . . . . . . . . . . . . . 16
|
237 | 231, 236 | nffv 6198 |
. . . . . . . . . . . . . . 15
|
238 | 234, 235,
237 | nfbr 4699 |
. . . . . . . . . . . . . 14
|
239 | | nfcv 2764 |
. . . . . . . . . . . . . . 15
|
240 | 237, 235,
239 | nfbr 4699 |
. . . . . . . . . . . . . 14
|
241 | 238, 240 | nfan 1828 |
. . . . . . . . . . . . 13
|
242 | 233, 241 | nfral 2945 |
. . . . . . . . . . . 12
|
243 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
244 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
245 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
246 | 237, 244,
245 | nfbr 4699 |
. . . . . . . . . . . . 13
|
247 | 243, 246 | nfral 2945 |
. . . . . . . . . . . 12
|
248 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
249 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
250 | 249, 244,
237 | nfbr 4699 |
. . . . . . . . . . . . 13
|
251 | 248, 250 | nfral 2945 |
. . . . . . . . . . . 12
|
252 | 242, 247,
251 | nf3an 1831 |
. . . . . . . . . . 11
|
253 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
254 | | nfcv 2764 |
. . . . . . . . . . . . . . . 16
|
255 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . 19
|
256 | | nfra1 2941 |
. . . . . . . . . . . . . . . . . . . . 21
|
257 | | nfra1 2941 |
. . . . . . . . . . . . . . . . . . . . 21
|
258 | | nfra1 2941 |
. . . . . . . . . . . . . . . . . . . . 21
|
259 | 256, 257,
258 | nf3an 1831 |
. . . . . . . . . . . . . . . . . . . 20
|
260 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . 20
|
261 | 259, 260 | nfrab 3123 |
. . . . . . . . . . . . . . . . . . 19
|
262 | 255, 261 | nfmpt 4746 |
. . . . . . . . . . . . . . . . . 18
|
263 | 5, 262 | nfcxfr 2762 |
. . . . . . . . . . . . . . . . 17
|
264 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
|
265 | 263, 264 | nfco 5287 |
. . . . . . . . . . . . . . . 16
|
266 | 254, 265 | nfco 5287 |
. . . . . . . . . . . . . . 15
|
267 | | nfcv 2764 |
. . . . . . . . . . . . . . 15
|
268 | 266, 267 | nffv 6198 |
. . . . . . . . . . . . . 14
|
269 | 253, 268 | nfeq 2776 |
. . . . . . . . . . . . 13
|
270 | | fveq1 6190 |
. . . . . . . . . . . . . . 15
|
271 | 270 | breq2d 4665 |
. . . . . . . . . . . . . 14
|
272 | 270 | breq1d 4663 |
. . . . . . . . . . . . . 14
|
273 | 271, 272 | anbi12d 747 |
. . . . . . . . . . . . 13
|
274 | 269, 273 | ralbid 2983 |
. . . . . . . . . . . 12
|
275 | 270 | breq1d 4663 |
. . . . . . . . . . . . 13
|
276 | 269, 275 | ralbid 2983 |
. . . . . . . . . . . 12
|
277 | 270 | breq2d 4665 |
. . . . . . . . . . . . 13
|
278 | 269, 277 | ralbid 2983 |
. . . . . . . . . . . 12
|
279 | 274, 276,
278 | 3anbi123d 1399 |
. . . . . . . . . . 11
|
280 | 231, 232,
252, 279 | elrabf 3360 |
. . . . . . . . . 10
|
281 | 280 | simprbi 480 |
. . . . . . . . 9
|
282 | 281 | simp2d 1074 |
. . . . . . . 8
|
283 | 226, 282 | syl6bi 243 |
. . . . . . 7
|
284 | 212, 283 | mpd 15 |
. . . . . 6
|
285 | | stoweidlem31.2 |
. . . . . . . . 9
|
286 | 263 | nfrn 5368 |
. . . . . . . . . . 11
|
287 | 254, 286 | nffn 5987 |
. . . . . . . . . 10
|
288 | | nfv 1843 |
. . . . . . . . . . 11
|
289 | 286, 288 | nfral 2945 |
. . . . . . . . . 10
|
290 | 287, 289 | nfan 1828 |
. . . . . . . . 9
|
291 | 285, 290 | nfan 1828 |
. . . . . . . 8
|
292 | | nfv 1843 |
. . . . . . . 8
|
293 | 291, 292 | nfan 1828 |
. . . . . . 7
|
294 | | stoweidlem31.11 |
. . . . . . . . . . 11
|
295 | 294 | ad3antrrr 766 |
. . . . . . . . . 10
|
296 | | simpr 477 |
. . . . . . . . . 10
|
297 | 295, 296 | sseldd 3604 |
. . . . . . . . 9
|
298 | 281 | simp3d 1075 |
. . . . . . . . . . . 12
|
299 | 226, 298 | syl6bi 243 |
. . . . . . . . . . 11
|
300 | 212, 299 | mpd 15 |
. . . . . . . . . 10
|
301 | 300 | r19.21bi 2932 |
. . . . . . . . 9
|
302 | 297, 301 | syldan 487 |
. . . . . . . 8
|
303 | 302 | ex 450 |
. . . . . . 7
|
304 | 293, 303 | ralrimi 2957 |
. . . . . 6
|
305 | 284, 304 | jca 554 |
. . . . 5
|
306 | 305 | ralrimiva 2966 |
. . . 4
|
307 | 192, 306 | jca 554 |
. . 3
|
308 | | feq1 6026 |
. . . . 5
|
309 | | nfcv 2764 |
. . . . . . . . 9
|
310 | 309, 266 | nfeq 2776 |
. . . . . . . 8
|
311 | | fveq1 6190 |
. . . . . . . . . 10
|
312 | 311 | fveq1d 6193 |
. . . . . . . . 9
|
313 | 312 | breq1d 4663 |
. . . . . . . 8
|
314 | 310, 313 | ralbid 2983 |
. . . . . . 7
|
315 | 312 | breq2d 4665 |
. . . . . . . 8
|
316 | 310, 315 | ralbid 2983 |
. . . . . . 7
|
317 | 314, 316 | anbi12d 747 |
. . . . . 6
|
318 | 317 | ralbidv 2986 |
. . . . 5
|
319 | 308, 318 | anbi12d 747 |
. . . 4
|
320 | 319 | spcegv 3294 |
. . 3
|
321 | 17, 307, 320 | sylc 65 |
. 2
|
322 | 3, 321 | exlimddv 1863 |
1
|