Step | Hyp | Ref
| Expression |
1 | | ufilfil 21708 |
. . . 4
↾t
↾t |
2 | | ufilfil 21708 |
. . . . 5
|
3 | | trfil3 21692 |
. . . . 5
↾t |
4 | 2, 3 | sylan 488 |
. . . 4
↾t |
5 | 1, 4 | syl5ib 234 |
. . 3
↾t |
6 | 4 | biimprd 238 |
. . . . 5
↾t |
7 | | elpwi 4168 |
. . . . . . 7
|
8 | | simpll 790 |
. . . . . . . . 9
|
9 | | simpr 477 |
. . . . . . . . . 10
|
10 | | simplr 792 |
. . . . . . . . . 10
|
11 | 9, 10 | sstrd 3613 |
. . . . . . . . 9
|
12 | | ufilss 21709 |
. . . . . . . . 9
|
13 | 8, 11, 12 | syl2anc 693 |
. . . . . . . 8
|
14 | | id 22 |
. . . . . . . . . . . . 13
|
15 | | elfvdm 6220 |
. . . . . . . . . . . . 13
|
16 | | ssexg 4804 |
. . . . . . . . . . . . 13
|
17 | 14, 15, 16 | syl2anr 495 |
. . . . . . . . . . . 12
|
18 | | elrestr 16089 |
. . . . . . . . . . . . 13
↾t |
19 | 18 | 3expia 1267 |
. . . . . . . . . . . 12
↾t |
20 | 17, 19 | syldan 487 |
. . . . . . . . . . 11
↾t |
21 | 20 | adantr 481 |
. . . . . . . . . 10
↾t |
22 | | df-ss 3588 |
. . . . . . . . . . . 12
|
23 | 9, 22 | sylib 208 |
. . . . . . . . . . 11
|
24 | 23 | eleq1d 2686 |
. . . . . . . . . 10
↾t
↾t |
25 | 21, 24 | sylibd 229 |
. . . . . . . . 9
↾t |
26 | | indif1 3871 |
. . . . . . . . . . . 12
|
27 | | simplr 792 |
. . . . . . . . . . . . . 14
|
28 | | sseqin2 3817 |
. . . . . . . . . . . . . 14
|
29 | 27, 28 | sylib 208 |
. . . . . . . . . . . . 13
|
30 | 29 | difeq1d 3727 |
. . . . . . . . . . . 12
|
31 | 26, 30 | syl5eq 2668 |
. . . . . . . . . . 11
|
32 | | simpll 790 |
. . . . . . . . . . . 12
|
33 | 17 | adantr 481 |
. . . . . . . . . . . 12
|
34 | | simprr 796 |
. . . . . . . . . . . 12
|
35 | | elrestr 16089 |
. . . . . . . . . . . 12
↾t |
36 | 32, 33, 34, 35 | syl3anc 1326 |
. . . . . . . . . . 11
↾t |
37 | 31, 36 | eqeltrrd 2702 |
. . . . . . . . . 10
↾t |
38 | 37 | expr 643 |
. . . . . . . . 9
↾t |
39 | 25, 38 | orim12d 883 |
. . . . . . . 8
↾t
↾t |
40 | 13, 39 | mpd 15 |
. . . . . . 7
↾t
↾t |
41 | 7, 40 | sylan2 491 |
. . . . . 6
↾t
↾t |
42 | 41 | ralrimiva 2966 |
. . . . 5
↾t ↾t |
43 | 6, 42 | jctird 567 |
. . . 4
↾t
↾t ↾t |
44 | | isufil 21707 |
. . . 4
↾t
↾t ↾t ↾t |
45 | 43, 44 | syl6ibr 242 |
. . 3
↾t |
46 | 5, 45 | impbid 202 |
. 2
↾t |
47 | | ufilb 21710 |
. . 3
|
48 | 47 | con1bid 345 |
. 2
|
49 | 46, 48 | bitrd 268 |
1
↾t |