Step | Hyp | Ref
| Expression |
1 | | pi1co.j |
. . . 4
 TopOn    |
2 | | pi1co.a |
. . . 4
   |
3 | | pi1co.p |
. . . . 5
    |
4 | 3 | pi1grp 22074 |
. . . 4
  TopOn     |
5 | 1, 2, 4 | syl2anc 666 |
. . 3
   |
6 | | pi1co.f |
. . . . . 6
     |
7 | | cntop2 20250 |
. . . . . 6
     |
8 | 6, 7 | syl 17 |
. . . . 5
   |
9 | | eqid 2450 |
. . . . . 6
   |
10 | 9 | toptopon 19941 |
. . . . 5

TopOn     |
11 | 8, 10 | sylib 200 |
. . . 4
 TopOn     |
12 | | pi1co.b |
. . . . 5
       |
13 | | cnf2 20258 |
. . . . . . 7
  TopOn  TopOn     
       |
14 | 1, 11, 6, 13 | syl3anc 1267 |
. . . . . 6
        |
15 | 14, 2 | ffvelrnd 6021 |
. . . . 5
        |
16 | 12, 15 | eqeltrrd 2529 |
. . . 4
    |
17 | | pi1co.q |
. . . . 5
    |
18 | 17 | pi1grp 22074 |
. . . 4
  TopOn    
  |
19 | 11, 16, 18 | syl2anc 666 |
. . 3
   |
20 | 5, 19 | jca 535 |
. 2
     |
21 | | pi1co.v |
. . . 4
     |
22 | | pi1co.g |
. . . 4
     ![] ]](rbrack.gif)        ![] ]](rbrack.gif)      |
23 | 3, 17, 21, 22, 1, 6, 2, 12 | pi1cof 22083 |
. . 3
           |
24 | 21 | a1i 11 |
. . . . . . . 8
       |
25 | 3, 1, 2, 24 | pi1bas2 22065 |
. . . . . . 7
          |
26 | 25 | eleq2d 2513 |
. . . . . 6
     
      |
27 | 26 | biimpa 487 |
. . . . 5
 
          |
28 | | eqid 2450 |
. . . . . 6
               |
29 | | oveq1 6295 |
. . . . . . . . 9
   ![] ]](rbrack.gif)      ![] ]](rbrack.gif)                  |
30 | 29 | fveq2d 5867 |
. . . . . . . 8
   ![] ]](rbrack.gif)         ![] ]](rbrack.gif)                       |
31 | | fveq2 5863 |
. . . . . . . . 9
   ![] ]](rbrack.gif)        ![] ]](rbrack.gif)          |
32 | 31 | oveq1d 6303 |
. . . . . . . 8
   ![] ]](rbrack.gif)         ![] ]](rbrack.gif)
                              |
33 | 30, 32 | eqeq12d 2465 |
. . . . . . 7
   ![] ]](rbrack.gif)          ![] ]](rbrack.gif)                ![] ]](rbrack.gif)
            
                             |
34 | 33 | ralbidv 2826 |
. . . . . 6
   ![] ]](rbrack.gif)    
      ![] ]](rbrack.gif)
               ![] ]](rbrack.gif)
            

                             |
35 | | oveq2 6296 |
. . . . . . . . . . 11
   ![] ]](rbrack.gif)      ![] ]](rbrack.gif)          ![] ]](rbrack.gif)       ![] ]](rbrack.gif)           |
36 | 35 | fveq2d 5867 |
. . . . . . . . . 10
   ![] ]](rbrack.gif)         ![] ]](rbrack.gif)          ![] ]](rbrack.gif)           ![] ]](rbrack.gif)            |
37 | | fveq2 5863 |
. . . . . . . . . . 11
   ![] ]](rbrack.gif)        ![] ]](rbrack.gif)          |
38 | 37 | oveq2d 6304 |
. . . . . . . . . 10
   ![] ]](rbrack.gif)         ![] ]](rbrack.gif)
             ![] ]](rbrack.gif)           ![] ]](rbrack.gif)                |
39 | 36, 38 | eqeq12d 2465 |
. . . . . . . . 9
   ![] ]](rbrack.gif)          ![] ]](rbrack.gif)          ![] ]](rbrack.gif)           ![] ]](rbrack.gif)              ![] ]](rbrack.gif)           ![] ]](rbrack.gif)                ![] ]](rbrack.gif)                 |
40 | 3, 1, 2, 24 | pi1eluni 22066 |
. . . . . . . . . . . . . . . 16
                  |
41 | 40 | biimpa 487 |
. . . . . . . . . . . . . . 15
 
                |
42 | 41 | simp1d 1019 |
. . . . . . . . . . . . . 14
 
      |
43 | 42 | adantr 467 |
. . . . . . . . . . . . 13
    
      |
44 | 1 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
  TopOn    |
45 | 2 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
    |
46 | 21 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
        |
47 | 3, 44, 45, 46 | pi1eluni 22066 |
. . . . . . . . . . . . . . 15
 
                   |
48 | 47 | biimpa 487 |
. . . . . . . . . . . . . 14
    
    
           |
49 | 48 | simp1d 1019 |
. . . . . . . . . . . . 13
    
      |
50 | 41 | simp3d 1021 |
. . . . . . . . . . . . . . 15
 
        |
51 | 50 | adantr 467 |
. . . . . . . . . . . . . 14
    
        |
52 | 48 | simp2d 1020 |
. . . . . . . . . . . . . 14
    
        |
53 | 51, 52 | eqtr4d 2487 |
. . . . . . . . . . . . 13
    
            |
54 | 6 | ad2antrr 731 |
. . . . . . . . . . . . 13
    
      |
55 | 43, 49, 53, 54 | copco 22042 |
. . . . . . . . . . . 12
    
                          |
56 | 55 | eceq1d 7397 |
. . . . . . . . . . 11
    
              ![] ]](rbrack.gif)
                ![] ]](rbrack.gif)
    |
57 | 43, 49, 53 | pcocn 22041 |
. . . . . . . . . . . . 13
    
              |
58 | 43, 49 | pco0 22038 |
. . . . . . . . . . . . . 14
    
                    |
59 | 41 | simp2d 1020 |
. . . . . . . . . . . . . . 15
 
        |
60 | 59 | adantr 467 |
. . . . . . . . . . . . . 14
    
        |
61 | 58, 60 | eqtrd 2484 |
. . . . . . . . . . . . 13
    
                |
62 | 43, 49 | pco1 22039 |
. . . . . . . . . . . . . 14
    
                    |
63 | 48 | simp3d 1021 |
. . . . . . . . . . . . . 14
    
        |
64 | 62, 63 | eqtrd 2484 |
. . . . . . . . . . . . 13
    
                |
65 | 1 | ad2antrr 731 |
. . . . . . . . . . . . . 14
    
  TopOn    |
66 | 2 | ad2antrr 731 |
. . . . . . . . . . . . . 14
    
    |
67 | 21 | a1i 11 |
. . . . . . . . . . . . . 14
    
        |
68 | 3, 65, 66, 67 | pi1eluni 22066 |
. . . . . . . . . . . . 13
    
           
                                       |
69 | 57, 61, 64, 68 | mpbir3and 1190 |
. . . . . . . . . . . 12
    
             |
70 | 3, 17, 21, 22, 1, 6, 2, 12 | pi1coval 22084 |
. . . . . . . . . . . . 13
 
                       ![] ]](rbrack.gif)                ![] ]](rbrack.gif)     |
71 | 70 | adantlr 720 |
. . . . . . . . . . . 12
              
             ![] ]](rbrack.gif)                ![] ]](rbrack.gif)
    |
72 | 69, 71 | syldan 473 |
. . . . . . . . . . 11
    
               ![] ]](rbrack.gif)                ![] ]](rbrack.gif)
    |
73 | | eqid 2450 |
. . . . . . . . . . . 12
         |
74 | 11 | ad2antrr 731 |
. . . . . . . . . . . 12
    
  TopOn     |
75 | 16 | ad2antrr 731 |
. . . . . . . . . . . 12
    
     |
76 | | eqid 2450 |
. . . . . . . . . . . 12
       |
77 | 6 | adantr 467 |
. . . . . . . . . . . . . . 15
 
      |
78 | | cnco 20275 |
. . . . . . . . . . . . . . 15
   
         |
79 | 42, 77, 78 | syl2anc 666 |
. . . . . . . . . . . . . 14
 
  
     |
80 | | iitopon 21904 |
. . . . . . . . . . . . . . . . . 18
TopOn   ![[,] [,]](_icc.gif)    |
81 | 80 | a1i 11 |
. . . . . . . . . . . . . . . . 17
 
  TopOn   ![[,] [,]](_icc.gif)     |
82 | | cnf2 20258 |
. . . . . . . . . . . . . . . . 17
  TopOn   ![[,] [,]](_icc.gif)   TopOn 

 
    ![[,] [,]](_icc.gif)      |
83 | 81, 44, 42, 82 | syl3anc 1267 |
. . . . . . . . . . . . . . . 16
 
      ![[,] [,]](_icc.gif)      |
84 | | 0elunit 11747 |
. . . . . . . . . . . . . . . 16
  ![[,] [,]](_icc.gif)   |
85 | | fvco3 5940 |
. . . . . . . . . . . . . . . 16
      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)  
 
              |
86 | 83, 84, 85 | sylancl 667 |
. . . . . . . . . . . . . . 15
 
                  |
87 | 59 | fveq2d 5867 |
. . . . . . . . . . . . . . 15
 
                |
88 | 12 | adantr 467 |
. . . . . . . . . . . . . . 15
 
        |
89 | 86, 87, 88 | 3eqtrd 2488 |
. . . . . . . . . . . . . 14
 
          |
90 | | 1elunit 11748 |
. . . . . . . . . . . . . . . 16
  ![[,] [,]](_icc.gif)   |
91 | | fvco3 5940 |
. . . . . . . . . . . . . . . 16
      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)  
 
              |
92 | 83, 90, 91 | sylancl 667 |
. . . . . . . . . . . . . . 15
 
                  |
93 | 50 | fveq2d 5867 |
. . . . . . . . . . . . . . 15
 
                |
94 | 92, 93, 88 | 3eqtrd 2488 |
. . . . . . . . . . . . . 14
 
          |
95 | 11 | adantr 467 |
. . . . . . . . . . . . . . 15
 
  TopOn     |
96 | 16 | adantr 467 |
. . . . . . . . . . . . . . 15
 
     |
97 | | eqidd 2451 |
. . . . . . . . . . . . . . 15
 
            |
98 | 17, 95, 96, 97 | pi1eluni 22066 |
. . . . . . . . . . . . . 14
 
         
 
  
 
              |
99 | 79, 89, 94, 98 | mpbir3and 1190 |
. . . . . . . . . . . . 13
 
  
        |
100 | 99 | adantr 467 |
. . . . . . . . . . . 12
    
           |
101 | | cnco 20275 |
. . . . . . . . . . . . . 14
   
         |
102 | 49, 54, 101 | syl2anc 666 |
. . . . . . . . . . . . 13
    
        |
103 | 80 | a1i 11 |
. . . . . . . . . . . . . . . 16
    
  TopOn   ![[,] [,]](_icc.gif)     |
104 | | cnf2 20258 |
. . . . . . . . . . . . . . . 16
  TopOn   ![[,] [,]](_icc.gif)   TopOn 

 
    ![[,] [,]](_icc.gif)      |
105 | 103, 65, 49, 104 | syl3anc 1267 |
. . . . . . . . . . . . . . 15
    
      ![[,] [,]](_icc.gif)      |
106 | | fvco3 5940 |
. . . . . . . . . . . . . . 15
      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)  
 
              |
107 | 105, 84, 106 | sylancl 667 |
. . . . . . . . . . . . . 14
    
                  |
108 | 52 | fveq2d 5867 |
. . . . . . . . . . . . . 14
    
                |
109 | 12 | ad2antrr 731 |
. . . . . . . . . . . . . 14
    
        |
110 | 107, 108,
109 | 3eqtrd 2488 |
. . . . . . . . . . . . 13
    
          |
111 | | fvco3 5940 |
. . . . . . . . . . . . . . 15
      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)  
 
              |
112 | 105, 90, 111 | sylancl 667 |
. . . . . . . . . . . . . 14
    
                  |
113 | 63 | fveq2d 5867 |
. . . . . . . . . . . . . 14
    
                |
114 | 112, 113,
109 | 3eqtrd 2488 |
. . . . . . . . . . . . 13
    
          |
115 | | eqidd 2451 |
. . . . . . . . . . . . . . 15
           |
116 | 17, 11, 16, 115 | pi1eluni 22066 |
. . . . . . . . . . . . . 14
                              |
117 | 116 | ad2antrr 731 |
. . . . . . . . . . . . 13
    
              
 
              |
118 | 102, 110,
114, 117 | mpbir3and 1190 |
. . . . . . . . . . . 12
    
           |
119 | 17, 73, 74, 75, 76, 100, 118 | pi1addval 22072 |
. . . . . . . . . . 11
    
       ![] ]](rbrack.gif)            ![] ]](rbrack.gif)
                 ![] ]](rbrack.gif)     |
120 | 56, 72, 119 | 3eqtr4d 2494 |
. . . . . . . . . 10
    
               ![] ]](rbrack.gif)         ![] ]](rbrack.gif)            ![] ]](rbrack.gif)
     |
121 | | eqid 2450 |
. . . . . . . . . . . 12
       |
122 | | simplr 761 |
. . . . . . . . . . . 12
    
     |
123 | | simpr 463 |
. . . . . . . . . . . 12
    
     |
124 | 3, 21, 65, 66, 121, 122, 123 | pi1addval 22072 |
. . . . . . . . . . 11
    
     ![] ]](rbrack.gif)          ![] ]](rbrack.gif)              ![] ]](rbrack.gif)     |
125 | 124 | fveq2d 5867 |
. . . . . . . . . 10
    
        ![] ]](rbrack.gif)          ![] ]](rbrack.gif)                  ![] ]](rbrack.gif)
     |
126 | 3, 17, 21, 22, 1, 6, 2, 12 | pi1coval 22084 |
. . . . . . . . . . . 12
 
       ![] ]](rbrack.gif)        ![] ]](rbrack.gif)     |
127 | 126 | adantr 467 |
. . . . . . . . . . 11
    
       ![] ]](rbrack.gif)        ![] ]](rbrack.gif)
    |
128 | 3, 17, 21, 22, 1, 6, 2, 12 | pi1coval 22084 |
. . . . . . . . . . . 12
 
       ![] ]](rbrack.gif)        ![] ]](rbrack.gif)     |
129 | 128 | adantlr 720 |
. . . . . . . . . . 11
    
       ![] ]](rbrack.gif)        ![] ]](rbrack.gif)
    |
130 | 127, 129 | oveq12d 6306 |
. . . . . . . . . 10
    
        ![] ]](rbrack.gif)
             ![] ]](rbrack.gif)          ![] ]](rbrack.gif)            ![] ]](rbrack.gif)      |
131 | 120, 125,
130 | 3eqtr4d 2494 |
. . . . . . . . 9
    
        ![] ]](rbrack.gif)          ![] ]](rbrack.gif)           ![] ]](rbrack.gif)              ![] ]](rbrack.gif)       |
132 | 28, 39, 131 | ectocld 7427 |
. . . . . . . 8
    
              ![] ]](rbrack.gif)                ![] ]](rbrack.gif)                |
133 | 132 | ralrimiva 2801 |
. . . . . . 7
 
                 ![] ]](rbrack.gif)                ![] ]](rbrack.gif)                |
134 | 25 | adantr 467 |
. . . . . . . 8
 
     
     |
135 | 134 | raleqdv 2992 |
. . . . . . 7
 
   
      ![] ]](rbrack.gif)                ![] ]](rbrack.gif)              
              ![] ]](rbrack.gif)                ![] ]](rbrack.gif)                 |
136 | 133, 135 | mpbird 236 |
. . . . . 6
 
  
      ![] ]](rbrack.gif)
               ![] ]](rbrack.gif)
               |
137 | 28, 34, 136 | ectocld 7427 |
. . . . 5
 
                                     |
138 | 27, 137 | syldan 473 |
. . . 4
 
 
                            |
139 | 138 | ralrimiva 2801 |
. . 3
  
                            |
140 | 23, 139 | jca 535 |
. 2
           
                             |
141 | 21, 73, 121, 76 | isghm 16876 |
. 2
               

     
                        |
142 | 20, 140, 141 | sylanbrc 669 |
1
     |