Step | Hyp | Ref
| Expression |
1 | | simpr 477 |
. . . . 5
|
2 | | sseqin2 3817 |
. . . . 5
|
3 | 1, 2 | sylib 208 |
. . . 4
|
4 | | simpl 473 |
. . . . 5
|
5 | | id 22 |
. . . . . 6
|
6 | | filtop 21659 |
. . . . . 6
|
7 | | ssexg 4804 |
. . . . . 6
|
8 | 5, 6, 7 | syl2anr 495 |
. . . . 5
|
9 | 6 | adantr 481 |
. . . . 5
|
10 | | elrestr 16089 |
. . . . 5
↾t |
11 | 4, 8, 9, 10 | syl3anc 1326 |
. . . 4
↾t |
12 | 3, 11 | eqeltrrd 2702 |
. . 3
↾t |
13 | | elpwi 4168 |
. . . . 5
|
14 | | vex 3203 |
. . . . . . . . . 10
|
15 | 14 | inex1 4799 |
. . . . . . . . 9
|
16 | 15 | a1i 11 |
. . . . . . . 8
|
17 | | elrest 16088 |
. . . . . . . . . 10
↾t
|
18 | 8, 17 | syldan 487 |
. . . . . . . . 9
↾t
|
19 | 18 | adantr 481 |
. . . . . . . 8
↾t
|
20 | | simpr 477 |
. . . . . . . . 9
|
21 | 20 | sseq1d 3632 |
. . . . . . . 8
|
22 | 16, 19, 21 | rexxfr2d 4883 |
. . . . . . 7
↾t |
23 | | indir 3875 |
. . . . . . . . . 10
|
24 | | simplr 792 |
. . . . . . . . . . . . 13
|
25 | | df-ss 3588 |
. . . . . . . . . . . . 13
|
26 | 24, 25 | sylib 208 |
. . . . . . . . . . . 12
|
27 | 26 | uneq2d 3767 |
. . . . . . . . . . 11
|
28 | | simprr 796 |
. . . . . . . . . . . 12
|
29 | | ssequn1 3783 |
. . . . . . . . . . . 12
|
30 | 28, 29 | sylib 208 |
. . . . . . . . . . 11
|
31 | 27, 30 | eqtrd 2656 |
. . . . . . . . . 10
|
32 | 23, 31 | syl5eq 2668 |
. . . . . . . . 9
|
33 | | simplll 798 |
. . . . . . . . . 10
|
34 | | simpllr 799 |
. . . . . . . . . . 11
|
35 | 33, 34, 8 | syl2anc 693 |
. . . . . . . . . 10
|
36 | | simprl 794 |
. . . . . . . . . . 11
|
37 | | filelss 21656 |
. . . . . . . . . . . . 13
|
38 | 33, 36, 37 | syl2anc 693 |
. . . . . . . . . . . 12
|
39 | 24, 34 | sstrd 3613 |
. . . . . . . . . . . 12
|
40 | 38, 39 | unssd 3789 |
. . . . . . . . . . 11
|
41 | | ssun1 3776 |
. . . . . . . . . . . 12
|
42 | 41 | a1i 11 |
. . . . . . . . . . 11
|
43 | | filss 21657 |
. . . . . . . . . . 11
|
44 | 33, 36, 40, 42, 43 | syl13anc 1328 |
. . . . . . . . . 10
|
45 | | elrestr 16089 |
. . . . . . . . . 10
↾t |
46 | 33, 35, 44, 45 | syl3anc 1326 |
. . . . . . . . 9
↾t |
47 | 32, 46 | eqeltrrd 2702 |
. . . . . . . 8
↾t |
48 | 47 | rexlimdvaa 3032 |
. . . . . . 7
↾t |
49 | 22, 48 | sylbid 230 |
. . . . . 6
↾t ↾t |
50 | 49 | ex 450 |
. . . . 5
↾t ↾t |
51 | 13, 50 | syl5 34 |
. . . 4
↾t ↾t |
52 | 51 | ralrimiv 2965 |
. . 3
↾t ↾t |
53 | | simpll 790 |
. . . . . 6
|
54 | 8 | adantr 481 |
. . . . . 6
|
55 | | filin 21658 |
. . . . . . . 8
|
56 | 55 | 3expb 1266 |
. . . . . . 7
|
57 | 56 | adantlr 751 |
. . . . . 6
|
58 | | elrestr 16089 |
. . . . . 6
↾t |
59 | 53, 54, 57, 58 | syl3anc 1326 |
. . . . 5
↾t |
60 | 59 | ralrimivva 2971 |
. . . 4
↾t |
61 | | vex 3203 |
. . . . . . 7
|
62 | 61 | inex1 4799 |
. . . . . 6
|
63 | 62 | a1i 11 |
. . . . 5
|
64 | | elrest 16088 |
. . . . . 6
↾t
|
65 | 8, 64 | syldan 487 |
. . . . 5
↾t
|
66 | 15 | a1i 11 |
. . . . . 6
|
67 | 18 | adantr 481 |
. . . . . 6
↾t
|
68 | | ineq12 3809 |
. . . . . . . . 9
|
69 | | inindir 3831 |
. . . . . . . . 9
|
70 | 68, 69 | syl6eqr 2674 |
. . . . . . . 8
|
71 | 70 | adantll 750 |
. . . . . . 7
|
72 | 71 | eleq1d 2686 |
. . . . . 6
↾t
↾t |
73 | 66, 67, 72 | ralxfr2d 4882 |
. . . . 5
↾t
↾t
↾t |
74 | 63, 65, 73 | ralxfr2d 4882 |
. . . 4
↾t
↾t
↾t
↾t |
75 | 60, 74 | mpbird 247 |
. . 3
↾t
↾t
↾t |
76 | | isfil2 21660 |
. . . . . 6
↾t ↾t
↾t
↾t
↾t ↾t ↾t
↾t
↾t |
77 | | restsspw 16092 |
. . . . . . . 8
↾t
|
78 | | 3anass 1042 |
. . . . . . . 8
↾t ↾t
↾t
↾t ↾t
↾t |
79 | 77, 78 | mpbiran 953 |
. . . . . . 7
↾t ↾t
↾t
↾t ↾t |
80 | 79 | 3anbi1i 1253 |
. . . . . 6
↾t ↾t ↾t
↾t ↾t ↾t
↾t
↾t
↾t
↾t
↾t ↾t ↾t
↾t
↾t |
81 | | 3anass 1042 |
. . . . . 6
↾t
↾t
↾t ↾t ↾t
↾t
↾t
↾t
↾t
↾t ↾t ↾t
↾t
↾t |
82 | 76, 80, 81 | 3bitri 286 |
. . . . 5
↾t ↾t
↾t
↾t ↾t ↾t
↾t
↾t |
83 | | anass 681 |
. . . . 5
↾t
↾t
↾t ↾t ↾t
↾t
↾t ↾t
↾t
↾t ↾t ↾t
↾t
↾t |
84 | | ancom 466 |
. . . . 5
↾t ↾t ↾t ↾t
↾t
↾t
↾t ↾t ↾t ↾t
↾t
↾t
↾t ↾t |
85 | 82, 83, 84 | 3bitri 286 |
. . . 4
↾t
↾t
↾t ↾t ↾t
↾t
↾t ↾t |
86 | 85 | baib 944 |
. . 3
↾t
↾t ↾t ↾t
↾t
↾t ↾t
↾t |
87 | 12, 52, 75, 86 | syl12anc 1324 |
. 2
↾t ↾t |
88 | | nesym 2850 |
. . . 4
|
89 | 88 | ralbii 2980 |
. . 3
|
90 | | elrest 16088 |
. . . . . 6
↾t
|
91 | 8, 90 | syldan 487 |
. . . . 5
↾t
|
92 | | dfrex2 2996 |
. . . . 5
|
93 | 91, 92 | syl6bb 276 |
. . . 4
↾t |
94 | 93 | con2bid 344 |
. . 3
↾t |
95 | 89, 94 | syl5bb 272 |
. 2
↾t |
96 | 87, 95 | bitr4d 271 |
1
↾t
|