Step | Hyp | Ref
| Expression |
1 | | elun 3753 |
. . . . . 6
|
2 | | predel 5697 |
. . . . . . . . . . 11
|
3 | | setlikespec 5701 |
. . . . . . . . . . . . . 14
Se
|
4 | | trpredpred 31728 |
. . . . . . . . . . . . . 14
|
5 | 3, 4 | syl 17 |
. . . . . . . . . . . . 13
Se
|
6 | 5 | expcom 451 |
. . . . . . . . . . . 12
Se
|
7 | 6 | adantl 482 |
. . . . . . . . . . 11
Se |
8 | 2, 7 | syl5 34 |
. . . . . . . . . 10
Se
|
9 | 8 | ancld 576 |
. . . . . . . . 9
Se
|
10 | | trpredeq3 31722 |
. . . . . . . . . . . 12
|
11 | 10 | sseq2d 3633 |
. . . . . . . . . . 11
|
12 | 11 | rspcev 3309 |
. . . . . . . . . 10
|
13 | | ssiun 4562 |
. . . . . . . . . 10
|
14 | 12, 13 | syl 17 |
. . . . . . . . 9
|
15 | 9, 14 | syl6 35 |
. . . . . . . 8
Se
|
16 | | eliun 4524 |
. . . . . . . . 9
|
17 | | predel 5697 |
. . . . . . . . . . . 12
|
18 | | setlikespec 5701 |
. . . . . . . . . . . . . . . . . . . . 21
Se
|
19 | 18 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . 20
Se
|
20 | 19 | adantll 750 |
. . . . . . . . . . . . . . . . . . 19
Se
|
21 | | trpredss 31729 |
. . . . . . . . . . . . . . . . . . 19
|
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . . . . 18
Se
|
23 | 22 | sseld 3602 |
. . . . . . . . . . . . . . . . 17
Se
|
24 | 3 | expcom 451 |
. . . . . . . . . . . . . . . . . 18
Se
|
25 | 24 | ad2antlr 763 |
. . . . . . . . . . . . . . . . 17
Se
|
26 | 23, 25 | syld 47 |
. . . . . . . . . . . . . . . 16
Se
|
27 | 26 | imp 445 |
. . . . . . . . . . . . . . 15
Se
|
28 | 27, 4 | syl 17 |
. . . . . . . . . . . . . 14
Se
|
29 | | simpr 477 |
. . . . . . . . . . . . . . . 16
Se
|
30 | | simplr 792 |
. . . . . . . . . . . . . . . 16
Se
Se |
31 | | trpredelss 31732 |
. . . . . . . . . . . . . . . 16
Se
|
32 | 29, 30, 31 | syl2anc 693 |
. . . . . . . . . . . . . . 15
Se
|
33 | 32 | imp 445 |
. . . . . . . . . . . . . 14
Se
|
34 | 28, 33 | sstrd 3613 |
. . . . . . . . . . . . 13
Se
|
35 | 34 | exp31 630 |
. . . . . . . . . . . 12
Se
|
36 | 17, 35 | syl5 34 |
. . . . . . . . . . 11
Se
|
37 | 36 | reximdvai 3015 |
. . . . . . . . . 10
Se
|
38 | 37, 13 | syl6 35 |
. . . . . . . . 9
Se
|
39 | 16, 38 | syl5bi 232 |
. . . . . . . 8
Se
|
40 | 15, 39 | jaod 395 |
. . . . . . 7
Se
|
41 | | ssun4 3779 |
. . . . . . 7
|
42 | 40, 41 | syl6 35 |
. . . . . 6
Se
|
43 | 1, 42 | syl5bi 232 |
. . . . 5
Se
|
44 | 43 | ralrimiv 2965 |
. . . 4
Se
|
45 | | ssun1 3776 |
. . . 4
|
46 | 44, 45 | jctir 561 |
. . 3
Se
|
47 | | trpredmintr 31731 |
. . 3
Se
|
48 | 46, 47 | mpdan 702 |
. 2
Se
|
49 | | setlikespec 5701 |
. . . 4
Se
|
50 | | trpredpred 31728 |
. . . 4
|
51 | 49, 50 | syl 17 |
. . 3
Se
|
52 | 51 | sseld 3602 |
. . . . . 6
Se
|
53 | | trpredelss 31732 |
. . . . . 6
Se
|
54 | 52, 53 | syld 47 |
. . . . 5
Se
|
55 | 54 | ralrimiv 2965 |
. . . 4
Se
|
56 | | iunss 4561 |
. . . 4
|
57 | 55, 56 | sylibr 224 |
. . 3
Se
|
58 | 51, 57 | unssd 3789 |
. 2
Se
|
59 | 48, 58 | eqssd 3620 |
1
Se
|