Step | Hyp | Ref
| Expression |
1 | | elutop 22037 |
. . . 4
UnifOn
unifTop
|
2 | 1 | simprbda 653 |
. . 3
UnifOn unifTop
|
3 | | restutop 22041 |
. . 3
UnifOn unifTop ↾t unifTop ↾t |
4 | 2, 3 | syldan 487 |
. 2
UnifOn unifTop
unifTop
↾t unifTop
↾t |
5 | | trust 22033 |
. . . . . . . . . . 11
UnifOn ↾t
UnifOn |
6 | 2, 5 | syldan 487 |
. . . . . . . . . 10
UnifOn unifTop
↾t UnifOn |
7 | | elutop 22037 |
. . . . . . . . . 10
↾t UnifOn unifTop ↾t
↾t |
8 | 6, 7 | syl 17 |
. . . . . . . . 9
UnifOn unifTop
unifTop ↾t
↾t |
9 | 8 | simprbda 653 |
. . . . . . . 8
UnifOn unifTop
unifTop ↾t |
10 | 2 | adantr 481 |
. . . . . . . 8
UnifOn unifTop
unifTop ↾t |
11 | 9, 10 | sstrd 3613 |
. . . . . . 7
UnifOn unifTop
unifTop ↾t |
12 | | simp-9l 816 |
. . . . . . . . . . . . 13
UnifOn unifTop
unifTop ↾t
↾t
UnifOn |
13 | | simplr 792 |
. . . . . . . . . . . . 13
UnifOn unifTop
unifTop ↾t
↾t
|
14 | | simp-4r 807 |
. . . . . . . . . . . . 13
UnifOn unifTop
unifTop ↾t
↾t
|
15 | | ustincl 22011 |
. . . . . . . . . . . . 13
UnifOn
|
16 | 12, 13, 14, 15 | syl3anc 1326 |
. . . . . . . . . . . 12
UnifOn unifTop
unifTop ↾t
↾t
|
17 | | inimass 5549 |
. . . . . . . . . . . . 13
|
18 | | ssrin 3838 |
. . . . . . . . . . . . . . . 16
|
19 | 18 | adantl 482 |
. . . . . . . . . . . . . . 15
UnifOn unifTop
unifTop ↾t
↾t
|
20 | | simpllr 799 |
. . . . . . . . . . . . . . . . 17
UnifOn unifTop
unifTop ↾t
↾t
|
21 | 20 | imaeq1d 5465 |
. . . . . . . . . . . . . . . 16
UnifOn unifTop
unifTop ↾t
↾t
|
22 | 9 | ad5antr 770 |
. . . . . . . . . . . . . . . . . . 19
UnifOn
unifTop
unifTop ↾t
↾t
|
23 | | simp-5r 809 |
. . . . . . . . . . . . . . . . . . 19
UnifOn
unifTop
unifTop ↾t
↾t
|
24 | 22, 23 | sseldd 3604 |
. . . . . . . . . . . . . . . . . 18
UnifOn
unifTop
unifTop ↾t
↾t
|
25 | 24 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
UnifOn unifTop
unifTop ↾t
↾t
|
26 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . 20
|
27 | | inimasn 5550 |
. . . . . . . . . . . . . . . . . . . 20
|
28 | 26, 27 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
|
29 | | xpimasn 5579 |
. . . . . . . . . . . . . . . . . . . 20
|
30 | 29 | ineq2d 3814 |
. . . . . . . . . . . . . . . . . . 19
|
31 | 28, 30 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . 18
|
32 | | incom 3805 |
. . . . . . . . . . . . . . . . . 18
|
33 | 31, 32 | syl6eq 2672 |
. . . . . . . . . . . . . . . . 17
|
34 | 25, 33 | syl 17 |
. . . . . . . . . . . . . . . 16
UnifOn unifTop
unifTop ↾t
↾t
|
35 | 21, 34 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
UnifOn unifTop
unifTop ↾t
↾t
|
36 | 19, 35 | sseqtr4d 3642 |
. . . . . . . . . . . . . 14
UnifOn unifTop
unifTop ↾t
↾t
|
37 | | simp-5r 809 |
. . . . . . . . . . . . . 14
UnifOn unifTop
unifTop ↾t
↾t
|
38 | 36, 37 | sstrd 3613 |
. . . . . . . . . . . . 13
UnifOn unifTop
unifTop ↾t
↾t
|
39 | 17, 38 | syl5ss 3614 |
. . . . . . . . . . . 12
UnifOn unifTop
unifTop ↾t
↾t
|
40 | | imaeq1 5461 |
. . . . . . . . . . . . . 14
|
41 | 40 | sseq1d 3632 |
. . . . . . . . . . . . 13
|
42 | 41 | rspcev 3309 |
. . . . . . . . . . . 12
|
43 | 16, 39, 42 | syl2anc 693 |
. . . . . . . . . . 11
UnifOn unifTop
unifTop ↾t
↾t
|
44 | | simp-4l 806 |
. . . . . . . . . . . . 13
UnifOn unifTop
unifTop ↾t
↾t UnifOn unifTop |
45 | 44 | ad2antrr 762 |
. . . . . . . . . . . 12
UnifOn
unifTop
unifTop ↾t
↾t
UnifOn
unifTop |
46 | 1 | simplbda 654 |
. . . . . . . . . . . . 13
UnifOn unifTop
|
47 | 46 | r19.21bi 2932 |
. . . . . . . . . . . 12
UnifOn unifTop
|
48 | 45, 24, 47 | syl2anc 693 |
. . . . . . . . . . 11
UnifOn
unifTop
unifTop ↾t
↾t
|
49 | 43, 48 | r19.29a 3078 |
. . . . . . . . . 10
UnifOn
unifTop
unifTop ↾t
↾t
|
50 | | simplr 792 |
. . . . . . . . . . 11
UnifOn unifTop
unifTop ↾t
↾t
↾t |
51 | | sqxpexg 6963 |
. . . . . . . . . . . . 13
unifTop
|
52 | | elrest 16088 |
. . . . . . . . . . . . 13
UnifOn ↾t
|
53 | 51, 52 | sylan2 491 |
. . . . . . . . . . . 12
UnifOn unifTop
↾t
|
54 | 53 | biimpa 501 |
. . . . . . . . . . 11
UnifOn unifTop
↾t
|
55 | 44, 50, 54 | syl2anc 693 |
. . . . . . . . . 10
UnifOn unifTop
unifTop ↾t
↾t
|
56 | 49, 55 | r19.29a 3078 |
. . . . . . . . 9
UnifOn unifTop
unifTop ↾t
↾t
|
57 | 8 | simplbda 654 |
. . . . . . . . . 10
UnifOn unifTop
unifTop ↾t
↾t |
58 | 57 | r19.21bi 2932 |
. . . . . . . . 9
UnifOn
unifTop
unifTop ↾t
↾t |
59 | 56, 58 | r19.29a 3078 |
. . . . . . . 8
UnifOn
unifTop
unifTop ↾t
|
60 | 59 | ralrimiva 2966 |
. . . . . . 7
UnifOn unifTop
unifTop ↾t
|
61 | | elutop 22037 |
. . . . . . . 8
UnifOn
unifTop
|
62 | 61 | ad2antrr 762 |
. . . . . . 7
UnifOn unifTop
unifTop ↾t unifTop |
63 | 11, 60, 62 | mpbir2and 957 |
. . . . . 6
UnifOn unifTop
unifTop ↾t unifTop |
64 | | df-ss 3588 |
. . . . . . . 8
|
65 | 9, 64 | sylib 208 |
. . . . . . 7
UnifOn unifTop
unifTop ↾t
|
66 | 65 | eqcomd 2628 |
. . . . . 6
UnifOn unifTop
unifTop ↾t |
67 | | ineq1 3807 |
. . . . . . . 8
|
68 | 67 | eqeq2d 2632 |
. . . . . . 7
|
69 | 68 | rspcev 3309 |
. . . . . 6
unifTop
unifTop |
70 | 63, 66, 69 | syl2anc 693 |
. . . . 5
UnifOn unifTop
unifTop ↾t unifTop |
71 | | fvex 6201 |
. . . . . . 7
unifTop |
72 | | elrest 16088 |
. . . . . . 7
unifTop unifTop
unifTop ↾t
unifTop |
73 | 71, 72 | mpan 706 |
. . . . . 6
unifTop
unifTop ↾t
unifTop |
74 | 73 | ad2antlr 763 |
. . . . 5
UnifOn unifTop
unifTop ↾t unifTop
↾t
unifTop |
75 | 70, 74 | mpbird 247 |
. . . 4
UnifOn unifTop
unifTop ↾t unifTop ↾t |
76 | 75 | ex 450 |
. . 3
UnifOn unifTop
unifTop ↾t
unifTop ↾t |
77 | 76 | ssrdv 3609 |
. 2
UnifOn unifTop
unifTop ↾t
unifTop ↾t |
78 | 4, 77 | eqssd 3620 |
1
UnifOn unifTop
unifTop
↾t unifTop
↾t |