Step | Hyp | Ref
| Expression |
1 | | fconstmpt 4897 |
. . . . 5
        
  |
2 | | pt1hmeo.a |
. . . . . . 7
   |
3 | 2 | adantr 471 |
. . . . . 6
 
   |
4 | | sneq 3990 |
. . . . . . . . 9
       |
5 | 4 | xpeq1d 4876 |
. . . . . . . 8
               |
6 | | opeq1 4180 |
. . . . . . . . 9
   
     |
7 | 6 | sneqd 3992 |
. . . . . . . 8
             |
8 | 5, 7 | eqeq12d 2477 |
. . . . . . 7
            
  
           |
9 | | vex 3060 |
. . . . . . . 8
 |
10 | | vex 3060 |
. . . . . . . 8
 |
11 | 9, 10 | xpsn 6090 |
. . . . . . 7
            |
12 | 8, 11 | vtoclg 3119 |
. . . . . 6
              |
13 | 3, 12 | syl 17 |
. . . . 5
 
              |
14 | 1, 13 | syl5eqr 2510 |
. . . 4
 
            |
15 | 14 | mpteq2dva 4503 |
. . 3
    
           |
16 | | pt1hmeo.j |
. . . 4
          |
17 | | pt1hmeo.r |
. . . 4
 TopOn    |
18 | | snex 4655 |
. . . . 5
 
 |
19 | 18 | a1i 11 |
. . . 4
     |
20 | | f1osng 5876 |
. . . . . . 7
 
TopOn                  |
21 | 2, 17, 20 | syl2anc 671 |
. . . . . 6
                |
22 | | f1of 5837 |
. . . . . 6
             
               |
23 | 21, 22 | syl 17 |
. . . . 5
                |
24 | | topontop 19990 |
. . . . . . 7
 TopOn 
  |
25 | 17, 24 | syl 17 |
. . . . . 6
   |
26 | 25 | snssd 4130 |
. . . . 5
     |
27 | 23, 26 | fssd 5761 |
. . . 4
              |
28 | 17 | cnmptid 20725 |
. . . . . 6
       |
29 | 28 | adantr 471 |
. . . . 5
 
         |
30 | | elsni 4005 |
. . . . . . . 8
     |
31 | 30 | fveq2d 5892 |
. . . . . . 7
                       |
32 | | fvsng 6122 |
. . . . . . . 8
 
TopOn              |
33 | 2, 17, 32 | syl2anc 671 |
. . . . . . 7
            |
34 | 31, 33 | sylan9eqr 2518 |
. . . . . 6
 
              |
35 | 34 | oveq2d 6331 |
. . . . 5
 
                  |
36 | 29, 35 | eleqtrrd 2543 |
. . . 4
 
                  |
37 | 16, 17, 19, 27, 36 | ptcn 20691 |
. . 3
    
      |
38 | 15, 37 | eqeltrrd 2541 |
. 2
            |
39 | | simprr 771 |
. . . . . . . . 9
 

              |
40 | 14 | adantrr 728 |
. . . . . . . . 9
 

         
        |
41 | 39, 40 | eqtr4d 2499 |
. . . . . . . 8
 

             |
42 | | simprl 769 |
. . . . . . . . . . 11
 

      
  |
43 | 42 | adantr 471 |
. . . . . . . . . 10
   
            |
44 | | eqid 2462 |
. . . . . . . . . 10
         |
45 | 43, 44 | fmptd 6069 |
. . . . . . . . 9
 

         
         |
46 | | toponmax 19992 |
. . . . . . . . . . . 12
 TopOn 
  |
47 | 17, 46 | syl 17 |
. . . . . . . . . . 11
   |
48 | 47 | adantr 471 |
. . . . . . . . . 10
 

      
  |
49 | | elmapg 7511 |
. . . . . . . . . 10
             
             |
50 | 48, 18, 49 | sylancl 673 |
. . . . . . . . 9
 

                             |
51 | 45, 50 | mpbird 240 |
. . . . . . . 8
 

         
       |
52 | 41, 51 | eqeltrd 2540 |
. . . . . . 7
 

             |
53 | 39 | fveq1d 5890 |
. . . . . . . 8
 

                      |
54 | 2 | adantr 471 |
. . . . . . . . 9
 

      
  |
55 | | fvsng 6122 |
. . . . . . . . 9
 
            |
56 | 54, 42, 55 | syl2anc 671 |
. . . . . . . 8
 

                  |
57 | 53, 56 | eqtr2d 2497 |
. . . . . . 7
 

      
      |
58 | 52, 57 | jca 539 |
. . . . . 6
 

                   |
59 | | simprr 771 |
. . . . . . . 8
 
                 |
60 | | simprl 769 |
. . . . . . . . . 10
 
                 |
61 | 47 | adantr 471 |
. . . . . . . . . . 11
 
             |
62 | | elmapg 7511 |
. . . . . . . . . . 11
         
         |
63 | 61, 18, 62 | sylancl 673 |
. . . . . . . . . 10
 
               
         |
64 | 60, 63 | mpbid 215 |
. . . . . . . . 9
 
                   |
65 | | snidg 4006 |
. . . . . . . . . . 11
     |
66 | 2, 65 | syl 17 |
. . . . . . . . . 10
     |
67 | 66 | adantr 471 |
. . . . . . . . 9
 
               |
68 | 64, 67 | ffvelrnd 6046 |
. . . . . . . 8
 
                 |
69 | 59, 68 | eqeltrd 2540 |
. . . . . . 7
 
             |
70 | 2 | adantr 471 |
. . . . . . . . . . 11
 
             |
71 | 4 | feq2d 5737 |
. . . . . . . . . . . 12
       
         |
72 | | fveq2 5888 |
. . . . . . . . . . . . . 14
           |
73 | 72 | eleq1d 2524 |
. . . . . . . . . . . . 13
     
       |
74 | | id 22 |
. . . . . . . . . . . . . . . 16
   |
75 | 74, 72 | opeq12d 4188 |
. . . . . . . . . . . . . . 15
                 |
76 | 75 | sneqd 3992 |
. . . . . . . . . . . . . 14
                     |
77 | 76 | eqeq2d 2472 |
. . . . . . . . . . . . 13
          
            |
78 | 73, 77 | anbi12d 722 |
. . . . . . . . . . . 12
      
         
    
             |
79 | 9 | fsn2 6086 |
. . . . . . . . . . . 12
                        |
80 | 71, 78, 79 | vtoclbg 3120 |
. . . . . . . . . . 11
                          |
81 | 70, 80 | syl 17 |
. . . . . . . . . 10
 
                 
    
             |
82 | 64, 81 | mpbid 215 |
. . . . . . . . 9
 
                            |
83 | 82 | simprd 469 |
. . . . . . . 8
 
                      |
84 | 59 | opeq2d 4187 |
. . . . . . . . 9
 
                       |
85 | 84 | sneqd 3992 |
. . . . . . . 8
 
                           |
86 | 83, 85 | eqtr4d 2499 |
. . . . . . 7
 
                  |
87 | 69, 86 | jca 539 |
. . . . . 6
 
                    |
88 | 58, 87 | impbida 848 |
. . . . 5
        
             |
89 | 88 | mptcnv 5257 |
. . . 4
                     |
90 | | xpsng 6089 |
. . . . . . . . . . 11
 
TopOn                |
91 | 2, 17, 90 | syl2anc 671 |
. . . . . . . . . 10
              |
92 | 91 | eqcomd 2468 |
. . . . . . . . 9
              |
93 | 92 | fveq2d 5892 |
. . . . . . . 8
                      |
94 | 16, 93 | syl5eq 2508 |
. . . . . . 7
             |
95 | | eqid 2462 |
. . . . . . . . 9
                     |
96 | 95 | pttoponconst 20661 |
. . . . . . . 8
    TopOn             TopOn        |
97 | 19, 17, 96 | syl2anc 671 |
. . . . . . 7
           TopOn        |
98 | 94, 97 | eqeltrd 2540 |
. . . . . 6
 TopOn 
      |
99 | | toponuni 19991 |
. . . . . 6
 TopOn             |
100 | 98, 99 | syl 17 |
. . . . 5
        |
101 | 100 | mpteq1d 4498 |
. . . 4
                    |
102 | 89, 101 | eqtrd 2496 |
. . 3
                  |
103 | | eqid 2462 |
. . . . . 6
   |
104 | 103, 16 | ptpjcn 20675 |
. . . . 5
              
                       |
105 | 19, 27, 66, 104 | syl3anc 1276 |
. . . 4
                     |
106 | 33 | oveq2d 6331 |
. . . 4
                |
107 | 105, 106 | eleqtrd 2542 |
. . 3
            |
108 | 102, 107 | eqeltrd 2540 |
. 2
             |
109 | | ishmeo 20823 |
. 2
           
                       |
110 | 38, 108, 109 | sylanbrc 675 |
1
              |