Step | Hyp | Ref
| Expression |
1 | | pi1xfr.j |
. . . 4
 TopOn    |
2 | | iitopon 18862 |
. . . . . . 7
TopOn   ![[,] [,]](_icc.gif)    |
3 | 2 | a1i 11 |
. . . . . 6
 TopOn   ![[,] [,]](_icc.gif)     |
4 | | pi1xfr.f |
. . . . . 6
     |
5 | | cnf2 17267 |
. . . . . 6
  TopOn   ![[,] [,]](_icc.gif)   TopOn 

 
    ![[,] [,]](_icc.gif)      |
6 | 3, 1, 4, 5 | syl3anc 1184 |
. . . . 5
     ![[,] [,]](_icc.gif)      |
7 | | 0elunit 10971 |
. . . . 5
  ![[,] [,]](_icc.gif)   |
8 | | ffvelrn 5827 |
. . . . 5
      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)  
      |
9 | 6, 7, 8 | sylancl 644 |
. . . 4
       |
10 | | pi1xfr.p |
. . . . 5
        |
11 | 10 | pi1grp 19028 |
. . . 4
  TopOn         |
12 | 1, 9, 11 | syl2anc 643 |
. . 3
   |
13 | | 1elunit 10972 |
. . . . 5
  ![[,] [,]](_icc.gif)   |
14 | | ffvelrn 5827 |
. . . . 5
      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)  
      |
15 | 6, 13, 14 | sylancl 644 |
. . . 4
       |
16 | | pi1xfr.q |
. . . . 5
        |
17 | 16 | pi1grp 19028 |
. . . 4
  TopOn         |
18 | 1, 15, 17 | syl2anc 643 |
. . 3
   |
19 | 12, 18 | jca 519 |
. 2
     |
20 | | pi1xfr.b |
. . . 4
     |
21 | | pi1xfr.g |
. . . 4
     ![] ]](rbrack.gif)                      ![] ]](rbrack.gif)      |
22 | | pi1xfr.i |
. . . . . . 7
   ![[,] [,]](_icc.gif)          |
23 | 22 | pcorevcl 19003 |
. . . . . 6
                         |
24 | 4, 23 | syl 16 |
. . . . 5
                       |
25 | 24 | simp1d 969 |
. . . 4
     |
26 | 24 | simp2d 970 |
. . . . 5
           |
27 | 26 | eqcomd 2409 |
. . . 4
           |
28 | 24 | simp3d 971 |
. . . 4
           |
29 | 10, 16, 20, 21, 1, 4, 25, 27, 28 | pi1xfrf 19031 |
. . 3
           |
30 | 20 | a1i 11 |
. . . . . . . 8
       |
31 | 10, 1, 9, 30 | pi1bas2 19019 |
. . . . . . 7
          |
32 | 31 | eleq2d 2471 |
. . . . . 6
     
      |
33 | 32 | biimpa 471 |
. . . . 5
 
          |
34 | | eqid 2404 |
. . . . . 6
               |
35 | | oveq1 6047 |
. . . . . . . . 9
   ![] ]](rbrack.gif)      ![] ]](rbrack.gif)                  |
36 | 35 | fveq2d 5691 |
. . . . . . . 8
   ![] ]](rbrack.gif)         ![] ]](rbrack.gif)                       |
37 | | fveq2 5687 |
. . . . . . . . 9
   ![] ]](rbrack.gif)        ![] ]](rbrack.gif)          |
38 | 37 | oveq1d 6055 |
. . . . . . . 8
   ![] ]](rbrack.gif)         ![] ]](rbrack.gif)
                              |
39 | 36, 38 | eqeq12d 2418 |
. . . . . . 7
   ![] ]](rbrack.gif)          ![] ]](rbrack.gif)                ![] ]](rbrack.gif)
            
                             |
40 | 39 | ralbidv 2686 |
. . . . . 6
   ![] ]](rbrack.gif)    
      ![] ]](rbrack.gif)
               ![] ]](rbrack.gif)
            

                             |
41 | 31 | eleq2d 2471 |
. . . . . . . . . 10
     
      |
42 | 41 | biimpa 471 |
. . . . . . . . 9
 
          |
43 | 42 | adantlr 696 |
. . . . . . . 8
    
          |
44 | | oveq2 6048 |
. . . . . . . . . . 11
   ![] ]](rbrack.gif)      ![] ]](rbrack.gif)          ![] ]](rbrack.gif)       ![] ]](rbrack.gif)           |
45 | 44 | fveq2d 5691 |
. . . . . . . . . 10
   ![] ]](rbrack.gif)         ![] ]](rbrack.gif)          ![] ]](rbrack.gif)           ![] ]](rbrack.gif)            |
46 | | fveq2 5687 |
. . . . . . . . . . 11
   ![] ]](rbrack.gif)        ![] ]](rbrack.gif)          |
47 | 46 | oveq2d 6056 |
. . . . . . . . . 10
   ![] ]](rbrack.gif)         ![] ]](rbrack.gif)
             ![] ]](rbrack.gif)           ![] ]](rbrack.gif)                |
48 | 45, 47 | eqeq12d 2418 |
. . . . . . . . 9
   ![] ]](rbrack.gif)          ![] ]](rbrack.gif)          ![] ]](rbrack.gif)           ![] ]](rbrack.gif)              ![] ]](rbrack.gif)           ![] ]](rbrack.gif)                ![] ]](rbrack.gif)                 |
49 | | phtpcer 18973 |
. . . . . . . . . . . . . 14
  
  |
50 | 49 | a1i 11 |
. . . . . . . . . . . . 13
 
         |
51 | 10, 1, 9, 30 | pi1eluni 19020 |
. . . . . . . . . . . . . . . . . . . . 21
                          |
52 | 51 | biimpa 471 |
. . . . . . . . . . . . . . . . . . . 20
 
                        |
53 | 52 | simp1d 969 |
. . . . . . . . . . . . . . . . . . 19
 
      |
54 | 53 | 3adant3 977 |
. . . . . . . . . . . . . . . . . 18
 
       |
55 | 10, 1, 9, 30 | pi1eluni 19020 |
. . . . . . . . . . . . . . . . . . . . 21
                          |
56 | 55 | adantr 452 |
. . . . . . . . . . . . . . . . . . . 20
 
                           |
57 | 56 | biimp3a 1283 |
. . . . . . . . . . . . . . . . . . 19
 
                         |
58 | 57 | simp1d 969 |
. . . . . . . . . . . . . . . . . 18
 
  
    |
59 | 54, 58 | pco0 18992 |
. . . . . . . . . . . . . . . . 17
 
                     |
60 | 52 | simp2d 970 |
. . . . . . . . . . . . . . . . . 18
 
            |
61 | 60 | 3adant3 977 |
. . . . . . . . . . . . . . . . 17
 
             |
62 | 59, 61 | eqtrd 2436 |
. . . . . . . . . . . . . . . 16
 
                     |
63 | 52 | simp3d 971 |
. . . . . . . . . . . . . . . . . . . 20
 
            |
64 | 63 | 3adant3 977 |
. . . . . . . . . . . . . . . . . . 19
 
             |
65 | 57 | simp2d 970 |
. . . . . . . . . . . . . . . . . . 19
 
             |
66 | 64, 65 | eqtr4d 2439 |
. . . . . . . . . . . . . . . . . 18
 
             |
67 | 54, 58, 66 | pcocn 18995 |
. . . . . . . . . . . . . . . . 17
 
               |
68 | 4 | 3ad2ant1 978 |
. . . . . . . . . . . . . . . . 17
 
  
    |
69 | 67, 68 | pco0 18992 |
. . . . . . . . . . . . . . . 16
 
                                     |
70 | 28 | 3ad2ant1 978 |
. . . . . . . . . . . . . . . 16
 
             |
71 | 62, 69, 70 | 3eqtr4rd 2447 |
. . . . . . . . . . . . . . 15
 
                             |
72 | 25 | 3ad2ant1 978 |
. . . . . . . . . . . . . . . 16
 
  
    |
73 | 50, 72 | erref 6884 |
. . . . . . . . . . . . . . 15
 
         |
74 | 57 | simp3d 971 |
. . . . . . . . . . . . . . . . 17
 
             |
75 | | eqid 2404 |
. . . . . . . . . . . . . . . . 17
   ![[,] [,]](_icc.gif)   
                            ![[,] [,]](_icc.gif)                              |
76 | 54, 58, 68, 66, 74, 75 | pcoass 19002 |
. . . . . . . . . . . . . . . 16
 
                                         |
77 | 58, 68 | pco0 18992 |
. . . . . . . . . . . . . . . . . . 19
 
                     |
78 | 66, 77 | eqtr4d 2439 |
. . . . . . . . . . . . . . . . . 18
 
                     |
79 | 50, 54 | erref 6884 |
. . . . . . . . . . . . . . . . . 18
 
         |
80 | 68, 72 | pco1 18993 |
. . . . . . . . . . . . . . . . . . . . . 22
 
                     |
81 | 65, 77, 70 | 3eqtr4rd 2447 |
. . . . . . . . . . . . . . . . . . . . . 22
 
                     |
82 | 80, 81 | eqtrd 2436 |
. . . . . . . . . . . . . . . . . . . . 21
 
                             |
83 | | eqid 2404 |
. . . . . . . . . . . . . . . . . . . . . . 23
   ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)          |
84 | 22, 83 | pcorev2 19006 |
. . . . . . . . . . . . . . . . . . . . . 22
           
      ![[,] [,]](_icc.gif)           |
85 | 68, 84 | syl 16 |
. . . . . . . . . . . . . . . . . . . . 21
 
                  ![[,] [,]](_icc.gif)           |
86 | 58, 68, 74 | pcocn 18995 |
. . . . . . . . . . . . . . . . . . . . . 22
 
               |
87 | 50, 86 | erref 6884 |
. . . . . . . . . . . . . . . . . . . . 21
 
                         |
88 | 82, 85, 87 | pcohtpy 18998 |
. . . . . . . . . . . . . . . . . . . 20
 
                                   ![[,] [,]](_icc.gif)                          |
89 | 77, 65 | eqtrd 2436 |
. . . . . . . . . . . . . . . . . . . . 21
 
                     |
90 | 83 | pcopt 19000 |
. . . . . . . . . . . . . . . . . . . . 21
                                 ![[,] [,]](_icc.gif)                        
             |
91 | 86, 89, 90 | syl2anc 643 |
. . . . . . . . . . . . . . . . . . . 20
 
       ![[,] [,]](_icc.gif)                                      |
92 | 50, 88, 91 | ertrd 6880 |
. . . . . . . . . . . . . . . . . . 19
 
                                         |
93 | 26 | 3ad2ant1 978 |
. . . . . . . . . . . . . . . . . . . . 21
 
             |
94 | 93 | eqcomd 2409 |
. . . . . . . . . . . . . . . . . . . 20
 
             |
95 | 68, 72, 86, 94, 81, 75 | pcoass 19002 |
. . . . . . . . . . . . . . . . . . 19
 
                                                         |
96 | 50, 92, 95 | ertr3d 6882 |
. . . . . . . . . . . . . . . . . 18
 
                                         |
97 | 78, 79, 96 | pcohtpy 18998 |
. . . . . . . . . . . . . . . . 17
 
                                                         |
98 | 72, 86, 81 | pcocn 18995 |
. . . . . . . . . . . . . . . . . 18
 
                       |
99 | 72, 86 | pco0 18992 |
. . . . . . . . . . . . . . . . . . . 20
 
                             |
100 | 99, 93 | eqtrd 2436 |
. . . . . . . . . . . . . . . . . . 19
 
                             |
101 | 100 | eqcomd 2409 |
. . . . . . . . . . . . . . . . . 18
 
                             |
102 | 54, 68, 98, 64, 101, 75 | pcoass 19002 |
. . . . . . . . . . . . . . . . 17
 
                                                                         |
103 | 50, 97, 102 | ertr4d 6883 |
. . . . . . . . . . . . . . . 16
 
                                                         |
104 | 50, 76, 103 | ertrd 6880 |
. . . . . . . . . . . . . . 15
 
                                                         |
105 | 71, 73, 104 | pcohtpy 18998 |
. . . . . . . . . . . . . 14
 
                                                                         |
106 | 4 | adantr 452 |
. . . . . . . . . . . . . . . . 17
 
      |
107 | 53, 106, 63 | pcocn 18995 |
. . . . . . . . . . . . . . . 16
 
              |
108 | 107 | 3adant3 977 |
. . . . . . . . . . . . . . 15
 
               |
109 | 53, 106 | pco0 18992 |
. . . . . . . . . . . . . . . . 17
 
                    |
110 | 28 | adantr 452 |
. . . . . . . . . . . . . . . . 17
 
            |
111 | 60, 109, 110 | 3eqtr4rd 2447 |
. . . . . . . . . . . . . . . 16
 
                    |
112 | 111 | 3adant3 977 |
. . . . . . . . . . . . . . 15
 
                     |
113 | 54, 68 | pco1 18993 |
. . . . . . . . . . . . . . . 16
 
                     |
114 | 113, 100 | eqtr4d 2439 |
. . . . . . . . . . . . . . 15
 
                                     |
115 | 72, 108, 98, 112, 114, 75 | pcoass 19002 |
. . . . . . . . . . . . . 14
 
                                                                                         |
116 | 50, 105, 115 | ertr4d 6883 |
. . . . . . . . . . . . 13
 
                                                                         |
117 | 50, 116 | erthi 6910 |
. . . . . . . . . . . 12
 
                             ![] ]](rbrack.gif)                                             ![] ]](rbrack.gif)     |
118 | 1 | 3ad2ant1 978 |
. . . . . . . . . . . . 13
 
  
TopOn    |
119 | 54, 58 | pco1 18993 |
. . . . . . . . . . . . . . 15
 
                     |
120 | 119, 74 | eqtrd 2436 |
. . . . . . . . . . . . . 14
 
                     |
121 | 10, 1, 9, 30 | pi1eluni 19020 |
. . . . . . . . . . . . . . 15
                                                          |
122 | 121 | 3ad2ant1 978 |
. . . . . . . . . . . . . 14
 
                                                            |
123 | 67, 62, 120, 122 | mpbir3and 1137 |
. . . . . . . . . . . . 13
 
              |
124 | 10, 16, 20, 21, 118, 68, 72, 94, 70, 123 | pi1xfrval 19032 |
. . . . . . . . . . . 12
 
                ![] ]](rbrack.gif)                              ![] ]](rbrack.gif)     |
125 | | eqid 2404 |
. . . . . . . . . . . . 13
         |
126 | 15 | 3ad2ant1 978 |
. . . . . . . . . . . . 13
 
         |
127 | | eqid 2404 |
. . . . . . . . . . . . 13
       |
128 | 25 | adantr 452 |
. . . . . . . . . . . . . . . 16
 
      |
129 | 128, 107,
111 | pcocn 18995 |
. . . . . . . . . . . . . . 15
 
                      |
130 | 129 | 3adant3 977 |
. . . . . . . . . . . . . 14
 
                       |
131 | 128, 107 | pco0 18992 |
. . . . . . . . . . . . . . . 16
 
                            |
132 | 26 | adantr 452 |
. . . . . . . . . . . . . . . 16
 
            |
133 | 131, 132 | eqtrd 2436 |
. . . . . . . . . . . . . . 15
 
                            |
134 | 133 | 3adant3 977 |
. . . . . . . . . . . . . 14
 
                             |
135 | 128, 107 | pco1 18993 |
. . . . . . . . . . . . . . . 16
 
                                    |
136 | 53, 106 | pco1 18993 |
. . . . . . . . . . . . . . . 16
 
                    |
137 | 135, 136 | eqtrd 2436 |
. . . . . . . . . . . . . . 15
 
                            |
138 | 137 | 3adant3 977 |
. . . . . . . . . . . . . 14
 
                             |
139 | | eqidd 2405 |
. . . . . . . . . . . . . . 15
 
             |
140 | 16, 118, 126, 139 | pi1eluni 19020 |
. . . . . . . . . . . . . 14
 
                                                                                                |
141 | 130, 134,
138, 140 | mpbir3and 1137 |
. . . . . . . . . . . . 13
 
                          |
142 | 72, 86 | pco1 18993 |
. . . . . . . . . . . . . . 15
 
                                     |
143 | 58, 68 | pco1 18993 |
. . . . . . . . . . . . . . 15
 
                     |
144 | 142, 143 | eqtrd 2436 |
. . . . . . . . . . . . . 14
 
                             |
145 | 16, 118, 126, 139 | pi1eluni 19020 |
. . . . . . . . . . . . . 14
 
                                                                                                |
146 | 98, 100, 144, 145 | mpbir3and 1137 |
. . . . . . . . . . . . 13
 
                          |
147 | 16, 125, 118, 126, 127, 141, 146 | pi1addval 19026 |
. . . . . . . . . . . 12
 
                      ![] ]](rbrack.gif)
                         ![] ]](rbrack.gif)
                                             ![] ]](rbrack.gif)     |
148 | 117, 124,
147 | 3eqtr4d 2446 |
. . . . . . . . . . 11
 
                ![] ]](rbrack.gif)                       ![] ]](rbrack.gif)
                         ![] ]](rbrack.gif)
     |
149 | 9 | 3ad2ant1 978 |
. . . . . . . . . . . . 13
 
         |
150 | | eqid 2404 |
. . . . . . . . . . . . 13
       |
151 | | simp2 958 |
. . . . . . . . . . . . 13
 
      |
152 | | simp3 959 |
. . . . . . . . . . . . 13
 
  
   |
153 | 10, 20, 118, 149, 150, 151, 152 | pi1addval 19026 |
. . . . . . . . . . . 12
 
      ![] ]](rbrack.gif)
         ![] ]](rbrack.gif)              ![] ]](rbrack.gif)     |
154 | 153 | fveq2d 5691 |
. . . . . . . . . . 11
 
         ![] ]](rbrack.gif)          ![] ]](rbrack.gif)                  ![] ]](rbrack.gif)
     |
155 | 1 | adantr 452 |
. . . . . . . . . . . . . 14
 
  TopOn    |
156 | 27 | adantr 452 |
. . . . . . . . . . . . . 14
 
            |
157 | | simpr 448 |
. . . . . . . . . . . . . 14
 
     |
158 | 10, 16, 20, 21, 155, 106, 128, 156, 110, 157 | pi1xfrval 19032 |
. . . . . . . . . . . . 13
 
       ![] ]](rbrack.gif)                      ![] ]](rbrack.gif)     |
159 | 158 | 3adant3 977 |
. . . . . . . . . . . 12
 
        ![] ]](rbrack.gif)                      ![] ]](rbrack.gif)     |
160 | 10, 16, 20, 21, 118, 68, 72, 94, 70, 152 | pi1xfrval 19032 |
. . . . . . . . . . . 12
 
        ![] ]](rbrack.gif)                      ![] ]](rbrack.gif)     |
161 | 159, 160 | oveq12d 6058 |
. . . . . . . . . . 11
 
         ![] ]](rbrack.gif)              ![] ]](rbrack.gif)                        ![] ]](rbrack.gif)                          ![] ]](rbrack.gif)      |
162 | 148, 154,
161 | 3eqtr4d 2446 |
. . . . . . . . . 10
 
         ![] ]](rbrack.gif)          ![] ]](rbrack.gif)           ![] ]](rbrack.gif)              ![] ]](rbrack.gif)       |
163 | 162 | 3expa 1153 |
. . . . . . . . 9
    
        ![] ]](rbrack.gif)          ![] ]](rbrack.gif)           ![] ]](rbrack.gif)              ![] ]](rbrack.gif)       |
164 | 34, 48, 163 | ectocld 6930 |
. . . . . . . 8
    
              ![] ]](rbrack.gif)                ![] ]](rbrack.gif)                |
165 | 43, 164 | syldan 457 |
. . . . . . 7
    
       ![] ]](rbrack.gif)                ![] ]](rbrack.gif)                |
166 | 165 | ralrimiva 2749 |
. . . . . 6
 
  
      ![] ]](rbrack.gif)
               ![] ]](rbrack.gif)
               |
167 | 34, 40, 166 | ectocld 6930 |
. . . . 5
 
                                     |
168 | 33, 167 | syldan 457 |
. . . 4
 
 
                            |
169 | 168 | ralrimiva 2749 |
. . 3
  
                            |
170 | 29, 169 | jca 519 |
. 2
           
                             |
171 | 20, 125, 150, 127 | isghm 14961 |
. 2
               

     
                        |
172 | 19, 170, 171 | sylanbrc 646 |
1
     |