Step | Hyp | Ref
| Expression |
1 | | simpr 477 |
. . . . . . 7
UnifOn unifTop
unifTop |
2 | | utopval 22036 |
. . . . . . . . 9
UnifOn
unifTop
|
3 | | ssrab2 3687 |
. . . . . . . . 9
|
4 | 2, 3 | syl6eqss 3655 |
. . . . . . . 8
UnifOn
unifTop
|
5 | 4 | adantr 481 |
. . . . . . 7
UnifOn unifTop
unifTop
|
6 | 1, 5 | sstrd 3613 |
. . . . . 6
UnifOn unifTop
|
7 | | sspwuni 4611 |
. . . . . 6
|
8 | 6, 7 | sylib 208 |
. . . . 5
UnifOn unifTop
|
9 | | simp-4l 806 |
. . . . . . . . 9
UnifOn
unifTop
UnifOn |
10 | | simp-4r 807 |
. . . . . . . . . 10
UnifOn
unifTop
unifTop |
11 | | simplr 792 |
. . . . . . . . . 10
UnifOn
unifTop
|
12 | 10, 11 | sseldd 3604 |
. . . . . . . . 9
UnifOn
unifTop
unifTop |
13 | | simpr 477 |
. . . . . . . . 9
UnifOn
unifTop
|
14 | | elutop 22037 |
. . . . . . . . . . . 12
UnifOn
unifTop
|
15 | 14 | biimpa 501 |
. . . . . . . . . . 11
UnifOn unifTop
|
16 | 15 | simprd 479 |
. . . . . . . . . 10
UnifOn unifTop
|
17 | 16 | r19.21bi 2932 |
. . . . . . . . 9
UnifOn unifTop
|
18 | 9, 12, 13, 17 | syl21anc 1325 |
. . . . . . . 8
UnifOn
unifTop
|
19 | | r19.41v 3089 |
. . . . . . . . 9
|
20 | | ssuni 4459 |
. . . . . . . . . 10
|
21 | 20 | reximi 3011 |
. . . . . . . . 9
|
22 | 19, 21 | sylbir 225 |
. . . . . . . 8
|
23 | 18, 11, 22 | syl2anc 693 |
. . . . . . 7
UnifOn
unifTop
|
24 | | eluni2 4440 |
. . . . . . . . 9
|
25 | 24 | biimpi 206 |
. . . . . . . 8
|
26 | 25 | adantl 482 |
. . . . . . 7
UnifOn unifTop
|
27 | 23, 26 | r19.29a 3078 |
. . . . . 6
UnifOn unifTop
|
28 | 27 | ralrimiva 2966 |
. . . . 5
UnifOn unifTop
|
29 | | elutop 22037 |
. . . . . 6
UnifOn
unifTop
|
30 | 29 | adantr 481 |
. . . . 5
UnifOn unifTop
unifTop
|
31 | 8, 28, 30 | mpbir2and 957 |
. . . 4
UnifOn unifTop
unifTop |
32 | 31 | ex 450 |
. . 3
UnifOn
unifTop unifTop |
33 | 32 | alrimiv 1855 |
. 2
UnifOn
unifTop unifTop |
34 | | elutop 22037 |
. . . . . . . 8
UnifOn
unifTop
|
35 | 34 | biimpa 501 |
. . . . . . 7
UnifOn unifTop
|
36 | 35 | simpld 475 |
. . . . . 6
UnifOn unifTop
|
37 | 36 | adantrr 753 |
. . . . 5
UnifOn unifTop
unifTop
|
38 | | ssinss1 3841 |
. . . . 5
|
39 | 37, 38 | syl 17 |
. . . 4
UnifOn unifTop
unifTop
|
40 | | simpl 473 |
. . . . . . . . . 10
UnifOn unifTop unifTop
UnifOn |
41 | | simpr31 1151 |
. . . . . . . . . 10
UnifOn unifTop unifTop
|
42 | | simpr32 1152 |
. . . . . . . . . 10
UnifOn unifTop unifTop
|
43 | | ustincl 22011 |
. . . . . . . . . 10
UnifOn
|
44 | 40, 41, 42, 43 | syl3anc 1326 |
. . . . . . . . 9
UnifOn unifTop unifTop
|
45 | | inss1 3833 |
. . . . . . . . . . . 12
|
46 | | imass1 5500 |
. . . . . . . . . . . 12
|
47 | 45, 46 | ax-mp 5 |
. . . . . . . . . . 11
|
48 | | simpr33 1153 |
. . . . . . . . . . . 12
UnifOn unifTop unifTop
|
49 | 48 | simpld 475 |
. . . . . . . . . . 11
UnifOn unifTop unifTop
|
50 | 47, 49 | syl5ss 3614 |
. . . . . . . . . 10
UnifOn unifTop unifTop
|
51 | | inss2 3834 |
. . . . . . . . . . . 12
|
52 | | imass1 5500 |
. . . . . . . . . . . 12
|
53 | 51, 52 | ax-mp 5 |
. . . . . . . . . . 11
|
54 | 48 | simprd 479 |
. . . . . . . . . . 11
UnifOn unifTop unifTop
|
55 | 53, 54 | syl5ss 3614 |
. . . . . . . . . 10
UnifOn unifTop unifTop
|
56 | 50, 55 | ssind 3837 |
. . . . . . . . 9
UnifOn unifTop unifTop
|
57 | | imaeq1 5461 |
. . . . . . . . . . 11
|
58 | 57 | sseq1d 3632 |
. . . . . . . . . 10
|
59 | 58 | rspcev 3309 |
. . . . . . . . 9
|
60 | 44, 56, 59 | syl2anc 693 |
. . . . . . . 8
UnifOn unifTop unifTop
|
61 | 60 | 3anassrs 1290 |
. . . . . . 7
UnifOn unifTop unifTop
|
62 | 61 | 3anassrs 1290 |
. . . . . 6
UnifOn unifTop
unifTop
|
63 | | simpll 790 |
. . . . . . . 8
UnifOn unifTop
unifTop UnifOn |
64 | | simplrl 800 |
. . . . . . . 8
UnifOn unifTop
unifTop unifTop |
65 | | simpr 477 |
. . . . . . . . . 10
UnifOn unifTop
unifTop |
66 | | elin 3796 |
. . . . . . . . . 10
|
67 | 65, 66 | sylib 208 |
. . . . . . . . 9
UnifOn unifTop
unifTop
|
68 | 67 | simpld 475 |
. . . . . . . 8
UnifOn unifTop
unifTop |
69 | 35 | simprd 479 |
. . . . . . . . 9
UnifOn unifTop
|
70 | 69 | r19.21bi 2932 |
. . . . . . . 8
UnifOn unifTop
|
71 | 63, 64, 68, 70 | syl21anc 1325 |
. . . . . . 7
UnifOn unifTop
unifTop
|
72 | | simplrr 801 |
. . . . . . . 8
UnifOn unifTop
unifTop unifTop |
73 | 67 | simprd 479 |
. . . . . . . 8
UnifOn unifTop
unifTop |
74 | 63, 72, 73, 17 | syl21anc 1325 |
. . . . . . 7
UnifOn unifTop
unifTop
|
75 | | reeanv 3107 |
. . . . . . 7
|
76 | 71, 74, 75 | sylanbrc 698 |
. . . . . 6
UnifOn unifTop
unifTop
|
77 | 62, 76 | r19.29vva 3081 |
. . . . 5
UnifOn unifTop
unifTop
|
78 | 77 | ralrimiva 2966 |
. . . 4
UnifOn unifTop
unifTop
|
79 | | elutop 22037 |
. . . . 5
UnifOn
unifTop
|
80 | 79 | adantr 481 |
. . . 4
UnifOn unifTop
unifTop
unifTop
|
81 | 39, 78, 80 | mpbir2and 957 |
. . 3
UnifOn unifTop
unifTop
unifTop |
82 | 81 | ralrimivva 2971 |
. 2
UnifOn
unifTop
unifTop unifTop |
83 | | fvex 6201 |
. . 3
unifTop |
84 | | istopg 20700 |
. . 3
unifTop unifTop
unifTop
unifTop unifTop unifTop unifTop |
85 | 83, 84 | ax-mp 5 |
. 2
unifTop unifTop
unifTop unifTop unifTop unifTop |
86 | 33, 82, 85 | sylanbrc 698 |
1
UnifOn
unifTop |