Step | Hyp | Ref
| Expression |
1 | | kqval.2 |
. . . . . . 7
 
   |
2 | 1 | kqffn 20795 |
. . . . . 6
 TopOn 
  |
3 | | elpreima 6030 |
. . . . . 6
                        |
4 | 2, 3 | syl 17 |
. . . . 5
 TopOn 
         

            |
5 | 4 | adantr 471 |
. . . 4
  TopOn                              |
6 | | noel 3747 |
. . . . . . . 8
     |
7 | | elin 3629 |
. . . . . . . . 9
                         
             |
8 | | incom 3637 |
. . . . . . . . . . 11
                         |
9 | | eqid 2462 |
. . . . . . . . . . . . . . . . . . . 20
   |
10 | 9 | cldss 20099 |
. . . . . . . . . . . . . . . . . . 19
    
   |
11 | 10 | adantl 472 |
. . . . . . . . . . . . . . . . . 18
  TopOn          |
12 | | fndm 5701 |
. . . . . . . . . . . . . . . . . . . . 21
   |
13 | 2, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
 TopOn 
  |
14 | | toponuni 19997 |
. . . . . . . . . . . . . . . . . . . 20
 TopOn 
   |
15 | 13, 14 | eqtrd 2496 |
. . . . . . . . . . . . . . . . . . 19
 TopOn 
   |
16 | 15 | adantr 471 |
. . . . . . . . . . . . . . . . . 18
  TopOn          |
17 | 11, 16 | sseqtr4d 3481 |
. . . . . . . . . . . . . . . . 17
  TopOn         |
18 | 13 | adantr 471 |
. . . . . . . . . . . . . . . . 17
  TopOn         |
19 | 17, 18 | sseqtrd 3480 |
. . . . . . . . . . . . . . . 16
  TopOn         |
20 | 19 | adantr 471 |
. . . . . . . . . . . . . . 15
   TopOn          |
21 | | dfss4 3689 |
. . . . . . . . . . . . . . 15

      |
22 | 20, 21 | sylib 201 |
. . . . . . . . . . . . . 14
   TopOn              |
23 | 22 | imaeq2d 5190 |
. . . . . . . . . . . . 13
   TopOn                      |
24 | 23 | ineq2d 3646 |
. . . . . . . . . . . 12
   TopOn                                      |
25 | | simpll 765 |
. . . . . . . . . . . . 13
   TopOn        TopOn    |
26 | 14 | adantr 471 |
. . . . . . . . . . . . . . . 16
  TopOn          |
27 | 26 | difeq1d 3562 |
. . . . . . . . . . . . . . 15
  TopOn              |
28 | 9 | cldopn 20101 |
. . . . . . . . . . . . . . . 16
    
     |
29 | 28 | adantl 472 |
. . . . . . . . . . . . . . 15
  TopOn        
   |
30 | 27, 29 | eqeltrd 2540 |
. . . . . . . . . . . . . 14
  TopOn           |
31 | 30 | adantr 471 |
. . . . . . . . . . . . 13
   TopOn            |
32 | 1 | kqdisj 20802 |
. . . . . . . . . . . . 13
  TopOn                       |
33 | 25, 31, 32 | syl2anc 671 |
. . . . . . . . . . . 12
   TopOn                          |
34 | 24, 33 | eqtr3d 2498 |
. . . . . . . . . . 11
   TopOn                      |
35 | 8, 34 | syl5eq 2508 |
. . . . . . . . . 10
   TopOn            
         |
36 | 35 | eleq2d 2525 |
. . . . . . . . 9
   TopOn                        
       |
37 | 7, 36 | syl5bbr 267 |
. . . . . . . 8
   TopOn                                    |
38 | 6, 37 | mtbiri 309 |
. . . . . . 7
   TopOn                              |
39 | | imnan 428 |
. . . . . . 7
                                           |
40 | 38, 39 | sylibr 217 |
. . . . . 6
   TopOn                              |
41 | | eldif 3426 |
. . . . . . . . . 10
  

   |
42 | 41 | baibr 920 |
. . . . . . . . 9
 
     |
43 | 42 | adantl 472 |
. . . . . . . 8
   TopOn        
     |
44 | | simpr 467 |
. . . . . . . . 9
   TopOn          |
45 | 1 | kqfvima 20800 |
. . . . . . . . 9
  TopOn       
             |
46 | 25, 31, 44, 45 | syl3anc 1276 |
. . . . . . . 8
   TopOn          
             |
47 | 43, 46 | bitrd 261 |
. . . . . . 7
   TopOn        
             |
48 | 47 | con1bid 336 |
. . . . . 6
   TopOn                  
   |
49 | 40, 48 | sylibd 222 |
. . . . 5
   TopOn                    |
50 | 49 | expimpd 612 |
. . . 4
  TopOn                     |
51 | 5, 50 | sylbid 223 |
. . 3
  TopOn                    |
52 | 51 | ssrdv 3450 |
. 2
  TopOn                  |
53 | | dfss1 3649 |
. . . 4

    |
54 | 17, 53 | sylib 201 |
. . 3
  TopOn           |
55 | | dminss 5272 |
. . 3

           |
56 | 54, 55 | syl6eqssr 3495 |
. 2
  TopOn                  |
57 | 52, 56 | eqssd 3461 |
1
  TopOn                  |