Step | Hyp | Ref
| Expression |
1 | | soseq.1 |
. . . 4
|
2 | | sopo 5052 |
. . . 4
|
3 | 1, 2 | ax-mp 5 |
. . 3
|
4 | | soseq.2 |
. . 3
|
5 | | soseq.3 |
. . 3
|
6 | 3, 4, 5 | poseq 31750 |
. 2
|
7 | | eleq1 2689 |
. . . . . . . . . . . 12
|
8 | 7 | anbi1d 741 |
. . . . . . . . . . 11
|
9 | | fveq1 6190 |
. . . . . . . . . . . . . . 15
|
10 | 9 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
|
11 | 10 | ralbidv 2986 |
. . . . . . . . . . . . 13
|
12 | | fveq1 6190 |
. . . . . . . . . . . . . 14
|
13 | 12 | breq1d 4663 |
. . . . . . . . . . . . 13
|
14 | 11, 13 | anbi12d 747 |
. . . . . . . . . . . 12
|
15 | 14 | rexbidv 3052 |
. . . . . . . . . . 11
|
16 | 8, 15 | anbi12d 747 |
. . . . . . . . . 10
|
17 | | eleq1 2689 |
. . . . . . . . . . . 12
|
18 | 17 | anbi2d 740 |
. . . . . . . . . . 11
|
19 | | fveq1 6190 |
. . . . . . . . . . . . . . 15
|
20 | 19 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
|
21 | 20 | ralbidv 2986 |
. . . . . . . . . . . . 13
|
22 | | fveq1 6190 |
. . . . . . . . . . . . . 14
|
23 | 22 | breq2d 4665 |
. . . . . . . . . . . . 13
|
24 | 21, 23 | anbi12d 747 |
. . . . . . . . . . . 12
|
25 | 24 | rexbidv 3052 |
. . . . . . . . . . 11
|
26 | 18, 25 | anbi12d 747 |
. . . . . . . . . 10
|
27 | 16, 26, 5 | brabg 4994 |
. . . . . . . . 9
|
28 | 27 | bianabs 924 |
. . . . . . . 8
|
29 | | eleq1 2689 |
. . . . . . . . . . . . 13
|
30 | 29 | anbi1d 741 |
. . . . . . . . . . . 12
|
31 | | fveq1 6190 |
. . . . . . . . . . . . . . . 16
|
32 | 31 | eqeq1d 2624 |
. . . . . . . . . . . . . . 15
|
33 | 32 | ralbidv 2986 |
. . . . . . . . . . . . . 14
|
34 | | fveq1 6190 |
. . . . . . . . . . . . . . 15
|
35 | 34 | breq1d 4663 |
. . . . . . . . . . . . . 14
|
36 | 33, 35 | anbi12d 747 |
. . . . . . . . . . . . 13
|
37 | 36 | rexbidv 3052 |
. . . . . . . . . . . 12
|
38 | 30, 37 | anbi12d 747 |
. . . . . . . . . . 11
|
39 | | eleq1 2689 |
. . . . . . . . . . . . 13
|
40 | 39 | anbi2d 740 |
. . . . . . . . . . . 12
|
41 | | fveq1 6190 |
. . . . . . . . . . . . . . . 16
|
42 | 41 | eqeq2d 2632 |
. . . . . . . . . . . . . . 15
|
43 | 42 | ralbidv 2986 |
. . . . . . . . . . . . . 14
|
44 | | fveq1 6190 |
. . . . . . . . . . . . . . 15
|
45 | 44 | breq2d 4665 |
. . . . . . . . . . . . . 14
|
46 | 43, 45 | anbi12d 747 |
. . . . . . . . . . . . 13
|
47 | 46 | rexbidv 3052 |
. . . . . . . . . . . 12
|
48 | 40, 47 | anbi12d 747 |
. . . . . . . . . . 11
|
49 | 38, 48, 5 | brabg 4994 |
. . . . . . . . . 10
|
50 | 49 | bianabs 924 |
. . . . . . . . 9
|
51 | 50 | ancoms 469 |
. . . . . . . 8
|
52 | 28, 51 | orbi12d 746 |
. . . . . . 7
|
53 | 52 | notbid 308 |
. . . . . 6
|
54 | | ralinexa 2997 |
. . . . . . . 8
|
55 | | andi 911 |
. . . . . . . . . . 11
|
56 | | eqcom 2629 |
. . . . . . . . . . . . . 14
|
57 | 56 | ralbii 2980 |
. . . . . . . . . . . . 13
|
58 | 57 | anbi1i 731 |
. . . . . . . . . . . 12
|
59 | 58 | orbi2i 541 |
. . . . . . . . . . 11
|
60 | 55, 59 | bitri 264 |
. . . . . . . . . 10
|
61 | 60 | rexbii 3041 |
. . . . . . . . 9
|
62 | | r19.43 3093 |
. . . . . . . . 9
|
63 | 61, 62 | bitri 264 |
. . . . . . . 8
|
64 | 54, 63 | xchbinx 324 |
. . . . . . 7
|
65 | | feq2 6027 |
. . . . . . . . . . . . . . 15
|
66 | 65 | cbvrexv 3172 |
. . . . . . . . . . . . . 14
|
67 | 66 | abbii 2739 |
. . . . . . . . . . . . 13
|
68 | 4, 67 | eqtri 2644 |
. . . . . . . . . . . 12
|
69 | 68 | orderseqlem 31749 |
. . . . . . . . . . 11
|
70 | 68 | orderseqlem 31749 |
. . . . . . . . . . 11
|
71 | | sotrieq 5062 |
. . . . . . . . . . . 12
|
72 | 1, 71 | mpan 706 |
. . . . . . . . . . 11
|
73 | 69, 70, 72 | syl2an 494 |
. . . . . . . . . 10
|
74 | 73 | imbi2d 330 |
. . . . . . . . 9
|
75 | 74 | ralbidv 2986 |
. . . . . . . 8
|
76 | | vex 3203 |
. . . . . . . . . . . . . 14
|
77 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
78 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
79 | 77, 78 | eqeq12d 2637 |
. . . . . . . . . . . . . 14
|
80 | 76, 79 | sbcie 3470 |
. . . . . . . . . . . . 13
|
81 | 80 | ralbii 2980 |
. . . . . . . . . . . 12
|
82 | 81 | imbi1i 339 |
. . . . . . . . . . 11
|
83 | 82 | ralbii 2980 |
. . . . . . . . . 10
|
84 | | tfisg 31716 |
. . . . . . . . . 10
|
85 | 83, 84 | sylbir 225 |
. . . . . . . . 9
|
86 | | vex 3203 |
. . . . . . . . . . . . . 14
|
87 | | feq1 6026 |
. . . . . . . . . . . . . . 15
|
88 | 87 | rexbidv 3052 |
. . . . . . . . . . . . . 14
|
89 | 86, 88, 4 | elab2 3354 |
. . . . . . . . . . . . 13
|
90 | | feq2 6027 |
. . . . . . . . . . . . . 14
|
91 | 90 | cbvrexv 3172 |
. . . . . . . . . . . . 13
|
92 | 89, 91 | bitri 264 |
. . . . . . . . . . . 12
|
93 | | vex 3203 |
. . . . . . . . . . . . . 14
|
94 | | feq1 6026 |
. . . . . . . . . . . . . . 15
|
95 | 94 | rexbidv 3052 |
. . . . . . . . . . . . . 14
|
96 | 93, 95, 4 | elab2 3354 |
. . . . . . . . . . . . 13
|
97 | | feq2 6027 |
. . . . . . . . . . . . . 14
|
98 | 97 | cbvrexv 3172 |
. . . . . . . . . . . . 13
|
99 | 96, 98 | bitri 264 |
. . . . . . . . . . . 12
|
100 | 92, 99 | anbi12i 733 |
. . . . . . . . . . 11
|
101 | | reeanv 3107 |
. . . . . . . . . . 11
|
102 | 100, 101 | bitr4i 267 |
. . . . . . . . . 10
|
103 | | onss 6990 |
. . . . . . . . . . . . . . . . . . 19
|
104 | | ssralv 3666 |
. . . . . . . . . . . . . . . . . . 19
|
105 | 103, 104 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
106 | 105 | ad2antlr 763 |
. . . . . . . . . . . . . . . . 17
|
107 | | soseq.4 |
. . . . . . . . . . . . . . . . . . 19
|
108 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
109 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
110 | 108, 109 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
111 | 110 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
112 | 111 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
|
113 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
114 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
115 | | eloni 5733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
116 | | ordirr 5741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
117 | 115, 116 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
118 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
119 | 118 | notbid 308 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
120 | 119 | biimparc 504 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
121 | 117, 120 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
122 | | ndmfv 6218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
123 | | eqtr2 2642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
124 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
125 | 124 | biimprd 238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
126 | 123, 125 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
127 | 126 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
128 | 121, 122,
127 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
129 | 128 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
130 | 114, 129 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
131 | 130 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
132 | 113, 131 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
133 | 132 | exp4b 632 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
134 | 133 | imp32 449 |
. . . . . . . . . . . . . . . . . . . . . 22
|
135 | 112, 134 | syldd 72 |
. . . . . . . . . . . . . . . . . . . . 21
|
136 | 135 | com23 86 |
. . . . . . . . . . . . . . . . . . . 20
|
137 | 136 | imp 445 |
. . . . . . . . . . . . . . . . . . 19
|
138 | 107, 137 | mtoi 190 |
. . . . . . . . . . . . . . . . . 18
|
139 | 138 | ex 450 |
. . . . . . . . . . . . . . . . 17
|
140 | 106, 139 | syld 47 |
. . . . . . . . . . . . . . . 16
|
141 | | onss 6990 |
. . . . . . . . . . . . . . . . . . 19
|
142 | | ssralv 3666 |
. . . . . . . . . . . . . . . . . . 19
|
143 | 141, 142 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
144 | 143 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
145 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
146 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
147 | 145, 146 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
148 | 147 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
149 | 148 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
|
150 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
151 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
152 | | eloni 5733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
153 | | ordirr 5741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
154 | 152, 153 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
155 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
156 | 155 | notbid 308 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
157 | 156 | biimparc 504 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
158 | | ndmfv 6218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
159 | 157, 158 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
160 | 154, 159 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
161 | | eqtr 2641 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
162 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
163 | 162 | biimpd 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
164 | 161, 163 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
165 | 164 | expcom 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
166 | 165 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
167 | 160, 166 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
168 | 167 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
169 | 151, 168 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
170 | 150, 169 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
171 | 170 | exp4b 632 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
172 | 171 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
173 | 172 | imp32 449 |
. . . . . . . . . . . . . . . . . . . . . 22
|
174 | 149, 173 | syldd 72 |
. . . . . . . . . . . . . . . . . . . . 21
|
175 | 174 | com23 86 |
. . . . . . . . . . . . . . . . . . . 20
|
176 | 175 | imp 445 |
. . . . . . . . . . . . . . . . . . 19
|
177 | 107, 176 | mtoi 190 |
. . . . . . . . . . . . . . . . . 18
|
178 | 177 | ex 450 |
. . . . . . . . . . . . . . . . 17
|
179 | 144, 178 | syld 47 |
. . . . . . . . . . . . . . . 16
|
180 | 140, 179 | jcad 555 |
. . . . . . . . . . . . . . 15
|
181 | | ordtri3or 5755 |
. . . . . . . . . . . . . . . . 17
|
182 | 115, 152,
181 | syl2an 494 |
. . . . . . . . . . . . . . . 16
|
183 | 182 | adantr 481 |
. . . . . . . . . . . . . . 15
|
184 | | 3orel13 31598 |
. . . . . . . . . . . . . . 15
|
185 | 180, 183,
184 | syl6ci 71 |
. . . . . . . . . . . . . 14
|
186 | 185, 144 | jcad 555 |
. . . . . . . . . . . . 13
|
187 | | ffn 6045 |
. . . . . . . . . . . . . . 15
|
188 | | ffn 6045 |
. . . . . . . . . . . . . . 15
|
189 | | eqfnfv2 6312 |
. . . . . . . . . . . . . . 15
|
190 | 187, 188,
189 | syl2an 494 |
. . . . . . . . . . . . . 14
|
191 | 190 | adantl 482 |
. . . . . . . . . . . . 13
|
192 | 186, 191 | sylibrd 249 |
. . . . . . . . . . . 12
|
193 | 192 | ex 450 |
. . . . . . . . . . 11
|
194 | 193 | rexlimivv 3036 |
. . . . . . . . . 10
|
195 | 102, 194 | sylbi 207 |
. . . . . . . . 9
|
196 | 85, 195 | syl5 34 |
. . . . . . . 8
|
197 | 75, 196 | sylbird 250 |
. . . . . . 7
|
198 | 64, 197 | syl5bir 233 |
. . . . . 6
|
199 | 53, 198 | sylbid 230 |
. . . . 5
|
200 | 199 | orrd 393 |
. . . 4
|
201 | | 3orcomb 1048 |
. . . . 5
|
202 | | df-3or 1038 |
. . . . 5
|
203 | 201, 202 | bitr2i 265 |
. . . 4
|
204 | 200, 203 | sylib 208 |
. . 3
|
205 | 204 | rgen2a 2977 |
. 2
|
206 | | df-so 5036 |
. 2
|
207 | 6, 205, 206 | mpbir2an 955 |
1
|