Proof of Theorem ressress
Step | Hyp | Ref
| Expression |
1 | | simplr 792 |
. . . . . . . . 9
↾s
|
2 | | simpr1 1067 |
. . . . . . . . 9
↾s
|
3 | | simpr2 1068 |
. . . . . . . . 9
↾s
|
4 | | eqid 2622 |
. . . . . . . . . 10
↾s ↾s |
5 | | eqid 2622 |
. . . . . . . . . 10
|
6 | 4, 5 | ressval2 15929 |
. . . . . . . . 9
↾s sSet
|
7 | 1, 2, 3, 6 | syl3anc 1326 |
. . . . . . . 8
↾s
↾s sSet
|
8 | | inass 3823 |
. . . . . . . . . . 11
|
9 | | in12 3824 |
. . . . . . . . . . 11
|
10 | 8, 9 | eqtri 2644 |
. . . . . . . . . 10
|
11 | 4, 5 | ressbas 15930 |
. . . . . . . . . . . 12
↾s |
12 | 3, 11 | syl 17 |
. . . . . . . . . . 11
↾s
↾s |
13 | 12 | ineq2d 3814 |
. . . . . . . . . 10
↾s
↾s |
14 | 10, 13 | syl5req 2669 |
. . . . . . . . 9
↾s
↾s
|
15 | 14 | opeq2d 4409 |
. . . . . . . 8
↾s
↾s
|
16 | 7, 15 | oveq12d 6668 |
. . . . . . 7
↾s
↾s sSet
↾s
sSet
sSet
|
17 | | fvex 6201 |
. . . . . . . . 9
|
18 | 17 | inex2 4800 |
. . . . . . . 8
|
19 | | setsabs 15902 |
. . . . . . . 8
sSet
sSet
sSet |
20 | 2, 18, 19 | sylancl 694 |
. . . . . . 7
↾s
sSet
sSet
sSet
|
21 | 16, 20 | eqtrd 2656 |
. . . . . 6
↾s
↾s sSet
↾s
sSet
|
22 | | simpll 790 |
. . . . . . 7
↾s
↾s |
23 | | ovexd 6680 |
. . . . . . 7
↾s
↾s |
24 | | simpr3 1069 |
. . . . . . 7
↾s
|
25 | | eqid 2622 |
. . . . . . . 8
↾s
↾s
↾s
↾s |
26 | | eqid 2622 |
. . . . . . . 8
↾s ↾s |
27 | 25, 26 | ressval2 15929 |
. . . . . . 7
↾s ↾s
↾s
↾s
↾s sSet ↾s |
28 | 22, 23, 24, 27 | syl3anc 1326 |
. . . . . 6
↾s
↾s ↾s ↾s sSet ↾s |
29 | | inss1 3833 |
. . . . . . . . 9
|
30 | | sstr 3611 |
. . . . . . . . 9
|
31 | 29, 30 | mpan2 707 |
. . . . . . . 8
|
32 | 1, 31 | nsyl 135 |
. . . . . . 7
↾s
|
33 | | inex1g 4801 |
. . . . . . . 8
|
34 | 3, 33 | syl 17 |
. . . . . . 7
↾s
|
35 | | eqid 2622 |
. . . . . . . 8
↾s ↾s |
36 | 35, 5 | ressval2 15929 |
. . . . . . 7
↾s
sSet
|
37 | 32, 2, 34, 36 | syl3anc 1326 |
. . . . . 6
↾s
↾s sSet
|
38 | 21, 28, 37 | 3eqtr4d 2666 |
. . . . 5
↾s
↾s ↾s ↾s |
39 | 38 | exp31 630 |
. . . 4
↾s
↾s
↾s ↾s |
40 | | ovex 6678 |
. . . . . . . 8
↾s |
41 | 25, 26 | ressid2 15928 |
. . . . . . . 8
↾s ↾s
↾s
↾s ↾s |
42 | 40, 41 | mp3an2 1412 |
. . . . . . 7
↾s
↾s
↾s ↾s |
43 | 42 | 3ad2antr3 1228 |
. . . . . 6
↾s
↾s
↾s ↾s |
44 | | in32 3825 |
. . . . . . . . 9
|
45 | | simpr2 1068 |
. . . . . . . . . . . 12
↾s
|
46 | 45, 11 | syl 17 |
. . . . . . . . . . 11
↾s
↾s |
47 | | simpl 473 |
. . . . . . . . . . 11
↾s
↾s
|
48 | 46, 47 | eqsstrd 3639 |
. . . . . . . . . 10
↾s
|
49 | | df-ss 3588 |
. . . . . . . . . 10
|
50 | 48, 49 | sylib 208 |
. . . . . . . . 9
↾s
|
51 | 44, 50 | syl5req 2669 |
. . . . . . . 8
↾s
|
52 | 51 | oveq2d 6666 |
. . . . . . 7
↾s
↾s
↾s
|
53 | 5 | ressinbas 15936 |
. . . . . . . 8
↾s ↾s |
54 | 45, 53 | syl 17 |
. . . . . . 7
↾s
↾s ↾s |
55 | 5 | ressinbas 15936 |
. . . . . . . 8
↾s
↾s
|
56 | 45, 33, 55 | 3syl 18 |
. . . . . . 7
↾s
↾s
↾s
|
57 | 52, 54, 56 | 3eqtr4d 2666 |
. . . . . 6
↾s
↾s ↾s |
58 | 43, 57 | eqtrd 2656 |
. . . . 5
↾s
↾s
↾s ↾s |
59 | 58 | ex 450 |
. . . 4
↾s
↾s
↾s ↾s |
60 | 4, 5 | ressid2 15928 |
. . . . . . . 8
↾s |
61 | 60 | 3adant3r3 1276 |
. . . . . . 7
↾s |
62 | 61 | oveq1d 6665 |
. . . . . 6
↾s
↾s ↾s |
63 | | inss2 3834 |
. . . . . . . . . . 11
|
64 | | simpl 473 |
. . . . . . . . . . 11
|
65 | 63, 64 | syl5ss 3614 |
. . . . . . . . . 10
|
66 | | sseqin2 3817 |
. . . . . . . . . 10
|
67 | 65, 66 | sylib 208 |
. . . . . . . . 9
|
68 | 8, 67 | syl5req 2669 |
. . . . . . . 8
|
69 | 68 | oveq2d 6666 |
. . . . . . 7
↾s
↾s |
70 | | simpr3 1069 |
. . . . . . . 8
|
71 | 5 | ressinbas 15936 |
. . . . . . . 8
↾s ↾s |
72 | 70, 71 | syl 17 |
. . . . . . 7
↾s ↾s |
73 | | simpr2 1068 |
. . . . . . . 8
|
74 | 73, 33, 55 | 3syl 18 |
. . . . . . 7
↾s ↾s |
75 | 69, 72, 74 | 3eqtr4d 2666 |
. . . . . 6
↾s ↾s |
76 | 62, 75 | eqtrd 2656 |
. . . . 5
↾s
↾s ↾s |
77 | 76 | ex 450 |
. . . 4
↾s
↾s ↾s |
78 | 39, 59, 77 | pm2.61ii 177 |
. . 3
↾s ↾s ↾s |
79 | 78 | 3expib 1268 |
. 2
↾s
↾s ↾s |
80 | | ress0 15934 |
. . . 4
↾s |
81 | | reldmress 15926 |
. . . . . 6
↾s |
82 | 81 | ovprc1 6684 |
. . . . 5
↾s |
83 | 82 | oveq1d 6665 |
. . . 4
↾s
↾s ↾s |
84 | 81 | ovprc1 6684 |
. . . 4
↾s |
85 | 80, 83, 84 | 3eqtr4a 2682 |
. . 3
↾s
↾s ↾s |
86 | 85 | a1d 25 |
. 2
↾s
↾s ↾s |
87 | 79, 86 | pm2.61i 176 |
1
↾s ↾s ↾s |