Metamath Proof Explorer


Theorem kur14lem7

Description: Lemma for kur14 : main proof. The set T here contains all the distinct combinations of k and c that can arise, and we prove here that applying k or c to any element of T yields another elemnt of T . In operator shorthand, we have T = { A , c A , k A , c k A , k c A , c k c A , k c k A , c k c k A , k c k c A , c k c k c A , k c k c k A , c k c k c k A , k c k c k c A , c k c k c k c A } . From the identities c c A = A and k k A = k A , we can reduce any operator combination containing two adjacent identical operators, which is why the list only contains alternating sequences. The reason the sequences don't keep going after a certain point is due to the identity k c k A = k c k c k c k A , proved in kur14lem6 . (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypotheses kur14lem.j J Top
kur14lem.x X = J
kur14lem.k K = cls J
kur14lem.i I = int J
kur14lem.a A X
kur14lem.b B = X K A
kur14lem.c C = K X A
kur14lem.d D = I K A
kur14lem.t T = A X A K A B C I A K B D K I A I C K D I K B K I C I K I A
Assertion kur14lem7 N T N X X N K N T

Proof

Step Hyp Ref Expression
1 kur14lem.j J Top
2 kur14lem.x X = J
3 kur14lem.k K = cls J
4 kur14lem.i I = int J
5 kur14lem.a A X
6 kur14lem.b B = X K A
7 kur14lem.c C = K X A
8 kur14lem.d D = I K A
9 kur14lem.t T = A X A K A B C I A K B D K I A I C K D I K B K I C I K I A
10 elun N A X A K A B C I A K B D K I A I C K D I K B K I C I K I A N A X A K A B C I A K B D K I A N I C K D I K B K I C I K I A
11 elun N A X A K A B C I A K B D K I A N A X A K A B C I A N K B D K I A
12 elun N A X A K A B C I A N A X A K A N B C I A
13 eltpi N A X A K A N = A N = X A N = K A
14 ssun1 A X A K A A X A K A B C I A
15 ssun1 A X A K A B C I A A X A K A B C I A K B D K I A
16 ssun1 A X A K A B C I A K B D K I A A X A K A B C I A K B D K I A I C K D I K B K I C I K I A
17 16 9 sseqtrri A X A K A B C I A K B D K I A T
18 15 17 sstri A X A K A B C I A T
19 14 18 sstri A X A K A T
20 2 topopn J Top X J
21 1 20 ax-mp X J
22 21 elexi X V
23 difss X A X
24 22 23 ssexi X A V
25 24 tpid2 X A A X A K A
26 19 25 sselii X A T
27 fvex K A V
28 27 tpid3 K A A X A K A
29 19 28 sselii K A T
30 5 26 29 kur14lem1 N = A N X X N K N T
31 1 2 3 4 5 kur14lem4 X X A = A
32 22 5 ssexi A V
33 32 tpid1 A A X A K A
34 19 33 sselii A T
35 31 34 eqeltri X X A T
36 ssun2 B C I A A X A K A B C I A
37 36 18 sstri B C I A T
38 1 2 3 4 23 kur14lem3 K X A X
39 7 38 eqsstri C X
40 22 39 ssexi C V
41 40 tpid2 C B C I A
42 37 41 sselii C T
43 7 42 eqeltrri K X A T
44 23 35 43 kur14lem1 N = X A N X X N K N T
45 1 2 3 4 5 kur14lem3 K A X
46 difss X K A X
47 6 46 eqsstri B X
48 22 47 ssexi B V
49 48 tpid1 B B C I A
50 37 49 sselii B T
51 6 50 eqeltrri X K A T
52 1 2 3 4 5 kur14lem5 K K A = K A
53 52 29 eqeltri K K A T
54 45 51 53 kur14lem1 N = K A N X X N K N T
55 30 44 54 3jaoi N = A N = X A N = K A N X X N K N T
56 13 55 syl N A X A K A N X X N K N T
57 eltpi N B C I A N = B N = C N = I A
58 6 difeq2i X B = X X K A
59 1 2 3 4 45 kur14lem4 X X K A = K A
60 58 59 eqtri X B = K A
61 60 29 eqeltri X B T
62 ssun2 K B D K I A A X A K A B C I A K B D K I A
63 62 17 sstri K B D K I A T
64 fvex K B V
65 64 tpid1 K B K B D K I A
66 63 65 sselii K B T
67 47 61 66 kur14lem1 N = B N X X N K N T
68 7 difeq2i X C = X K X A
69 1 2 3 4 5 kur14lem2 I A = X K X A
70 68 69 eqtr4i X C = I A
71 fvex I A V
72 71 tpid3 I A B C I A
73 37 72 sselii I A T
74 70 73 eqeltri X C T
75 1 2 3 4 23 kur14lem5 K K X A = K X A
76 7 fveq2i K C = K K X A
77 75 76 7 3eqtr4i K C = C
78 77 42 eqeltri K C T
79 39 74 78 kur14lem1 N = C N X X N K N T
80 difss X K X A X
81 69 80 eqsstri I A X
82 70 difeq2i X X C = X I A
83 1 2 3 4 39 kur14lem4 X X C = C
84 82 83 eqtr3i X I A = C
85 84 42 eqeltri X I A T
86 fvex K I A V
87 86 tpid3 K I A K B D K I A
88 63 87 sselii K I A T
89 81 85 88 kur14lem1 N = I A N X X N K N T
90 67 79 89 3jaoi N = B N = C N = I A N X X N K N T
91 57 90 syl N B C I A N X X N K N T
92 56 91 jaoi N A X A K A N B C I A N X X N K N T
93 12 92 sylbi N A X A K A B C I A N X X N K N T
94 eltpi N K B D K I A N = K B N = D N = K I A
95 1 2 3 4 47 kur14lem3 K B X
96 1 2 3 4 45 kur14lem2 I K A = X K X K A
97 6 fveq2i K B = K X K A
98 97 difeq2i X K B = X K X K A
99 96 8 98 3eqtr4i D = X K B
100 8 96 eqtri D = X K X K A
101 difss X K X K A X
102 100 101 eqsstri D X
103 22 102 ssexi D V
104 103 tpid2 D K B D K I A
105 63 104 sselii D T
106 99 105 eqeltrri X K B T
107 1 2 3 4 47 kur14lem5 K K B = K B
108 107 66 eqeltri K K B T
109 95 106 108 kur14lem1 N = K B N X X N K N T
110 99 difeq2i X D = X X K B
111 1 2 3 4 95 kur14lem4 X X K B = K B
112 110 111 eqtri X D = K B
113 112 66 eqeltri X D T
114 ssun1 I C K D I K B I C K D I K B K I C I K I A
115 ssun2 I C K D I K B K I C I K I A A X A K A B C I A K B D K I A I C K D I K B K I C I K I A
116 115 9 sseqtrri I C K D I K B K I C I K I A T
117 114 116 sstri I C K D I K B T
118 fvex K D V
119 118 tpid2 K D I C K D I K B
120 117 119 sselii K D T
121 102 113 120 kur14lem1 N = D N X X N K N T
122 1 2 3 4 81 kur14lem3 K I A X
123 1 2 3 4 39 kur14lem2 I C = X K X C
124 70 fveq2i K X C = K I A
125 124 difeq2i X K X C = X K I A
126 123 125 eqtri I C = X K I A
127 fvex I C V
128 127 tpid1 I C I C K D I K B
129 117 128 sselii I C T
130 126 129 eqeltrri X K I A T
131 1 2 3 4 81 kur14lem5 K K I A = K I A
132 131 88 eqeltri K K I A T
133 122 130 132 kur14lem1 N = K I A N X X N K N T
134 109 121 133 3jaoi N = K B N = D N = K I A N X X N K N T
135 94 134 syl N K B D K I A N X X N K N T
136 93 135 jaoi N A X A K A B C I A N K B D K I A N X X N K N T
137 11 136 sylbi N A X A K A B C I A K B D K I A N X X N K N T
138 elun N I C K D I K B K I C I K I A N I C K D I K B N K I C I K I A
139 eltpi N I C K D I K B N = I C N = K D N = I K B
140 difss X K X C X
141 123 140 eqsstri I C X
142 126 difeq2i X I C = X X K I A
143 1 2 3 4 122 kur14lem4 X X K I A = K I A
144 142 143 eqtri X I C = K I A
145 144 88 eqeltri X I C T
146 ssun2 K I C I K I A I C K D I K B K I C I K I A
147 146 116 sstri K I C I K I A T
148 fvex K I C V
149 148 prid1 K I C K I C I K I A
150 147 149 sselii K I C T
151 141 145 150 kur14lem1 N = I C N X X N K N T
152 1 2 3 4 102 kur14lem3 K D X
153 99 fveq2i K D = K X K B
154 153 difeq2i X K D = X K X K B
155 1 2 3 4 95 kur14lem2 I K B = X K X K B
156 154 155 eqtr4i X K D = I K B
157 fvex I K B V
158 157 tpid3 I K B I C K D I K B
159 117 158 sselii I K B T
160 156 159 eqeltri X K D T
161 1 2 3 4 102 kur14lem5 K K D = K D
162 161 120 eqeltri K K D T
163 152 160 162 kur14lem1 N = K D N X X N K N T
164 difss X K X K B X
165 155 164 eqsstri I K B X
166 156 difeq2i X X K D = X I K B
167 1 2 3 4 152 kur14lem4 X X K D = K D
168 166 167 eqtr3i X I K B = K D
169 168 120 eqeltri X I K B T
170 1 2 3 4 5 6 kur14lem6 K I K B = K B
171 170 66 eqeltri K I K B T
172 165 169 171 kur14lem1 N = I K B N X X N K N T
173 151 163 172 3jaoi N = I C N = K D N = I K B N X X N K N T
174 139 173 syl N I C K D I K B N X X N K N T
175 elpri N K I C I K I A N = K I C N = I K I A
176 1 2 3 4 141 kur14lem3 K I C X
177 126 fveq2i K I C = K X K I A
178 177 difeq2i X K I C = X K X K I A
179 1 2 3 4 122 kur14lem2 I K I A = X K X K I A
180 178 179 eqtr4i X K I C = I K I A
181 fvex I K I A V
182 181 prid2 I K I A K I C I K I A
183 147 182 sselii I K I A T
184 180 183 eqeltri X K I C T
185 1 2 3 4 141 kur14lem5 K K I C = K I C
186 185 150 eqeltri K K I C T
187 176 184 186 kur14lem1 N = K I C N X X N K N T
188 difss X K X K I A X
189 179 188 eqsstri I K I A X
190 180 difeq2i X X K I C = X I K I A
191 1 2 3 4 176 kur14lem4 X X K I C = K I C
192 190 191 eqtr3i X I K I A = K I C
193 192 150 eqeltri X I K I A T
194 1 2 3 4 23 69 kur14lem6 K I K I A = K I A
195 194 88 eqeltri K I K I A T
196 189 193 195 kur14lem1 N = I K I A N X X N K N T
197 187 196 jaoi N = K I C N = I K I A N X X N K N T
198 175 197 syl N K I C I K I A N X X N K N T
199 174 198 jaoi N I C K D I K B N K I C I K I A N X X N K N T
200 138 199 sylbi N I C K D I K B K I C I K I A N X X N K N T
201 137 200 jaoi N A X A K A B C I A K B D K I A N I C K D I K B K I C I K I A N X X N K N T
202 10 201 sylbi N A X A K A B C I A K B D K I A I C K D I K B K I C I K I A N X X N K N T
203 202 9 eleq2s N T N X X N K N T