Step | Hyp | Ref
| Expression |
1 | | sseq2 3525 |
. . . . . 6
|
2 | | fveq2 5871 |
. . . . . . 7
|
3 | 2 | sseq2d 3531 |
. . . . . 6
|
4 | 1, 3 | imbi12d 320 |
. . . . 5
|
5 | 4 | imbi2d 316 |
. . . 4
|
6 | | sseq2 3525 |
. . . . . 6
|
7 | | fveq2 5871 |
. . . . . . 7
|
8 | 7 | sseq2d 3531 |
. . . . . 6
|
9 | 6, 8 | imbi12d 320 |
. . . . 5
|
10 | 9 | imbi2d 316 |
. . . 4
|
11 | | r19.21v 2862 |
. . . . 5
|
12 | | simpllr 760 |
. . . . . . . . . 10
|
13 | | simplr 755 |
. . . . . . . . . 10
|
14 | | onsseleq 4924 |
. . . . . . . . . 10
|
15 | 12, 13, 14 | syl2anc 661 |
. . . . . . . . 9
|
16 | | sseq2 3525 |
. . . . . . . . . . . . 13
|
17 | | sseq2 3525 |
. . . . . . . . . . . . 13
|
18 | | ttukeylem.4 |
. . . . . . . . . . . . . . . . . . 19
|
19 | 18 | tfr1 7085 |
. . . . . . . . . . . . . . . . . 18
|
20 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
21 | | simplr 755 |
. . . . . . . . . . . . . . . . . 18
|
22 | | onss 6626 |
. . . . . . . . . . . . . . . . . 18
|
23 | 21, 22 | syl 16 |
. . . . . . . . . . . . . . . . 17
|
24 | | simprr 757 |
. . . . . . . . . . . . . . . . 17
|
25 | | fnfvima 6150 |
. . . . . . . . . . . . . . . . 17
|
26 | 20, 23, 24, 25 | syl3anc 1228 |
. . . . . . . . . . . . . . . 16
|
27 | | elssuni 4279 |
. . . . . . . . . . . . . . . 16
|
28 | 26, 27 | syl 16 |
. . . . . . . . . . . . . . 15
|
29 | | n0i 3789 |
. . . . . . . . . . . . . . . 16
|
30 | | iffalse 3950 |
. . . . . . . . . . . . . . . 16
|
31 | 24, 29, 30 | 3syl 20 |
. . . . . . . . . . . . . . 15
|
32 | 28, 31 | sseqtr4d 3540 |
. . . . . . . . . . . . . 14
|
33 | 32 | adantr 465 |
. . . . . . . . . . . . 13
|
34 | | vex 3112 |
. . . . . . . . . . . . . . . . . 18
|
35 | 34 | uniex 6596 |
. . . . . . . . . . . . . . . . 17
|
36 | 35 | sucid 4962 |
. . . . . . . . . . . . . . . 16
|
37 | | eloni 4893 |
. . . . . . . . . . . . . . . . . 18
|
38 | | orduniorsuc 6665 |
. . . . . . . . . . . . . . . . . 18
|
39 | 21, 37, 38 | 3syl 20 |
. . . . . . . . . . . . . . . . 17
|
40 | 39 | orcanai 913 |
. . . . . . . . . . . . . . . 16
|
41 | 36, 40 | syl5eleqr 2552 |
. . . . . . . . . . . . . . 15
|
42 | | simplrl 761 |
. . . . . . . . . . . . . . 15
|
43 | 24 | adantr 465 |
. . . . . . . . . . . . . . . 16
|
44 | | elssuni 4279 |
. . . . . . . . . . . . . . . 16
|
45 | 43, 44 | syl 16 |
. . . . . . . . . . . . . . 15
|
46 | | sseq2 3525 |
. . . . . . . . . . . . . . . . 17
|
47 | | fveq2 5871 |
. . . . . . . . . . . . . . . . . 18
|
48 | 47 | sseq2d 3531 |
. . . . . . . . . . . . . . . . 17
|
49 | 46, 48 | imbi12d 320 |
. . . . . . . . . . . . . . . 16
|
50 | 49 | rspcv 3206 |
. . . . . . . . . . . . . . 15
|
51 | 41, 42, 45, 50 | syl3c 61 |
. . . . . . . . . . . . . 14
|
52 | | ssun1 3666 |
. . . . . . . . . . . . . 14
|
53 | 51, 52 | syl6ss 3515 |
. . . . . . . . . . . . 13
|
54 | 16, 17, 33, 53 | ifbothda 3976 |
. . . . . . . . . . . 12
|
55 | | simplll 759 |
. . . . . . . . . . . . 13
|
56 | | ttukeylem.1 |
. . . . . . . . . . . . . 14
|
57 | | ttukeylem.2 |
. . . . . . . . . . . . . 14
|
58 | | ttukeylem.3 |
. . . . . . . . . . . . . 14
|
59 | 56, 57, 58, 18 | ttukeylem3 8912 |
. . . . . . . . . . . . 13
|
60 | 55, 21, 59 | syl2anc 661 |
. . . . . . . . . . . 12
|
61 | 54, 60 | sseqtr4d 3540 |
. . . . . . . . . . 11
|
62 | 61 | expr 615 |
. . . . . . . . . 10
|
63 | | fveq2 5871 |
. . . . . . . . . . . 12
|
64 | | eqimss 3555 |
. . . . . . . . . . . 12
|
65 | 63, 64 | syl 16 |
. . . . . . . . . . 11
|
66 | 65 | a1i 11 |
. . . . . . . . . 10
|
67 | 62, 66 | jaod 380 |
. . . . . . . . 9
|
68 | 15, 67 | sylbid 215 |
. . . . . . . 8
|
69 | 68 | ex 434 |
. . . . . . 7
|
70 | 69 | expcom 435 |
. . . . . 6
|
71 | 70 | a2d 26 |
. . . . 5
|
72 | 11, 71 | syl5bi 217 |
. . . 4
|
73 | 5, 10, 72 | tfis3 6692 |
. . 3
|
74 | 73 | expdcom 439 |
. 2
|
75 | 74 | 3imp2 1211 |
1
|