Step | Hyp | Ref
| Expression |
1 | | ishaus2 21155 |
. 2
TopOn
|
2 | | topontop 20718 |
. . 3
TopOn
|
3 | | simp1 1061 |
. . . . . . . . . . . 12
|
4 | 3 | adantr 481 |
. . . . . . . . . . 11
|
5 | | simp2 1062 |
. . . . . . . . . . . 12
|
6 | 5 | adantr 481 |
. . . . . . . . . . 11
|
7 | | simp1 1061 |
. . . . . . . . . . . 12
|
8 | 7 | adantl 482 |
. . . . . . . . . . 11
|
9 | | opnneip 20923 |
. . . . . . . . . . 11
|
10 | 4, 6, 8, 9 | syl3anc 1326 |
. . . . . . . . . 10
|
11 | | simp3 1063 |
. . . . . . . . . . . 12
|
12 | 11 | adantr 481 |
. . . . . . . . . . 11
|
13 | | simp2 1062 |
. . . . . . . . . . . 12
|
14 | 13 | adantl 482 |
. . . . . . . . . . 11
|
15 | | opnneip 20923 |
. . . . . . . . . . 11
|
16 | 4, 12, 14, 15 | syl3anc 1326 |
. . . . . . . . . 10
|
17 | | simp3 1063 |
. . . . . . . . . . 11
|
18 | 17 | adantl 482 |
. . . . . . . . . 10
|
19 | | ineq1 3807 |
. . . . . . . . . . . 12
|
20 | 19 | eqeq1d 2624 |
. . . . . . . . . . 11
|
21 | | ineq2 3808 |
. . . . . . . . . . . 12
|
22 | 21 | eqeq1d 2624 |
. . . . . . . . . . 11
|
23 | 20, 22 | rspc2ev 3324 |
. . . . . . . . . 10
|
24 | 10, 16, 18, 23 | syl3anc 1326 |
. . . . . . . . 9
|
25 | 24 | ex 450 |
. . . . . . . 8
|
26 | 25 | 3expib 1268 |
. . . . . . 7
|
27 | 26 | rexlimdvv 3037 |
. . . . . 6
|
28 | | neii2 20912 |
. . . . . . . . 9
|
29 | 28 | ex 450 |
. . . . . . . 8
|
30 | | neii2 20912 |
. . . . . . . . 9
|
31 | 30 | ex 450 |
. . . . . . . 8
|
32 | | vex 3203 |
. . . . . . . . . . . . . . 15
|
33 | 32 | snss 4316 |
. . . . . . . . . . . . . 14
|
34 | 33 | anbi1i 731 |
. . . . . . . . . . . . 13
|
35 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
36 | 35 | snss 4316 |
. . . . . . . . . . . . . . . . . . . . . 22
|
37 | 36 | anbi1i 731 |
. . . . . . . . . . . . . . . . . . . . 21
|
38 | | simp1l 1085 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
39 | | simp2l 1087 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
40 | | ss2in 3840 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
41 | | ssn0 3976 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
42 | 41 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
43 | 42 | necon4d 2818 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
44 | 40, 43 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
45 | 44 | ad2ant2l 782 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
46 | 45 | 3impia 1261 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
47 | 38, 39, 46 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . . 22
|
48 | 47 | 3exp 1264 |
. . . . . . . . . . . . . . . . . . . . 21
|
49 | 37, 48 | syl5bir 233 |
. . . . . . . . . . . . . . . . . . . 20
|
50 | 49 | com3r 87 |
. . . . . . . . . . . . . . . . . . 19
|
51 | 50 | imp 445 |
. . . . . . . . . . . . . . . . . 18
|
52 | 51 | 3adant1 1079 |
. . . . . . . . . . . . . . . . 17
|
53 | 52 | reximdv 3016 |
. . . . . . . . . . . . . . . 16
|
54 | 53 | 3exp 1264 |
. . . . . . . . . . . . . . 15
|
55 | 54 | com34 91 |
. . . . . . . . . . . . . 14
|
56 | 55 | 3imp 1256 |
. . . . . . . . . . . . 13
|
57 | 34, 56 | syl5bir 233 |
. . . . . . . . . . . 12
|
58 | 57 | reximdv 3016 |
. . . . . . . . . . 11
|
59 | 58 | 3exp 1264 |
. . . . . . . . . 10
|
60 | 59 | com24 95 |
. . . . . . . . 9
|
61 | 60 | impd 447 |
. . . . . . . 8
|
62 | 29, 31, 61 | syl2and 500 |
. . . . . . 7
|
63 | 62 | rexlimdvv 3037 |
. . . . . 6
|
64 | 27, 63 | impbid 202 |
. . . . 5
|
65 | 64 | imbi2d 330 |
. . . 4
|
66 | 65 | 2ralbidv 2989 |
. . 3
|
67 | 2, 66 | syl 17 |
. 2
TopOn
|
68 | 1, 67 | bitrd 268 |
1
TopOn
|