Proof of Theorem reusv2lem3
Step | Hyp | Ref
| Expression |
1 | | simpr 477 |
. . . 4
|
2 | | nfv 1843 |
. . . . . 6
|
3 | | nfeu1 2480 |
. . . . . 6
|
4 | 2, 3 | nfan 1828 |
. . . . 5
|
5 | | euex 2494 |
. . . . . . . 8
|
6 | | rexn0 4074 |
. . . . . . . . 9
|
7 | 6 | exlimiv 1858 |
. . . . . . . 8
|
8 | | r19.2z 4060 |
. . . . . . . . 9
|
9 | 8 | ex 450 |
. . . . . . . 8
|
10 | 5, 7, 9 | 3syl 18 |
. . . . . . 7
|
11 | 10 | adantl 482 |
. . . . . 6
|
12 | | nfra1 2941 |
. . . . . . . 8
|
13 | | nfre1 3005 |
. . . . . . . . 9
|
14 | 13 | nfeu 2486 |
. . . . . . . 8
|
15 | 12, 14 | nfan 1828 |
. . . . . . 7
|
16 | | rsp 2929 |
. . . . . . . . . . . . . 14
|
17 | 16 | impcom 446 |
. . . . . . . . . . . . 13
|
18 | | isset 3207 |
. . . . . . . . . . . . 13
|
19 | 17, 18 | sylib 208 |
. . . . . . . . . . . 12
|
20 | 19 | adantrr 753 |
. . . . . . . . . . 11
|
21 | | rspe 3003 |
. . . . . . . . . . . . . . 15
|
22 | 21 | ex 450 |
. . . . . . . . . . . . . 14
|
23 | 22 | ancrd 577 |
. . . . . . . . . . . . 13
|
24 | 23 | eximdv 1846 |
. . . . . . . . . . . 12
|
25 | 24 | imp 445 |
. . . . . . . . . . 11
|
26 | 20, 25 | syldan 487 |
. . . . . . . . . 10
|
27 | | eupick 2536 |
. . . . . . . . . 10
|
28 | 1, 26, 27 | syl2an2 875 |
. . . . . . . . 9
|
29 | 28 | ex 450 |
. . . . . . . 8
|
30 | 29 | com3l 89 |
. . . . . . 7
|
31 | 15, 13, 30 | ralrimd 2959 |
. . . . . 6
|
32 | 11, 31 | impbid 202 |
. . . . 5
|
33 | 4, 32 | eubid 2488 |
. . . 4
|
34 | 1, 33 | mpbird 247 |
. . 3
|
35 | 34 | ex 450 |
. 2
|
36 | | reusv2lem2 4869 |
. 2
|
37 | 35, 36 | impbid1 215 |
1
|