Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. . . 4
UnifOn unifTop ↾t UnifOn |
2 | | fvexd 6203 |
. . . . . . 7
UnifOn unifTop |
3 | | elfvex 6221 |
. . . . . . . . 9
UnifOn
|
4 | 3 | adantr 481 |
. . . . . . . 8
UnifOn |
5 | | simpr 477 |
. . . . . . . 8
UnifOn |
6 | 4, 5 | ssexd 4805 |
. . . . . . 7
UnifOn |
7 | | elrest 16088 |
. . . . . . 7
unifTop unifTop
↾t
unifTop |
8 | 2, 6, 7 | syl2anc 693 |
. . . . . 6
UnifOn unifTop
↾t
unifTop |
9 | 8 | biimpa 501 |
. . . . 5
UnifOn unifTop ↾t
unifTop |
10 | | inss2 3834 |
. . . . . . 7
|
11 | | sseq1 3626 |
. . . . . . 7
|
12 | 10, 11 | mpbiri 248 |
. . . . . 6
|
13 | 12 | rexlimivw 3029 |
. . . . 5
unifTop |
14 | 9, 13 | syl 17 |
. . . 4
UnifOn unifTop ↾t
|
15 | | simp-5l 808 |
. . . . . . . . . 10
UnifOn unifTop ↾t
unifTop
UnifOn |
16 | 15 | ad2antrr 762 |
. . . . . . . . 9
UnifOn
unifTop ↾t unifTop
UnifOn |
17 | 6 | ad6antr 772 |
. . . . . . . . . 10
UnifOn
unifTop ↾t unifTop
|
18 | | xpexg 6960 |
. . . . . . . . . 10
|
19 | 17, 17, 18 | syl2anc 693 |
. . . . . . . . 9
UnifOn
unifTop ↾t unifTop
|
20 | | simplr 792 |
. . . . . . . . 9
UnifOn
unifTop ↾t unifTop
|
21 | | elrestr 16089 |
. . . . . . . . 9
UnifOn
↾t |
22 | 16, 19, 20, 21 | syl3anc 1326 |
. . . . . . . 8
UnifOn
unifTop ↾t unifTop
↾t |
23 | | inss1 3833 |
. . . . . . . . . . . . 13
|
24 | | imass1 5500 |
. . . . . . . . . . . . 13
|
25 | 23, 24 | ax-mp 5 |
. . . . . . . . . . . 12
|
26 | | sstr 3611 |
. . . . . . . . . . . 12
|
27 | 25, 26 | mpan 706 |
. . . . . . . . . . 11
|
28 | | imassrn 5477 |
. . . . . . . . . . . . . . 15
|
29 | | rnin 5542 |
. . . . . . . . . . . . . . 15
|
30 | 28, 29 | sstri 3612 |
. . . . . . . . . . . . . 14
|
31 | | inss2 3834 |
. . . . . . . . . . . . . 14
|
32 | 30, 31 | sstri 3612 |
. . . . . . . . . . . . 13
|
33 | | rnxpid 5567 |
. . . . . . . . . . . . 13
|
34 | 32, 33 | sseqtri 3637 |
. . . . . . . . . . . 12
|
35 | 34 | a1i 11 |
. . . . . . . . . . 11
|
36 | 27, 35 | ssind 3837 |
. . . . . . . . . 10
|
37 | 36 | adantl 482 |
. . . . . . . . 9
UnifOn
unifTop ↾t unifTop
|
38 | | simpllr 799 |
. . . . . . . . 9
UnifOn
unifTop ↾t unifTop
|
39 | 37, 38 | sseqtr4d 3642 |
. . . . . . . 8
UnifOn
unifTop ↾t unifTop
|
40 | | imaeq1 5461 |
. . . . . . . . . 10
|
41 | 40 | sseq1d 3632 |
. . . . . . . . 9
|
42 | 41 | rspcev 3309 |
. . . . . . . 8
↾t
↾t
|
43 | 22, 39, 42 | syl2anc 693 |
. . . . . . 7
UnifOn
unifTop ↾t unifTop
↾t |
44 | | simplr 792 |
. . . . . . . 8
UnifOn unifTop ↾t
unifTop
unifTop |
45 | | inss1 3833 |
. . . . . . . . 9
|
46 | | simpllr 799 |
. . . . . . . . . 10
UnifOn unifTop ↾t
unifTop
|
47 | | simpr 477 |
. . . . . . . . . 10
UnifOn unifTop ↾t
unifTop
|
48 | 46, 47 | eleqtrd 2703 |
. . . . . . . . 9
UnifOn unifTop ↾t
unifTop
|
49 | 45, 48 | sseldi 3601 |
. . . . . . . 8
UnifOn unifTop ↾t
unifTop
|
50 | | elutop 22037 |
. . . . . . . . . 10
UnifOn
unifTop
|
51 | 50 | simplbda 654 |
. . . . . . . . 9
UnifOn unifTop
|
52 | 51 | r19.21bi 2932 |
. . . . . . . 8
UnifOn unifTop
|
53 | 15, 44, 49, 52 | syl21anc 1325 |
. . . . . . 7
UnifOn unifTop ↾t
unifTop
|
54 | 43, 53 | r19.29a 3078 |
. . . . . 6
UnifOn unifTop ↾t
unifTop
↾t
|
55 | 9 | adantr 481 |
. . . . . 6
UnifOn
unifTop ↾t unifTop |
56 | 54, 55 | r19.29a 3078 |
. . . . 5
UnifOn
unifTop ↾t
↾t |
57 | 56 | ralrimiva 2966 |
. . . 4
UnifOn unifTop ↾t
↾t
|
58 | | trust 22033 |
. . . . . 6
UnifOn ↾t
UnifOn |
59 | | elutop 22037 |
. . . . . 6
↾t UnifOn unifTop ↾t
↾t |
60 | 58, 59 | syl 17 |
. . . . 5
UnifOn unifTop ↾t
↾t |
61 | 60 | biimpar 502 |
. . . 4
UnifOn
↾t unifTop ↾t
|
62 | 1, 14, 57, 61 | syl12anc 1324 |
. . 3
UnifOn unifTop ↾t unifTop ↾t
|
63 | 62 | ex 450 |
. 2
UnifOn unifTop
↾t unifTop ↾t |
64 | 63 | ssrdv 3609 |
1
UnifOn unifTop ↾t unifTop ↾t |