Step | Hyp | Ref
| Expression |
1 | | pi1xfr.j |
. . . 4
TopOn |
2 | | iitopon 22682 |
. . . . . . 7
TopOn |
3 | 2 | a1i 11 |
. . . . . 6
TopOn |
4 | | pi1xfr.f |
. . . . . 6
|
5 | | cnf2 21053 |
. . . . . 6
TopOn TopOn
|
6 | 3, 1, 4, 5 | syl3anc 1326 |
. . . . 5
|
7 | | 0elunit 12290 |
. . . . 5
|
8 | | ffvelrn 6357 |
. . . . 5
|
9 | 6, 7, 8 | sylancl 694 |
. . . 4
|
10 | | pi1xfr.p |
. . . . 5
|
11 | 10 | pi1grp 22850 |
. . . 4
TopOn |
12 | 1, 9, 11 | syl2anc 693 |
. . 3
|
13 | | 1elunit 12291 |
. . . . 5
|
14 | | ffvelrn 6357 |
. . . . 5
|
15 | 6, 13, 14 | sylancl 694 |
. . . 4
|
16 | | pi1xfr.q |
. . . . 5
|
17 | 16 | pi1grp 22850 |
. . . 4
TopOn |
18 | 1, 15, 17 | syl2anc 693 |
. . 3
|
19 | 12, 18 | jca 554 |
. 2
|
20 | | pi1xfr.b |
. . . 4
|
21 | | pi1xfr.g |
. . . 4
|
22 | | pi1xfr.i |
. . . . . . 7
|
23 | 22 | pcorevcl 22825 |
. . . . . 6
|
24 | 4, 23 | syl 17 |
. . . . 5
|
25 | 24 | simp1d 1073 |
. . . 4
|
26 | 24 | simp2d 1074 |
. . . . 5
|
27 | 26 | eqcomd 2628 |
. . . 4
|
28 | 24 | simp3d 1075 |
. . . 4
|
29 | 10, 16, 20, 21, 1, 4, 25, 27, 28 | pi1xfrf 22853 |
. . 3
|
30 | 20 | a1i 11 |
. . . . . . . 8
|
31 | 10, 1, 9, 30 | pi1bas2 22841 |
. . . . . . 7
|
32 | 31 | eleq2d 2687 |
. . . . . 6
|
33 | 32 | biimpa 501 |
. . . . 5
|
34 | | eqid 2622 |
. . . . . 6
|
35 | | oveq1 6657 |
. . . . . . . . 9
|
36 | 35 | fveq2d 6195 |
. . . . . . . 8
|
37 | | fveq2 6191 |
. . . . . . . . 9
|
38 | 37 | oveq1d 6665 |
. . . . . . . 8
|
39 | 36, 38 | eqeq12d 2637 |
. . . . . . 7
|
40 | 39 | ralbidv 2986 |
. . . . . 6
|
41 | 31 | eleq2d 2687 |
. . . . . . . . . 10
|
42 | 41 | biimpa 501 |
. . . . . . . . 9
|
43 | 42 | adantlr 751 |
. . . . . . . 8
|
44 | | oveq2 6658 |
. . . . . . . . . . 11
|
45 | 44 | fveq2d 6195 |
. . . . . . . . . 10
|
46 | | fveq2 6191 |
. . . . . . . . . . 11
|
47 | 46 | oveq2d 6666 |
. . . . . . . . . 10
|
48 | 45, 47 | eqeq12d 2637 |
. . . . . . . . 9
|
49 | | phtpcer 22794 |
. . . . . . . . . . . . . 14
|
50 | 49 | a1i 11 |
. . . . . . . . . . . . 13
|
51 | 10, 1, 9, 30 | pi1eluni 22842 |
. . . . . . . . . . . . . . . . . . . . 21
|
52 | 51 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . 20
|
53 | 52 | simp1d 1073 |
. . . . . . . . . . . . . . . . . . 19
|
54 | 53 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . 18
|
55 | 10, 1, 9, 30 | pi1eluni 22842 |
. . . . . . . . . . . . . . . . . . . . 21
|
56 | 55 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
57 | 56 | biimp3a 1432 |
. . . . . . . . . . . . . . . . . . 19
|
58 | 57 | simp1d 1073 |
. . . . . . . . . . . . . . . . . 18
|
59 | 54, 58 | pco0 22814 |
. . . . . . . . . . . . . . . . 17
|
60 | 52 | simp2d 1074 |
. . . . . . . . . . . . . . . . . 18
|
61 | 60 | 3adant3 1081 |
. . . . . . . . . . . . . . . . 17
|
62 | 59, 61 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
|
63 | 52 | simp3d 1075 |
. . . . . . . . . . . . . . . . . . . 20
|
64 | 63 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . 19
|
65 | 57 | simp2d 1074 |
. . . . . . . . . . . . . . . . . . 19
|
66 | 64, 65 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . 18
|
67 | 54, 58, 66 | pcocn 22817 |
. . . . . . . . . . . . . . . . 17
|
68 | 4 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . 17
|
69 | 67, 68 | pco0 22814 |
. . . . . . . . . . . . . . . 16
|
70 | 28 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . 16
|
71 | 62, 69, 70 | 3eqtr4rd 2667 |
. . . . . . . . . . . . . . 15
|
72 | 25 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . 16
|
73 | 50, 72 | erref 7762 |
. . . . . . . . . . . . . . 15
|
74 | 57 | simp3d 1075 |
. . . . . . . . . . . . . . . . 17
|
75 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
76 | 54, 58, 68, 66, 74, 75 | pcoass 22824 |
. . . . . . . . . . . . . . . 16
|
77 | 58, 68 | pco0 22814 |
. . . . . . . . . . . . . . . . . . 19
|
78 | 66, 77 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . 18
|
79 | 50, 54 | erref 7762 |
. . . . . . . . . . . . . . . . . 18
|
80 | 68, 72 | pco1 22815 |
. . . . . . . . . . . . . . . . . . . . . 22
|
81 | 65, 77, 70 | 3eqtr4rd 2667 |
. . . . . . . . . . . . . . . . . . . . . 22
|
82 | 80, 81 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . 21
|
83 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
84 | 22, 83 | pcorev2 22828 |
. . . . . . . . . . . . . . . . . . . . . 22
|
85 | 68, 84 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
86 | 58, 68, 74 | pcocn 22817 |
. . . . . . . . . . . . . . . . . . . . . 22
|
87 | 50, 86 | erref 7762 |
. . . . . . . . . . . . . . . . . . . . 21
|
88 | 82, 85, 87 | pcohtpy 22820 |
. . . . . . . . . . . . . . . . . . . 20
|
89 | 77, 65 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . 21
|
90 | 83 | pcopt 22822 |
. . . . . . . . . . . . . . . . . . . . 21
|
91 | 86, 89, 90 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
|
92 | 50, 88, 91 | ertrd 7758 |
. . . . . . . . . . . . . . . . . . 19
|
93 | 26 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . 21
|
94 | 93 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . 20
|
95 | 68, 72, 86, 94, 81, 75 | pcoass 22824 |
. . . . . . . . . . . . . . . . . . 19
|
96 | 50, 92, 95 | ertr3d 7760 |
. . . . . . . . . . . . . . . . . 18
|
97 | 78, 79, 96 | pcohtpy 22820 |
. . . . . . . . . . . . . . . . 17
|
98 | 72, 86, 81 | pcocn 22817 |
. . . . . . . . . . . . . . . . . 18
|
99 | 72, 86 | pco0 22814 |
. . . . . . . . . . . . . . . . . . . 20
|
100 | 99, 93 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
|
101 | 100 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . 18
|
102 | 54, 68, 98, 64, 101, 75 | pcoass 22824 |
. . . . . . . . . . . . . . . . 17
|
103 | 50, 97, 102 | ertr4d 7761 |
. . . . . . . . . . . . . . . 16
|
104 | 50, 76, 103 | ertrd 7758 |
. . . . . . . . . . . . . . 15
|
105 | 71, 73, 104 | pcohtpy 22820 |
. . . . . . . . . . . . . 14
|
106 | 4 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
107 | 53, 106, 63 | pcocn 22817 |
. . . . . . . . . . . . . . . 16
|
108 | 107 | 3adant3 1081 |
. . . . . . . . . . . . . . 15
|
109 | 53, 106 | pco0 22814 |
. . . . . . . . . . . . . . . . 17
|
110 | 28 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
111 | 60, 109, 110 | 3eqtr4rd 2667 |
. . . . . . . . . . . . . . . 16
|
112 | 111 | 3adant3 1081 |
. . . . . . . . . . . . . . 15
|
113 | 54, 68 | pco1 22815 |
. . . . . . . . . . . . . . . 16
|
114 | 113, 100 | eqtr4d 2659 |
. . . . . . . . . . . . . . 15
|
115 | 72, 108, 98, 112, 114, 75 | pcoass 22824 |
. . . . . . . . . . . . . 14
|
116 | 50, 105, 115 | ertr4d 7761 |
. . . . . . . . . . . . 13
|
117 | 50, 116 | erthi 7793 |
. . . . . . . . . . . 12
|
118 | 1 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
TopOn |
119 | 54, 58 | pco1 22815 |
. . . . . . . . . . . . . . 15
|
120 | 119, 74 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
121 | 10, 1, 9, 30 | pi1eluni 22842 |
. . . . . . . . . . . . . . 15
|
122 | 121 | 3ad2ant1 1082 |
. . . . . . . . . . . . . 14
|
123 | 67, 62, 120, 122 | mpbir3and 1245 |
. . . . . . . . . . . . 13
|
124 | 10, 16, 20, 21, 118, 68, 72, 94, 70, 123 | pi1xfrval 22854 |
. . . . . . . . . . . 12
|
125 | | eqid 2622 |
. . . . . . . . . . . . 13
|
126 | 15 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
|
127 | | eqid 2622 |
. . . . . . . . . . . . 13
|
128 | 25 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
129 | 128, 107,
111 | pcocn 22817 |
. . . . . . . . . . . . . . 15
|
130 | 129 | 3adant3 1081 |
. . . . . . . . . . . . . 14
|
131 | 128, 107 | pco0 22814 |
. . . . . . . . . . . . . . . 16
|
132 | 26 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
133 | 131, 132 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
134 | 133 | 3adant3 1081 |
. . . . . . . . . . . . . 14
|
135 | 128, 107 | pco1 22815 |
. . . . . . . . . . . . . . . 16
|
136 | 53, 106 | pco1 22815 |
. . . . . . . . . . . . . . . 16
|
137 | 135, 136 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
138 | 137 | 3adant3 1081 |
. . . . . . . . . . . . . 14
|
139 | | eqidd 2623 |
. . . . . . . . . . . . . . 15
|
140 | 16, 118, 126, 139 | pi1eluni 22842 |
. . . . . . . . . . . . . 14
|
141 | 130, 134,
138, 140 | mpbir3and 1245 |
. . . . . . . . . . . . 13
|
142 | 72, 86 | pco1 22815 |
. . . . . . . . . . . . . . 15
|
143 | 58, 68 | pco1 22815 |
. . . . . . . . . . . . . . 15
|
144 | 142, 143 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
145 | 16, 118, 126, 139 | pi1eluni 22842 |
. . . . . . . . . . . . . 14
|
146 | 98, 100, 144, 145 | mpbir3and 1245 |
. . . . . . . . . . . . 13
|
147 | 16, 125, 118, 126, 127, 141, 146 | pi1addval 22848 |
. . . . . . . . . . . 12
|
148 | 117, 124,
147 | 3eqtr4d 2666 |
. . . . . . . . . . 11
|
149 | 9 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
|
150 | | eqid 2622 |
. . . . . . . . . . . . 13
|
151 | | simp2 1062 |
. . . . . . . . . . . . 13
|
152 | | simp3 1063 |
. . . . . . . . . . . . 13
|
153 | 10, 20, 118, 149, 150, 151, 152 | pi1addval 22848 |
. . . . . . . . . . . 12
|
154 | 153 | fveq2d 6195 |
. . . . . . . . . . 11
|
155 | 1 | adantr 481 |
. . . . . . . . . . . . . 14
TopOn |
156 | 27 | adantr 481 |
. . . . . . . . . . . . . 14
|
157 | | simpr 477 |
. . . . . . . . . . . . . 14
|
158 | 10, 16, 20, 21, 155, 106, 128, 156, 110, 157 | pi1xfrval 22854 |
. . . . . . . . . . . . 13
|
159 | 158 | 3adant3 1081 |
. . . . . . . . . . . 12
|
160 | 10, 16, 20, 21, 118, 68, 72, 94, 70, 152 | pi1xfrval 22854 |
. . . . . . . . . . . 12
|
161 | 159, 160 | oveq12d 6668 |
. . . . . . . . . . 11
|
162 | 148, 154,
161 | 3eqtr4d 2666 |
. . . . . . . . . 10
|
163 | 162 | 3expa 1265 |
. . . . . . . . 9
|
164 | 34, 48, 163 | ectocld 7814 |
. . . . . . . 8
|
165 | 43, 164 | syldan 487 |
. . . . . . 7
|
166 | 165 | ralrimiva 2966 |
. . . . . 6
|
167 | 34, 40, 166 | ectocld 7814 |
. . . . 5
|
168 | 33, 167 | syldan 487 |
. . . 4
|
169 | 168 | ralrimiva 2966 |
. . 3
|
170 | 29, 169 | jca 554 |
. 2
|
171 | 20, 125, 150, 127 | isghm 17660 |
. 2
|
172 | 19, 170, 171 | sylanbrc 698 |
1
|