Step | Hyp | Ref
| Expression |
1 | | simp1 1061 |
. . . . 5
UnifOn
CauFilu
↾t
UnifOn |
2 | | simp2l 1087 |
. . . . 5
UnifOn
CauFilu
↾t
CauFilu |
3 | | iscfilu 22092 |
. . . . . 6
UnifOn
CauFilu
|
4 | 3 | biimpa 501 |
. . . . 5
UnifOn CauFilu
|
5 | 1, 2, 4 | syl2anc 693 |
. . . 4
UnifOn
CauFilu
↾t
|
6 | 5 | simpld 475 |
. . 3
UnifOn
CauFilu
↾t
|
7 | | simp3 1063 |
. . 3
UnifOn
CauFilu
↾t |
8 | | simp2r 1088 |
. . 3
UnifOn
CauFilu
↾t ↾t |
9 | | trfbas2 21647 |
. . . 4
↾t ↾t |
10 | 9 | biimpar 502 |
. . 3
↾t
↾t |
11 | 6, 7, 8, 10 | syl21anc 1325 |
. 2
UnifOn
CauFilu
↾t
↾t |
12 | 2 | ad5antr 770 |
. . . . . . 7
UnifOn
CauFilu
↾t
↾t
CauFilu |
13 | 1 | adantr 481 |
. . . . . . . . . 10
UnifOn
CauFilu
↾t
↾t
UnifOn |
14 | 13 | elfvexd 6222 |
. . . . . . . . 9
UnifOn
CauFilu
↾t
↾t
|
15 | 7 | adantr 481 |
. . . . . . . . 9
UnifOn
CauFilu
↾t
↾t
|
16 | 14, 15 | ssexd 4805 |
. . . . . . . 8
UnifOn
CauFilu
↾t
↾t
|
17 | 16 | ad4antr 768 |
. . . . . . 7
UnifOn
CauFilu
↾t
↾t
|
18 | | simplr 792 |
. . . . . . 7
UnifOn
CauFilu
↾t
↾t
|
19 | | elrestr 16089 |
. . . . . . 7
CauFilu
↾t |
20 | 12, 17, 18, 19 | syl3anc 1326 |
. . . . . 6
UnifOn
CauFilu
↾t
↾t
↾t |
21 | | inxp 5254 |
. . . . . . 7
|
22 | | simpr 477 |
. . . . . . . . 9
UnifOn
CauFilu
↾t
↾t
|
23 | | ssrin 3838 |
. . . . . . . . 9
|
24 | 22, 23 | syl 17 |
. . . . . . . 8
UnifOn
CauFilu
↾t
↾t
|
25 | | simpllr 799 |
. . . . . . . 8
UnifOn
CauFilu
↾t
↾t
|
26 | 24, 25 | sseqtr4d 3642 |
. . . . . . 7
UnifOn
CauFilu
↾t
↾t
|
27 | 21, 26 | syl5eqssr 3650 |
. . . . . 6
UnifOn
CauFilu
↾t
↾t
|
28 | | id 22 |
. . . . . . . . 9
|
29 | 28 | sqxpeqd 5141 |
. . . . . . . 8
|
30 | 29 | sseq1d 3632 |
. . . . . . 7
|
31 | 30 | rspcev 3309 |
. . . . . 6
↾t
↾t |
32 | 20, 27, 31 | syl2anc 693 |
. . . . 5
UnifOn
CauFilu
↾t
↾t
↾t |
33 | 5 | simprd 479 |
. . . . . . . 8
UnifOn
CauFilu
↾t
|
34 | 33 | r19.21bi 2932 |
. . . . . . 7
UnifOn
CauFilu
↾t
|
35 | 34 | 3ad2antr2 1227 |
. . . . . 6
UnifOn
CauFilu
↾t
↾t
|
36 | 35 | 3anassrs 1290 |
. . . . 5
UnifOn
CauFilu ↾t
↾t
|
37 | 32, 36 | r19.29a 3078 |
. . . 4
UnifOn
CauFilu ↾t
↾t
↾t |
38 | | xpexg 6960 |
. . . . . 6
|
39 | 16, 16, 38 | syl2anc 693 |
. . . . 5
UnifOn
CauFilu
↾t
↾t
|
40 | | simpr 477 |
. . . . 5
UnifOn
CauFilu
↾t
↾t
↾t |
41 | | elrest 16088 |
. . . . . 6
UnifOn ↾t
|
42 | 41 | biimpa 501 |
. . . . 5
UnifOn
↾t
|
43 | 13, 39, 40, 42 | syl21anc 1325 |
. . . 4
UnifOn
CauFilu
↾t
↾t
|
44 | 37, 43 | r19.29a 3078 |
. . 3
UnifOn
CauFilu
↾t
↾t
↾t |
45 | 44 | ralrimiva 2966 |
. 2
UnifOn
CauFilu
↾t
↾t
↾t |
46 | | trust 22033 |
. . . 4
UnifOn ↾t
UnifOn |
47 | 1, 7, 46 | syl2anc 693 |
. . 3
UnifOn
CauFilu
↾t
↾t UnifOn |
48 | | iscfilu 22092 |
. . 3
↾t UnifOn
↾t CauFilu
↾t ↾t
↾t ↾t |
49 | 47, 48 | syl 17 |
. 2
UnifOn
CauFilu
↾t ↾t CauFilu ↾t ↾t
↾t ↾t |
50 | 11, 45, 49 | mpbir2and 957 |
1
UnifOn
CauFilu
↾t
↾t CauFilu
↾t |