Step | Hyp | Ref
| Expression |
1 | | kqval.2 |
. . . . . . 7
|
2 | 1 | kqffn 21528 |
. . . . . 6
TopOn
|
3 | | elpreima 6337 |
. . . . . 6
|
4 | 2, 3 | syl 17 |
. . . . 5
TopOn
|
5 | 4 | adantr 481 |
. . . 4
TopOn |
6 | | noel 3919 |
. . . . . . . 8
|
7 | | elin 3796 |
. . . . . . . . 9
|
8 | | incom 3805 |
. . . . . . . . . . 11
|
9 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
|
10 | 9 | cldss 20833 |
. . . . . . . . . . . . . . . . . . 19
|
11 | 10 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
TopOn |
12 | | fndm 5990 |
. . . . . . . . . . . . . . . . . . . . 21
|
13 | 2, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
TopOn
|
14 | | toponuni 20719 |
. . . . . . . . . . . . . . . . . . . 20
TopOn
|
15 | 13, 14 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
TopOn
|
16 | 15 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
TopOn |
17 | 11, 16 | sseqtr4d 3642 |
. . . . . . . . . . . . . . . . 17
TopOn |
18 | 13 | adantr 481 |
. . . . . . . . . . . . . . . . 17
TopOn |
19 | 17, 18 | sseqtrd 3641 |
. . . . . . . . . . . . . . . 16
TopOn |
20 | 19 | adantr 481 |
. . . . . . . . . . . . . . 15
TopOn |
21 | | dfss4 3858 |
. . . . . . . . . . . . . . 15
|
22 | 20, 21 | sylib 208 |
. . . . . . . . . . . . . 14
TopOn |
23 | 22 | imaeq2d 5466 |
. . . . . . . . . . . . 13
TopOn |
24 | 23 | ineq2d 3814 |
. . . . . . . . . . . 12
TopOn |
25 | | simpll 790 |
. . . . . . . . . . . . 13
TopOn TopOn |
26 | 14 | adantr 481 |
. . . . . . . . . . . . . . . 16
TopOn |
27 | 26 | difeq1d 3727 |
. . . . . . . . . . . . . . 15
TopOn |
28 | 9 | cldopn 20835 |
. . . . . . . . . . . . . . . 16
|
29 | 28 | adantl 482 |
. . . . . . . . . . . . . . 15
TopOn
|
30 | 27, 29 | eqeltrd 2701 |
. . . . . . . . . . . . . 14
TopOn |
31 | 30 | adantr 481 |
. . . . . . . . . . . . 13
TopOn |
32 | 1 | kqdisj 21535 |
. . . . . . . . . . . . 13
TopOn |
33 | 25, 31, 32 | syl2anc 693 |
. . . . . . . . . . . 12
TopOn |
34 | 24, 33 | eqtr3d 2658 |
. . . . . . . . . . 11
TopOn |
35 | 8, 34 | syl5eq 2668 |
. . . . . . . . . 10
TopOn
|
36 | 35 | eleq2d 2687 |
. . . . . . . . 9
TopOn
|
37 | 7, 36 | syl5bbr 274 |
. . . . . . . 8
TopOn |
38 | 6, 37 | mtbiri 317 |
. . . . . . 7
TopOn |
39 | | imnan 438 |
. . . . . . 7
|
40 | 38, 39 | sylibr 224 |
. . . . . 6
TopOn |
41 | | eldif 3584 |
. . . . . . . . . 10
|
42 | 41 | baibr 945 |
. . . . . . . . 9
|
43 | 42 | adantl 482 |
. . . . . . . 8
TopOn
|
44 | | simpr 477 |
. . . . . . . . 9
TopOn |
45 | 1 | kqfvima 21533 |
. . . . . . . . 9
TopOn
|
46 | 25, 31, 44, 45 | syl3anc 1326 |
. . . . . . . 8
TopOn
|
47 | 43, 46 | bitrd 268 |
. . . . . . 7
TopOn
|
48 | 47 | con1bid 345 |
. . . . . 6
TopOn
|
49 | 40, 48 | sylibd 229 |
. . . . 5
TopOn |
50 | 49 | expimpd 629 |
. . . 4
TopOn |
51 | 5, 50 | sylbid 230 |
. . 3
TopOn |
52 | 51 | ssrdv 3609 |
. 2
TopOn |
53 | | sseqin2 3817 |
. . . 4
|
54 | 17, 53 | sylib 208 |
. . 3
TopOn |
55 | | dminss 5547 |
. . 3
|
56 | 54, 55 | syl6eqssr 3656 |
. 2
TopOn |
57 | 52, 56 | eqssd 3620 |
1
TopOn |