Proof of Theorem elovmpt3rab1
Step | Hyp | Ref
| Expression |
1 | | ovmpt3rab1.o |
. . . 4
|
2 | 1 | elovmpt3imp 6890 |
. . 3
|
3 | | simprl 794 |
. . . . 5
|
4 | | elfvdm 6220 |
. . . . . . 7
|
5 | | simpl 473 |
. . . . . . . . . . . . . . 15
|
6 | 5 | adantr 481 |
. . . . . . . . . . . . . 14
|
7 | | simplr 792 |
. . . . . . . . . . . . . 14
|
8 | | simprl 794 |
. . . . . . . . . . . . . 14
|
9 | | simprr 796 |
. . . . . . . . . . . . . 14
|
10 | | ovmpt3rab1.m |
. . . . . . . . . . . . . . 15
|
11 | | ovmpt3rab1.n |
. . . . . . . . . . . . . . 15
|
12 | 1, 10, 11 | ovmpt3rabdm 6892 |
. . . . . . . . . . . . . 14
|
13 | 6, 7, 8, 9, 12 | syl31anc 1329 |
. . . . . . . . . . . . 13
|
14 | 13 | eleq2d 2687 |
. . . . . . . . . . . 12
|
15 | 14 | biimpcd 239 |
. . . . . . . . . . 11
|
16 | 15 | adantr 481 |
. . . . . . . . . 10
|
17 | 16 | imp 445 |
. . . . . . . . 9
|
18 | | simpl 473 |
. . . . . . . . . 10
|
19 | | simplr 792 |
. . . . . . . . . . . . 13
|
20 | 19 | adantl 482 |
. . . . . . . . . . . 12
|
21 | | simpl 473 |
. . . . . . . . . . . . . . . . 17
|
22 | 21 | anim2i 593 |
. . . . . . . . . . . . . . . 16
|
23 | | df-3an 1039 |
. . . . . . . . . . . . . . . 16
|
24 | 22, 23 | sylibr 224 |
. . . . . . . . . . . . . . 15
|
25 | 24 | ad2antll 765 |
. . . . . . . . . . . . . 14
|
26 | | sbceq1a 3446 |
. . . . . . . . . . . . . . . . 17
|
27 | | sbceq1a 3446 |
. . . . . . . . . . . . . . . . 17
|
28 | 26, 27 | sylan9bbr 737 |
. . . . . . . . . . . . . . . 16
|
29 | | nfsbc1v 3455 |
. . . . . . . . . . . . . . . 16
|
30 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
|
31 | | nfsbc1v 3455 |
. . . . . . . . . . . . . . . . 17
|
32 | 30, 31 | nfsbc 3457 |
. . . . . . . . . . . . . . . 16
|
33 | 1, 10, 11, 28, 29, 32 | ovmpt3rab1 6891 |
. . . . . . . . . . . . . . 15
|
34 | 33 | fveq1d 6193 |
. . . . . . . . . . . . . 14
|
35 | 25, 34 | syl 17 |
. . . . . . . . . . . . 13
|
36 | | rabexg 4812 |
. . . . . . . . . . . . . . . 16
|
37 | 36 | adantl 482 |
. . . . . . . . . . . . . . 15
|
38 | 37 | ad2antll 765 |
. . . . . . . . . . . . . 14
|
39 | | nfcv 2764 |
. . . . . . . . . . . . . . 15
|
40 | | nfsbc1v 3455 |
. . . . . . . . . . . . . . . 16
|
41 | | nfcv 2764 |
. . . . . . . . . . . . . . . 16
|
42 | 40, 41 | nfrab 3123 |
. . . . . . . . . . . . . . 15
|
43 | | sbceq1a 3446 |
. . . . . . . . . . . . . . . 16
|
44 | 43 | rabbidv 3189 |
. . . . . . . . . . . . . . 15
|
45 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
46 | 39, 42, 44, 45 | fvmptf 6301 |
. . . . . . . . . . . . . 14
|
47 | 38, 46 | sylan2 491 |
. . . . . . . . . . . . 13
|
48 | 35, 47 | eqtr2d 2657 |
. . . . . . . . . . . 12
|
49 | 20, 48 | eleqtrrd 2704 |
. . . . . . . . . . 11
|
50 | | elrabi 3359 |
. . . . . . . . . . 11
|
51 | 49, 50 | syl 17 |
. . . . . . . . . 10
|
52 | 18, 51 | jca 554 |
. . . . . . . . 9
|
53 | 17, 52 | mpancom 703 |
. . . . . . . 8
|
54 | 53 | exp31 630 |
. . . . . . 7
|
55 | 4, 54 | mpcom 38 |
. . . . . 6
|
56 | 55 | imp 445 |
. . . . 5
|
57 | 3, 56 | jca 554 |
. . . 4
|
58 | 57 | exp32 631 |
. . 3
|
59 | 2, 58 | mpd 15 |
. 2
|
60 | 59 | com12 32 |
1
|