Proof of Theorem suppssov1
Step | Hyp | Ref
| Expression |
1 | | suppssov1.a |
. . . . . . . . . . 11
|
2 | | elex 3212 |
. . . . . . . . . . 11
|
3 | 1, 2 | syl 17 |
. . . . . . . . . 10
|
4 | 3 | adantll 750 |
. . . . . . . . 9
|
5 | 4 | adantr 481 |
. . . . . . . 8
|
6 | | eldifsni 4320 |
. . . . . . . . . 10
|
7 | | suppssov1.b |
. . . . . . . . . . . . . 14
|
8 | 7 | adantll 750 |
. . . . . . . . . . . . 13
|
9 | | suppssov1.o |
. . . . . . . . . . . . . . . 16
|
10 | 9 | ralrimiva 2966 |
. . . . . . . . . . . . . . 15
|
11 | 10 | adantl 482 |
. . . . . . . . . . . . . 14
|
12 | 11 | adantr 481 |
. . . . . . . . . . . . 13
|
13 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
|
14 | 13 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
|
15 | 14 | rspcva 3307 |
. . . . . . . . . . . . 13
|
16 | 8, 12, 15 | syl2anc 693 |
. . . . . . . . . . . 12
|
17 | | oveq1 6657 |
. . . . . . . . . . . . 13
|
18 | 17 | eqeq1d 2624 |
. . . . . . . . . . . 12
|
19 | 16, 18 | syl5ibrcom 237 |
. . . . . . . . . . 11
|
20 | 19 | necon3d 2815 |
. . . . . . . . . 10
|
21 | 6, 20 | syl5 34 |
. . . . . . . . 9
|
22 | 21 | imp 445 |
. . . . . . . 8
|
23 | | eldifsn 4317 |
. . . . . . . 8
|
24 | 5, 22, 23 | sylanbrc 698 |
. . . . . . 7
|
25 | 24 | ex 450 |
. . . . . 6
|
26 | 25 | ss2rabdv 3683 |
. . . . 5
|
27 | | eqid 2622 |
. . . . . 6
|
28 | | simpll 790 |
. . . . . 6
|
29 | | simplr 792 |
. . . . . 6
|
30 | 27, 28, 29 | mptsuppdifd 7317 |
. . . . 5
supp |
31 | | eqid 2622 |
. . . . . 6
|
32 | | suppssov1.y |
. . . . . . 7
|
33 | 32 | adantl 482 |
. . . . . 6
|
34 | 31, 28, 33 | mptsuppdifd 7317 |
. . . . 5
supp |
35 | 26, 30, 34 | 3sstr4d 3648 |
. . . 4
supp supp |
36 | | suppssov1.s |
. . . . 5
supp
|
37 | 36 | adantl 482 |
. . . 4
supp |
38 | 35, 37 | sstrd 3613 |
. . 3
supp |
39 | 38 | ex 450 |
. 2
supp |
40 | | mptexg 6484 |
. . . . . . 7
|
41 | | ovex 6678 |
. . . . . . . . . 10
|
42 | 41 | rgenw 2924 |
. . . . . . . . 9
|
43 | | dmmptg 5632 |
. . . . . . . . 9
|
44 | 42, 43 | ax-mp 5 |
. . . . . . . 8
|
45 | | dmexg 7097 |
. . . . . . . 8
|
46 | 44, 45 | syl5eqelr 2706 |
. . . . . . 7
|
47 | 40, 46 | impbii 199 |
. . . . . 6
|
48 | 47 | anbi1i 731 |
. . . . 5
|
49 | | supp0prc 7298 |
. . . . 5
supp |
50 | 48, 49 | sylnbi 320 |
. . . 4
supp |
51 | | 0ss 3972 |
. . . 4
|
52 | 50, 51 | syl6eqss 3655 |
. . 3
supp
|
53 | 52 | a1d 25 |
. 2
supp |
54 | 39, 53 | pm2.61i 176 |
1
supp
|