Step | Hyp | Ref
| Expression |
1 | | simp1r 1086 |
. . . . 5
TopOn
|
2 | | simp2l 1087 |
. . . . 5
TopOn
|
3 | | simp2r 1088 |
. . . . . 6
TopOn
|
4 | | simp1l 1085 |
. . . . . . 7
TopOn
TopOn |
5 | | toponuni 20719 |
. . . . . . 7
TopOn
|
6 | 4, 5 | syl 17 |
. . . . . 6
TopOn
|
7 | 3, 6 | eleqtrd 2703 |
. . . . 5
TopOn
|
8 | | simp3 1063 |
. . . . 5
TopOn
|
9 | | eqid 2622 |
. . . . . 6
|
10 | 9 | regsep2 21180 |
. . . . 5
|
11 | 1, 2, 7, 8, 10 | syl13anc 1328 |
. . . 4
TopOn
|
12 | 11 | 3expia 1267 |
. . 3
TopOn
|
13 | 12 | ralrimivva 2971 |
. 2
TopOn
|
14 | | topontop 20718 |
. . . 4
TopOn
|
15 | 14 | adantr 481 |
. . 3
TopOn
|
16 | 5 | adantr 481 |
. . . . . . . . 9
TopOn |
17 | 16 | difeq1d 3727 |
. . . . . . . 8
TopOn |
18 | 9 | opncld 20837 |
. . . . . . . . 9
|
19 | 14, 18 | sylan 488 |
. . . . . . . 8
TopOn
|
20 | 17, 19 | eqeltrd 2701 |
. . . . . . 7
TopOn |
21 | | eleq2 2690 |
. . . . . . . . . . . 12
|
22 | 21 | notbid 308 |
. . . . . . . . . . 11
|
23 | | eldif 3584 |
. . . . . . . . . . . . 13
|
24 | 23 | baibr 945 |
. . . . . . . . . . . 12
|
25 | 24 | con1bid 345 |
. . . . . . . . . . 11
|
26 | 22, 25 | sylan9bb 736 |
. . . . . . . . . 10
|
27 | | simpl 473 |
. . . . . . . . . . . . 13
|
28 | 27 | sseq1d 3632 |
. . . . . . . . . . . 12
|
29 | 28 | 3anbi1d 1403 |
. . . . . . . . . . 11
|
30 | 29 | 2rexbidv 3057 |
. . . . . . . . . 10
|
31 | 26, 30 | imbi12d 334 |
. . . . . . . . 9
|
32 | 31 | ralbidva 2985 |
. . . . . . . 8
|
33 | 32 | rspcv 3305 |
. . . . . . 7
|
34 | 20, 33 | syl 17 |
. . . . . 6
TopOn
|
35 | | ralcom3 3105 |
. . . . . . 7
|
36 | | toponss 20731 |
. . . . . . . . . 10
TopOn |
37 | 36 | sselda 3603 |
. . . . . . . . 9
TopOn |
38 | | simprr2 1110 |
. . . . . . . . . . . . . 14
TopOn
|
39 | 5 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . 18
TopOn
|
40 | 39 | difeq1d 3727 |
. . . . . . . . . . . . . . . . 17
TopOn
|
41 | 14 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . 18
TopOn
|
42 | | simprll 802 |
. . . . . . . . . . . . . . . . . 18
TopOn
|
43 | 9 | opncld 20837 |
. . . . . . . . . . . . . . . . . 18
|
44 | 41, 42, 43 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
TopOn
|
45 | 40, 44 | eqeltrd 2701 |
. . . . . . . . . . . . . . . 16
TopOn
|
46 | | incom 3805 |
. . . . . . . . . . . . . . . . . 18
|
47 | | simprr3 1111 |
. . . . . . . . . . . . . . . . . 18
TopOn
|
48 | 46, 47 | syl5eq 2668 |
. . . . . . . . . . . . . . . . 17
TopOn
|
49 | | simplll 798 |
. . . . . . . . . . . . . . . . . . 19
TopOn
TopOn |
50 | | simprlr 803 |
. . . . . . . . . . . . . . . . . . 19
TopOn
|
51 | | toponss 20731 |
. . . . . . . . . . . . . . . . . . 19
TopOn |
52 | 49, 50, 51 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
TopOn
|
53 | | reldisj 4020 |
. . . . . . . . . . . . . . . . . 18
|
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . . 17
TopOn
|
55 | 48, 54 | mpbid 222 |
. . . . . . . . . . . . . . . 16
TopOn
|
56 | 9 | clsss2 20876 |
. . . . . . . . . . . . . . . 16
|
57 | 45, 55, 56 | syl2anc 693 |
. . . . . . . . . . . . . . 15
TopOn
|
58 | | simprr1 1109 |
. . . . . . . . . . . . . . . 16
TopOn
|
59 | | difcom 4053 |
. . . . . . . . . . . . . . . 16
|
60 | 58, 59 | sylib 208 |
. . . . . . . . . . . . . . 15
TopOn
|
61 | 57, 60 | sstrd 3613 |
. . . . . . . . . . . . . 14
TopOn
|
62 | 38, 61 | jca 554 |
. . . . . . . . . . . . 13
TopOn
|
63 | 62 | expr 643 |
. . . . . . . . . . . 12
TopOn
|
64 | 63 | anassrs 680 |
. . . . . . . . . . 11
TopOn
|
65 | 64 | reximdva 3017 |
. . . . . . . . . 10
TopOn
|
66 | 65 | rexlimdva 3031 |
. . . . . . . . 9
TopOn
|
67 | 37, 66 | embantd 59 |
. . . . . . . 8
TopOn
|
68 | 67 | ralimdva 2962 |
. . . . . . 7
TopOn
|
69 | 35, 68 | syl5bi 232 |
. . . . . 6
TopOn
|
70 | 34, 69 | syld 47 |
. . . . 5
TopOn
|
71 | 70 | ralrimdva 2969 |
. . . 4
TopOn
|
72 | 71 | imp 445 |
. . 3
TopOn
|
73 | | isreg 21136 |
. . 3
|
74 | 15, 72, 73 | sylanbrc 698 |
. 2
TopOn
|
75 | 13, 74 | impbida 877 |
1
TopOn
|