Step | Hyp | Ref
| Expression |
1 | | cvmliftpht.b |
. . . 4
  |
2 | | cvmliftpht.m |
. . . 4
               |
3 | | cvmliftpht.f |
. . . 4
  CovMap    |
4 | | cvmliftphtlem.g |
. . . 4
     |
5 | | cvmliftpht.p |
. . . 4
   |
6 | | cvmliftpht.e |
. . . 4
           |
7 | 1, 2, 3, 4, 5, 6 | cvmliftiota 30017 |
. . 3
             |
8 | 7 | simp1d 1019 |
. 2
     |
9 | | cvmliftpht.n |
. . . 4
               |
10 | | cvmliftphtlem.h |
. . . 4
     |
11 | | cvmliftphtlem.k |
. . . . . . 7
           |
12 | 4, 10, 11 | phtpy01 22009 |
. . . . . 6
                     |
13 | 12 | simpld 461 |
. . . . 5
           |
14 | 6, 13 | eqtrd 2484 |
. . . 4
           |
15 | 1, 9, 3, 10, 5, 14 | cvmliftiota 30017 |
. . 3
             |
16 | 15 | simp1d 1019 |
. 2
     |
17 | | cvmliftphtlem.a |
. 2
  
    |
18 | | iitop 21905 |
. . . . . . . . . . . . . . . 16
 |
19 | | iiuni 21906 |
. . . . . . . . . . . . . . . 16
  ![[,] [,]](_icc.gif)    |
20 | 18, 18, 19, 19 | txunii 20601 |
. . . . . . . . . . . . . . 15
   ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)       |
21 | 20, 1 | cnf 20255 |
. . . . . . . . . . . . . 14
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)       |
22 | 17, 21 | syl 17 |
. . . . . . . . . . . . 13
      ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)       |
23 | | 0elunit 11747 |
. . . . . . . . . . . . . 14
  ![[,] [,]](_icc.gif)   |
24 | | opelxpi 4865 |
. . . . . . . . . . . . . 14
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     |
25 | 23, 24 | mpan2 676 |
. . . . . . . . . . . . 13
   ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     |
26 | | fvco3 5940 |
. . . . . . . . . . . . 13
       ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)                          |
27 | 22, 25, 26 | syl2an 480 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)                         |
28 | | cvmliftphtlem.c |
. . . . . . . . . . . . . 14
     |
29 | 28 | adantr 467 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)   
   |
30 | 29 | fveq1d 5865 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)                     |
31 | 27, 30 | eqtr3d 2486 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)                       |
32 | | df-ov 6291 |
. . . . . . . . . . . 12
            |
33 | 32 | fveq2i 5866 |
. . . . . . . . . . 11
                    |
34 | | df-ov 6291 |
. . . . . . . . . . 11
            |
35 | 31, 33, 34 | 3eqtr4g 2509 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)                 |
36 | | iitopon 21904 |
. . . . . . . . . . . . 13
TopOn   ![[,] [,]](_icc.gif)    |
37 | 36 | a1i 11 |
. . . . . . . . . . . 12
 TopOn   ![[,] [,]](_icc.gif)     |
38 | 4, 10 | phtpyhtpy 22006 |
. . . . . . . . . . . . 13
            Htpy      |
39 | 38, 11 | sseldd 3432 |
. . . . . . . . . . . 12
    Htpy      |
40 | 37, 4, 10, 39 | htpyi 21998 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)                       |
41 | 40 | simpld 461 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)             |
42 | 35, 41 | eqtrd 2484 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)                 |
43 | 42 | mpteq2dva 4488 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)         |
44 | | fovrn 6436 |
. . . . . . . . . . 11
       ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
      |
45 | 23, 44 | mp3an3 1352 |
. . . . . . . . . 10
       ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)  
      |
46 | 22, 45 | sylan 474 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)         |
47 | | eqidd 2451 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)         |
48 | | cvmcn 29978 |
. . . . . . . . . . . 12
  CovMap 

   |
49 | 3, 48 | syl 17 |
. . . . . . . . . . 11
     |
50 | | eqid 2450 |
. . . . . . . . . . . 12
   |
51 | 1, 50 | cnf 20255 |
. . . . . . . . . . 11
          |
52 | 49, 51 | syl 17 |
. . . . . . . . . 10
        |
53 | 52 | feqmptd 5916 |
. . . . . . . . 9
         |
54 | | fveq2 5863 |
. . . . . . . . 9
                   |
55 | 46, 47, 53, 54 | fmptco 6054 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)             |
56 | 19, 50 | cnf 20255 |
. . . . . . . . . 10
       ![[,] [,]](_icc.gif)       |
57 | 4, 56 | syl 17 |
. . . . . . . . 9
     ![[,] [,]](_icc.gif)       |
58 | 57 | feqmptd 5916 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)         |
59 | 43, 55, 58 | 3eqtr4d 2494 |
. . . . . . 7
     ![[,] [,]](_icc.gif)          |
60 | | cvmliftphtlem.0 |
. . . . . . 7
       |
61 | 37 | cnmptid 20669 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)       |
62 | 23 | a1i 11 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)    |
63 | 37, 37, 62 | cnmptc 20670 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)       |
64 | 37, 61, 63, 17 | cnmpt12f 20674 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)           |
65 | 1 | cvmlift 30015 |
. . . . . . . . 9
    CovMap 
   
         
              |
66 | 3, 4, 5, 6, 65 | syl22anc 1268 |
. . . . . . . 8
               |
67 | | coeq2 4992 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)          |
68 | 67 | eqeq1d 2452 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)           |
69 | | fveq1 5862 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)            |
70 | | oveq1 6295 |
. . . . . . . . . . . . . 14
           |
71 | | eqid 2450 |
. . . . . . . . . . . . . 14
   ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)        |
72 | | ovex 6316 |
. . . . . . . . . . . . . 14
     |
73 | 70, 71, 72 | fvmpt 5946 |
. . . . . . . . . . . . 13
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                |
74 | 23, 73 | ax-mp 5 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)               |
75 | 69, 74 | syl6eq 2500 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)                 |
76 | 75 | eqeq1d 2452 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)                   |
77 | 68, 76 | anbi12d 716 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)               
 
   ![[,] [,]](_icc.gif)                |
78 | 77 | riota2 6272 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)                            ![[,] [,]](_icc.gif)            
                 ![[,] [,]](_icc.gif)          |
79 | 64, 66, 78 | syl2anc 666 |
. . . . . . 7
       ![[,] [,]](_icc.gif)            
                 ![[,] [,]](_icc.gif)          |
80 | 59, 60, 79 | mpbi2and 931 |
. . . . . 6
                  ![[,] [,]](_icc.gif)         |
81 | 2, 80 | syl5eq 2496 |
. . . . 5
    ![[,] [,]](_icc.gif)         |
82 | 19, 1 | cnf 20255 |
. . . . . . 7
       ![[,] [,]](_icc.gif)      |
83 | 8, 82 | syl 17 |
. . . . . 6
     ![[,] [,]](_icc.gif)      |
84 | 83 | feqmptd 5916 |
. . . . 5
    ![[,] [,]](_icc.gif)         |
85 | 81, 84 | eqtr3d 2486 |
. . . 4
    ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)         |
86 | | mpteqb 5962 |
. . . . 5
 
  ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)              |
87 | | ovex 6316 |
. . . . . 6
     |
88 | 87 | a1i 11 |
. . . . 5
   ![[,] [,]](_icc.gif)        |
89 | 86, 88 | mprg 2750 |
. . . 4
    ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       
  ![[,] [,]](_icc.gif)             |
90 | 85, 89 | sylib 200 |
. . 3
    ![[,] [,]](_icc.gif)             |
91 | 90 | r19.21bi 2756 |
. 2
 
  ![[,] [,]](_icc.gif)             |
92 | | 1elunit 11748 |
. . . . . . . . . . . . . 14
  ![[,] [,]](_icc.gif)   |
93 | | opelxpi 4865 |
. . . . . . . . . . . . . 14
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     |
94 | 92, 93 | mpan2 676 |
. . . . . . . . . . . . 13
   ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     |
95 | | fvco3 5940 |
. . . . . . . . . . . . 13
       ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)                          |
96 | 22, 94, 95 | syl2an 480 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)                         |
97 | 29 | fveq1d 5865 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)                     |
98 | 96, 97 | eqtr3d 2486 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)                       |
99 | | df-ov 6291 |
. . . . . . . . . . . 12
            |
100 | 99 | fveq2i 5866 |
. . . . . . . . . . 11
                    |
101 | | df-ov 6291 |
. . . . . . . . . . 11
            |
102 | 98, 100, 101 | 3eqtr4g 2509 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)                 |
103 | 40 | simprd 465 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)             |
104 | 102, 103 | eqtrd 2484 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)                 |
105 | 104 | mpteq2dva 4488 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)         |
106 | | fovrn 6436 |
. . . . . . . . . . 11
       ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
      |
107 | 92, 106 | mp3an3 1352 |
. . . . . . . . . 10
       ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)  
      |
108 | 22, 107 | sylan 474 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)         |
109 | | eqidd 2451 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)         |
110 | | fveq2 5863 |
. . . . . . . . 9
                   |
111 | 108, 109,
53, 110 | fmptco 6054 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)             |
112 | 19, 50 | cnf 20255 |
. . . . . . . . . 10
       ![[,] [,]](_icc.gif)       |
113 | 10, 112 | syl 17 |
. . . . . . . . 9
     ![[,] [,]](_icc.gif)       |
114 | 113 | feqmptd 5916 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)         |
115 | 105, 111,
114 | 3eqtr4d 2494 |
. . . . . . 7
     ![[,] [,]](_icc.gif)          |
116 | | iicon 21912 |
. . . . . . . . . . . . 13
 |
117 | 116 | a1i 11 |
. . . . . . . . . . . 12
   |
118 | | iinllycon 29970 |
. . . . . . . . . . . . 13
𝑛Locally  |
119 | 118 | a1i 11 |
. . . . . . . . . . . 12

𝑛Locally   |
120 | 37, 63, 61, 17 | cnmpt12f 20674 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)           |
121 | | cvmtop1 29976 |
. . . . . . . . . . . . . . 15
  CovMap 
  |
122 | 3, 121 | syl 17 |
. . . . . . . . . . . . . 14
   |
123 | 1 | toptopon 19941 |
. . . . . . . . . . . . . 14

TopOn    |
124 | 122, 123 | sylib 200 |
. . . . . . . . . . . . 13
 TopOn    |
125 | | ffvelrn 6018 |
. . . . . . . . . . . . . 14
      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)  
      |
126 | 83, 23, 125 | sylancl 667 |
. . . . . . . . . . . . 13
       |
127 | | cnconst2 20292 |
. . . . . . . . . . . . 13
  TopOn   ![[,] [,]](_icc.gif)   TopOn          ![[,] [,]](_icc.gif)             |
128 | 37, 124, 126, 127 | syl3anc 1267 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)             |
129 | 4, 10, 11 | phtpyi 22008 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)                       |
130 | 129 | simpld 461 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)             |
131 | | opelxpi 4865 |
. . . . . . . . . . . . . . . . . . . 20
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     |
132 | 23, 131 | mpan 675 |
. . . . . . . . . . . . . . . . . . 19
   ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     |
133 | | fvco3 5940 |
. . . . . . . . . . . . . . . . . . 19
       ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)          
               |
134 | 22, 132, 133 | syl2an 480 |
. . . . . . . . . . . . . . . . . 18
 
  ![[,] [,]](_icc.gif)                         |
135 | 29 | fveq1d 5865 |
. . . . . . . . . . . . . . . . . 18
 
  ![[,] [,]](_icc.gif)                     |
136 | 134, 135 | eqtr3d 2486 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)                       |
137 | | df-ov 6291 |
. . . . . . . . . . . . . . . . . 18
        
   |
138 | 137 | fveq2i 5866 |
. . . . . . . . . . . . . . . . 17
                    |
139 | | df-ov 6291 |
. . . . . . . . . . . . . . . . 17
        
   |
140 | 136, 138,
139 | 3eqtr4g 2509 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)                 |
141 | 7 | simp3d 1021 |
. . . . . . . . . . . . . . . . . . 19
       |
142 | 141 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
  ![[,] [,]](_icc.gif)         |
143 | 142 | fveq2d 5867 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)                 |
144 | 6 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)             |
145 | 143, 144 | eqtrd 2484 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)                 |
146 | 130, 140,
145 | 3eqtr4d 2494 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)                     |
147 | 146 | mpteq2dva 4488 |
. . . . . . . . . . . . . 14
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)             |
148 | | fconstmpt 4877 |
. . . . . . . . . . . . . 14
   ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)            |
149 | 147, 148 | syl6eqr 2502 |
. . . . . . . . . . . . 13
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)               |
150 | | fovrn 6436 |
. . . . . . . . . . . . . . . 16
       ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
      |
151 | 23, 150 | mp3an2 1351 |
. . . . . . . . . . . . . . 15
       ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)  
      |
152 | 22, 151 | sylan 474 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)         |
153 | | eqidd 2451 |
. . . . . . . . . . . . . 14
    ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)         |
154 | | fveq2 5863 |
. . . . . . . . . . . . . 14
                   |
155 | 152, 153,
53, 154 | fmptco 6054 |
. . . . . . . . . . . . 13
     ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)             |
156 | | ffn 5726 |
. . . . . . . . . . . . . . 15
        |
157 | 52, 156 | syl 17 |
. . . . . . . . . . . . . 14
   |
158 | | fcoconst 6058 |
. . . . . . . . . . . . . 14
           ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)               |
159 | 157, 126,
158 | syl2anc 666 |
. . . . . . . . . . . . 13
     ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)               |
160 | 149, 155,
159 | 3eqtr4d 2494 |
. . . . . . . . . . . 12
     ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)            |
161 | 60, 141 | eqtr4d 2487 |
. . . . . . . . . . . . 13
           |
162 | | oveq2 6296 |
. . . . . . . . . . . . . . 15
           |
163 | | eqid 2450 |
. . . . . . . . . . . . . . 15
   ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)        |
164 | 162, 163,
72 | fvmpt 5946 |
. . . . . . . . . . . . . 14
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                |
165 | 23, 164 | ax-mp 5 |
. . . . . . . . . . . . 13
    ![[,] [,]](_icc.gif)               |
166 | | fvex 5873 |
. . . . . . . . . . . . . . 15
     |
167 | 166 | fvconst2 6118 |
. . . . . . . . . . . . . 14
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                  |
168 | 23, 167 | ax-mp 5 |
. . . . . . . . . . . . 13
    ![[,] [,]](_icc.gif)                 |
169 | 161, 165,
168 | 3eqtr4g 2509 |
. . . . . . . . . . . 12
     ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)              |
170 | 1, 19, 3, 117, 119, 62, 120, 128, 160, 169 | cvmliftmoi 29999 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)           |
171 | | fconstmpt 4877 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)        |
172 | 170, 171 | syl6eq 2500 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)         |
173 | | mpteqb 5962 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)              |
174 | | ovex 6316 |
. . . . . . . . . . . 12
     |
175 | 174 | a1i 11 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)        |
176 | 173, 175 | mprg 2750 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       
  ![[,] [,]](_icc.gif)             |
177 | 172, 176 | sylib 200 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)             |
178 | | oveq2 6296 |
. . . . . . . . . . 11
           |
179 | 178 | eqeq1d 2452 |
. . . . . . . . . 10
         
           |
180 | 179 | rspcv 3145 |
. . . . . . . . 9
   ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)                      |
181 | 92, 177, 180 | mpsyl 65 |
. . . . . . . 8
           |
182 | 181, 141 | eqtrd 2484 |
. . . . . . 7
       |
183 | 92 | a1i 11 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)    |
184 | 37, 37, 183 | cnmptc 20670 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)       |
185 | 37, 61, 184, 17 | cnmpt12f 20674 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)           |
186 | 1 | cvmlift 30015 |
. . . . . . . . 9
    CovMap 
   
         
              |
187 | 3, 10, 5, 14, 186 | syl22anc 1268 |
. . . . . . . 8
               |
188 | | coeq2 4992 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)          |
189 | 188 | eqeq1d 2452 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)           |
190 | | fveq1 5862 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)            |
191 | | oveq1 6295 |
. . . . . . . . . . . . . 14
           |
192 | | eqid 2450 |
. . . . . . . . . . . . . 14
   ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)        |
193 | | ovex 6316 |
. . . . . . . . . . . . . 14
     |
194 | 191, 192,
193 | fvmpt 5946 |
. . . . . . . . . . . . 13
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                |
195 | 23, 194 | ax-mp 5 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)               |
196 | 190, 195 | syl6eq 2500 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)                 |
197 | 196 | eqeq1d 2452 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)                   |
198 | 189, 197 | anbi12d 716 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)               
 
   ![[,] [,]](_icc.gif)                |
199 | 198 | riota2 6272 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)                            ![[,] [,]](_icc.gif)            
                 ![[,] [,]](_icc.gif)          |
200 | 185, 187,
199 | syl2anc 666 |
. . . . . . 7
       ![[,] [,]](_icc.gif)            
                 ![[,] [,]](_icc.gif)          |
201 | 115, 182,
200 | mpbi2and 931 |
. . . . . 6
                  ![[,] [,]](_icc.gif)         |
202 | 9, 201 | syl5eq 2496 |
. . . . 5
    ![[,] [,]](_icc.gif)         |
203 | 19, 1 | cnf 20255 |
. . . . . . 7
       ![[,] [,]](_icc.gif)      |
204 | 16, 203 | syl 17 |
. . . . . 6
     ![[,] [,]](_icc.gif)      |
205 | 204 | feqmptd 5916 |
. . . . 5
    ![[,] [,]](_icc.gif)         |
206 | 202, 205 | eqtr3d 2486 |
. . . 4
    ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)         |
207 | | mpteqb 5962 |
. . . . 5
 
  ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)              |
208 | | ovex 6316 |
. . . . . 6
     |
209 | 208 | a1i 11 |
. . . . 5
   ![[,] [,]](_icc.gif)        |
210 | 207, 209 | mprg 2750 |
. . . 4
    ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       
  ![[,] [,]](_icc.gif)             |
211 | 206, 210 | sylib 200 |
. . 3
    ![[,] [,]](_icc.gif)             |
212 | 211 | r19.21bi 2756 |
. 2
 
  ![[,] [,]](_icc.gif)             |
213 | 177 | r19.21bi 2756 |
. 2
 
  ![[,] [,]](_icc.gif)             |
214 | 37, 184, 61, 17 | cnmpt12f 20674 |
. . . . . 6
    ![[,] [,]](_icc.gif)           |
215 | | ffvelrn 6018 |
. . . . . . . 8
      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)  
      |
216 | 83, 92, 215 | sylancl 667 |
. . . . . . 7
       |
217 | | cnconst2 20292 |
. . . . . . 7
  TopOn   ![[,] [,]](_icc.gif)   TopOn          ![[,] [,]](_icc.gif)             |
218 | 37, 124, 216, 217 | syl3anc 1267 |
. . . . . 6
    ![[,] [,]](_icc.gif)             |
219 | | opelxpi 4865 |
. . . . . . . . . . . . . 14
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     |
220 | 92, 219 | mpan 675 |
. . . . . . . . . . . . 13
   ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     |
221 | | fvco3 5940 |
. . . . . . . . . . . . 13
       ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)          
               |
222 | 22, 220, 221 | syl2an 480 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)                         |
223 | 29 | fveq1d 5865 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)                     |
224 | 222, 223 | eqtr3d 2486 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)                       |
225 | | df-ov 6291 |
. . . . . . . . . . . 12
        
   |
226 | 225 | fveq2i 5866 |
. . . . . . . . . . 11
                    |
227 | | df-ov 6291 |
. . . . . . . . . . 11
        
   |
228 | 224, 226,
227 | 3eqtr4g 2509 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)                 |
229 | 129 | simprd 465 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)             |
230 | 7 | simp2d 1020 |
. . . . . . . . . . . . 13
     |
231 | 230 | adantr 467 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)   
   |
232 | 231 | fveq1d 5865 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)               |
233 | 83 | adantr 467 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)      |
234 | | fvco3 5940 |
. . . . . . . . . . . 12
      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)  
 
              |
235 | 233, 92, 234 | sylancl 667 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)                   |
236 | 232, 235 | eqtr3d 2486 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)                 |
237 | 228, 229,
236 | 3eqtrd 2488 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)                     |
238 | 237 | mpteq2dva 4488 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)             |
239 | | fconstmpt 4877 |
. . . . . . . 8
   ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)            |
240 | 238, 239 | syl6eqr 2502 |
. . . . . . 7
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)               |
241 | | fovrn 6436 |
. . . . . . . . . 10
       ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
      |
242 | 92, 241 | mp3an2 1351 |
. . . . . . . . 9
       ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)  
      |
243 | 22, 242 | sylan 474 |
. . . . . . . 8
 
  ![[,] [,]](_icc.gif)         |
244 | | eqidd 2451 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)         |
245 | | fveq2 5863 |
. . . . . . . 8
                   |
246 | 243, 244,
53, 245 | fmptco 6054 |
. . . . . . 7
     ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)             |
247 | | fcoconst 6058 |
. . . . . . . 8
           ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)               |
248 | 157, 216,
247 | syl2anc 666 |
. . . . . . 7
     ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)               |
249 | 240, 246,
248 | 3eqtr4d 2494 |
. . . . . 6
     ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)            |
250 | | oveq1 6295 |
. . . . . . . . . 10
           |
251 | | fveq2 5863 |
. . . . . . . . . 10
           |
252 | 250, 251 | eqeq12d 2465 |
. . . . . . . . 9
         
           |
253 | 252 | rspcv 3145 |
. . . . . . . 8
   ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)                      |
254 | 92, 90, 253 | mpsyl 65 |
. . . . . . 7
           |
255 | | oveq2 6296 |
. . . . . . . . 9
           |
256 | | eqid 2450 |
. . . . . . . . 9
   ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)        |
257 | | ovex 6316 |
. . . . . . . . 9
     |
258 | 255, 256,
257 | fvmpt 5946 |
. . . . . . . 8
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                |
259 | 23, 258 | ax-mp 5 |
. . . . . . 7
    ![[,] [,]](_icc.gif)               |
260 | | fvex 5873 |
. . . . . . . . 9
     |
261 | 260 | fvconst2 6118 |
. . . . . . . 8
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                  |
262 | 23, 261 | ax-mp 5 |
. . . . . . 7
    ![[,] [,]](_icc.gif)                 |
263 | 254, 259,
262 | 3eqtr4g 2509 |
. . . . . 6
     ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)              |
264 | 1, 19, 3, 117, 119, 62, 214, 218, 249, 263 | cvmliftmoi 29999 |
. . . . 5
    ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)           |
265 | | fconstmpt 4877 |
. . . . 5
   ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)        |
266 | 264, 265 | syl6eq 2500 |
. . . 4
    ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)         |
267 | | mpteqb 5962 |
. . . . 5
 
  ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)              |
268 | | ovex 6316 |
. . . . . 6
     |
269 | 268 | a1i 11 |
. . . . 5
   ![[,] [,]](_icc.gif)        |
270 | 267, 269 | mprg 2750 |
. . . 4
    ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       
  ![[,] [,]](_icc.gif)             |
271 | 266, 270 | sylib 200 |
. . 3
    ![[,] [,]](_icc.gif)             |
272 | 271 | r19.21bi 2756 |
. 2
 
  ![[,] [,]](_icc.gif)             |
273 | 8, 16, 17, 91, 212, 213, 272 | isphtpy2d 22011 |
1
           |