Step | Hyp | Ref
| Expression |
1 | | zfregfr 4298 |
. 2
|
2 | | epel 4029 |
. . . . . 6
|
3 | | epel 4029 |
. . . . . 6
|
4 | 2, 3 | anbi12i 433 |
. . . . 5
|
5 | | simpr 103 |
. . . . . 6
|
6 | | elirr 4266 |
. . . . . . . 8
|
7 | | simprr 484 |
. . . . . . . . . 10
|
8 | | noel 3228 |
. . . . . . . . . . . . 13
|
9 | | eleq2 2101 |
. . . . . . . . . . . . 13
|
10 | 8, 9 | mtbiri 600 |
. . . . . . . . . . . 12
|
11 | | simprl 483 |
. . . . . . . . . . . 12
|
12 | 10, 11 | nsyl3 556 |
. . . . . . . . . . 11
|
13 | | elrabi 2695 |
. . . . . . . . . . . . . . . 16
|
14 | | reg3exmidlemwe.a |
. . . . . . . . . . . . . . . 16
|
15 | 13, 14 | eleq2s 2132 |
. . . . . . . . . . . . . . 15
|
16 | | elpri 3398 |
. . . . . . . . . . . . . . 15
|
17 | 15, 16 | syl 14 |
. . . . . . . . . . . . . 14
|
18 | 17 | orcomd 648 |
. . . . . . . . . . . . 13
|
19 | 18 | 3ad2ant2 926 |
. . . . . . . . . . . 12
|
20 | 19 | adantr 261 |
. . . . . . . . . . 11
|
21 | 12, 20 | ecased 1239 |
. . . . . . . . . 10
|
22 | | noel 3228 |
. . . . . . . . . . . . 13
|
23 | | eleq2 2101 |
. . . . . . . . . . . . 13
|
24 | 22, 23 | mtbiri 600 |
. . . . . . . . . . . 12
|
25 | 24, 7 | nsyl3 556 |
. . . . . . . . . . 11
|
26 | | elrabi 2695 |
. . . . . . . . . . . . . . . 16
|
27 | 26, 14 | eleq2s 2132 |
. . . . . . . . . . . . . . 15
|
28 | | vex 2560 |
. . . . . . . . . . . . . . . 16
|
29 | 28 | elpr 3396 |
. . . . . . . . . . . . . . 15
|
30 | 27, 29 | sylib 127 |
. . . . . . . . . . . . . 14
|
31 | 30 | orcomd 648 |
. . . . . . . . . . . . 13
|
32 | 31 | 3ad2ant3 927 |
. . . . . . . . . . . 12
|
33 | 32 | adantr 261 |
. . . . . . . . . . 11
|
34 | 25, 33 | ecased 1239 |
. . . . . . . . . 10
|
35 | 7, 21, 34 | 3eltr3d 2120 |
. . . . . . . . 9
|
36 | 35 | ex 108 |
. . . . . . . 8
|
37 | 6, 36 | mtoi 590 |
. . . . . . 7
|
38 | 37 | adantr 261 |
. . . . . 6
|
39 | 5, 38 | pm2.21dd 550 |
. . . . 5
|
40 | 4, 39 | sylan2b 271 |
. . . 4
|
41 | 40 | ex 108 |
. . 3
|
42 | 41 | rgen3 2406 |
. 2
|
43 | | df-wetr 4071 |
. 2
|
44 | 1, 42, 43 | mpbir2an 849 |
1
|