Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  kur14lem7 Structured version   Visualization version   Unicode version

Theorem kur14lem7 29935
 Description: Lemma for kur14 29939: main proof. The set here contains all the distinct combinations of and that can arise, and we prove here that applying or to any element of yields another elemnt of . In operator shorthand, we have . From the identities and , 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 , proved in kur14lem6 29934. (Contributed by Mario Carneiro, 11-Feb-2015.)
Hypotheses
Ref Expression
kur14lem.j
kur14lem.x
kur14lem.k
kur14lem.i
kur14lem.a
kur14lem.b
kur14lem.c
kur14lem.d
kur14lem.t
Assertion
Ref Expression
kur14lem7

Proof of Theorem kur14lem7
StepHypRef Expression
1 elun 3574 . . 3
2 elun 3574 . . . . 5
3 elun 3574 . . . . . . 7
4 eltpi 4016 . . . . . . . . 9
5 kur14lem.a . . . . . . . . . . 11
6 ssun1 3597 . . . . . . . . . . . . 13
7 ssun1 3597 . . . . . . . . . . . . . 14
8 ssun1 3597 . . . . . . . . . . . . . . 15
9 kur14lem.t . . . . . . . . . . . . . . 15
108, 9sseqtr4i 3465 . . . . . . . . . . . . . 14
117, 10sstri 3441 . . . . . . . . . . . . 13
126, 11sstri 3441 . . . . . . . . . . . 12
13 kur14lem.j . . . . . . . . . . . . . . . 16
14 kur14lem.x . . . . . . . . . . . . . . . . 17
1514topopn 19936 . . . . . . . . . . . . . . . 16
1613, 15ax-mp 5 . . . . . . . . . . . . . . 15
1716elexi 3055 . . . . . . . . . . . . . 14
18 difss 3560 . . . . . . . . . . . . . 14
1917, 18ssexi 4548 . . . . . . . . . . . . 13
2019tpid2 4086 . . . . . . . . . . . 12
2112, 20sselii 3429 . . . . . . . . . . 11
22 fvex 5875 . . . . . . . . . . . . 13
2322tpid3 4088 . . . . . . . . . . . 12
2412, 23sselii 3429 . . . . . . . . . . 11
255, 21, 24kur14lem1 29929 . . . . . . . . . 10
26 kur14lem.k . . . . . . . . . . . . 13
27 kur14lem.i . . . . . . . . . . . . 13
2813, 14, 26, 27, 5kur14lem4 29932 . . . . . . . . . . . 12
2917, 5ssexi 4548 . . . . . . . . . . . . . 14
3029tpid1 4085 . . . . . . . . . . . . 13
3112, 30sselii 3429 . . . . . . . . . . . 12
3228, 31eqeltri 2525 . . . . . . . . . . 11
33 kur14lem.c . . . . . . . . . . . 12
34 ssun2 3598 . . . . . . . . . . . . . 14
3534, 11sstri 3441 . . . . . . . . . . . . 13
3613, 14, 26, 27, 18kur14lem3 29931 . . . . . . . . . . . . . . . 16
3733, 36eqsstri 3462 . . . . . . . . . . . . . . 15
3817, 37ssexi 4548 . . . . . . . . . . . . . 14
3938tpid2 4086 . . . . . . . . . . . . 13
4035, 39sselii 3429 . . . . . . . . . . . 12
4133, 40eqeltrri 2526 . . . . . . . . . . 11
4218, 32, 41kur14lem1 29929 . . . . . . . . . 10
4313, 14, 26, 27, 5kur14lem3 29931 . . . . . . . . . . 11
44 kur14lem.b . . . . . . . . . . . 12
45 difss 3560 . . . . . . . . . . . . . . . 16
4644, 45eqsstri 3462 . . . . . . . . . . . . . . 15
4717, 46ssexi 4548 . . . . . . . . . . . . . 14
4847tpid1 4085 . . . . . . . . . . . . 13
4935, 48sselii 3429 . . . . . . . . . . . 12
5044, 49eqeltrri 2526 . . . . . . . . . . 11
5113, 14, 26, 27, 5kur14lem5 29933 . . . . . . . . . . . 12
5251, 24eqeltri 2525 . . . . . . . . . . 11
5343, 50, 52kur14lem1 29929 . . . . . . . . . 10
5425, 42, 533jaoi 1331 . . . . . . . . 9
554, 54syl 17 . . . . . . . 8
56 eltpi 4016 . . . . . . . . 9
5744difeq2i 3548 . . . . . . . . . . . . 13
5813, 14, 26, 27, 43kur14lem4 29932 . . . . . . . . . . . . 13
5957, 58eqtri 2473 . . . . . . . . . . . 12
6059, 24eqeltri 2525 . . . . . . . . . . 11
61 ssun2 3598 . . . . . . . . . . . . 13
6261, 10sstri 3441 . . . . . . . . . . . 12
63 fvex 5875 . . . . . . . . . . . . 13
6463tpid1 4085 . . . . . . . . . . . 12
6562, 64sselii 3429 . . . . . . . . . . 11
6646, 60, 65kur14lem1 29929 . . . . . . . . . 10
6733difeq2i 3548 . . . . . . . . . . . . 13
6813, 14, 26, 27, 5kur14lem2 29930 . . . . . . . . . . . . 13
6967, 68eqtr4i 2476 . . . . . . . . . . . 12
70 fvex 5875 . . . . . . . . . . . . . 14
7170tpid3 4088 . . . . . . . . . . . . 13
7235, 71sselii 3429 . . . . . . . . . . . 12
7369, 72eqeltri 2525 . . . . . . . . . . 11
7413, 14, 26, 27, 18kur14lem5 29933 . . . . . . . . . . . . 13
7533fveq2i 5868 . . . . . . . . . . . . 13
7674, 75, 333eqtr4i 2483 . . . . . . . . . . . 12
7776, 40eqeltri 2525 . . . . . . . . . . 11
7837, 73, 77kur14lem1 29929 . . . . . . . . . 10
79 difss 3560 . . . . . . . . . . . 12
8068, 79eqsstri 3462 . . . . . . . . . . 11
8169difeq2i 3548 . . . . . . . . . . . . 13
8213, 14, 26, 27, 37kur14lem4 29932 . . . . . . . . . . . . 13
8381, 82eqtr3i 2475 . . . . . . . . . . . 12
8483, 40eqeltri 2525 . . . . . . . . . . 11
85 fvex 5875 . . . . . . . . . . . . 13
8685tpid3 4088 . . . . . . . . . . . 12
8762, 86sselii 3429 . . . . . . . . . . 11
8880, 84, 87kur14lem1 29929 . . . . . . . . . 10
8966, 78, 883jaoi 1331 . . . . . . . . 9
9056, 89syl 17 . . . . . . . 8
9155, 90jaoi 381 . . . . . . 7
923, 91sylbi 199 . . . . . 6
93 eltpi 4016 . . . . . . 7
9413, 14, 26, 27, 46kur14lem3 29931 . . . . . . . . 9
9513, 14, 26, 27, 43kur14lem2 29930 . . . . . . . . . . 11
96 kur14lem.d . . . . . . . . . . 11
9744fveq2i 5868 . . . . . . . . . . . 12
9897difeq2i 3548 . . . . . . . . . . 11
9995, 96, 983eqtr4i 2483 . . . . . . . . . 10
10096, 95eqtri 2473 . . . . . . . . . . . . . 14
101 difss 3560 . . . . . . . . . . . . . 14
102100, 101eqsstri 3462 . . . . . . . . . . . . 13
10317, 102ssexi 4548 . . . . . . . . . . . 12
104103tpid2 4086 . . . . . . . . . . 11
10562, 104sselii 3429 . . . . . . . . . 10
10699, 105eqeltrri 2526 . . . . . . . . 9
10713, 14, 26, 27, 46kur14lem5 29933 . . . . . . . . . 10
108107, 65eqeltri 2525 . . . . . . . . 9
10994, 106, 108kur14lem1 29929 . . . . . . . 8
11099difeq2i 3548 . . . . . . . . . . 11
11113, 14, 26, 27, 94kur14lem4 29932 . . . . . . . . . . 11
112110, 111eqtri 2473 . . . . . . . . . 10
113112, 65eqeltri 2525 . . . . . . . . 9
114 ssun1 3597 . . . . . . . . . . 11
115 ssun2 3598 . . . . . . . . . . . 12
116115, 9sseqtr4i 3465 . . . . . . . . . . 11
117114, 116sstri 3441 . . . . . . . . . 10
118 fvex 5875 . . . . . . . . . . 11
119118tpid2 4086 . . . . . . . . . 10
120117, 119sselii 3429 . . . . . . . . 9
121102, 113, 120kur14lem1 29929 . . . . . . . 8
12213, 14, 26, 27, 80kur14lem3 29931 . . . . . . . . 9
12313, 14, 26, 27, 37kur14lem2 29930 . . . . . . . . . . 11
12469fveq2i 5868 . . . . . . . . . . . 12
125124difeq2i 3548 . . . . . . . . . . 11
126123, 125eqtri 2473 . . . . . . . . . 10
127 fvex 5875 . . . . . . . . . . . 12
128127tpid1 4085 . . . . . . . . . . 11
129117, 128sselii 3429 . . . . . . . . . 10
130126, 129eqeltrri 2526 . . . . . . . . 9
13113, 14, 26, 27, 80kur14lem5 29933 . . . . . . . . . 10
132131, 87eqeltri 2525 . . . . . . . . 9
133122, 130, 132kur14lem1 29929 . . . . . . . 8
134109, 121, 1333jaoi 1331 . . . . . . 7
13593, 134syl 17 . . . . . 6
13692, 135jaoi 381 . . . . 5
1372, 136sylbi 199 . . . 4
138 elun 3574 . . . . 5
139 eltpi 4016 . . . . . . 7
140 difss 3560 . . . . . . . . . 10
141123, 140eqsstri 3462 . . . . . . . . 9
142126difeq2i 3548 . . . . . . . . . . 11
14313, 14, 26, 27, 122kur14lem4 29932 . . . . . . . . . . 11
144142, 143eqtri 2473 . . . . . . . . . 10
145144, 87eqeltri 2525 . . . . . . . . 9
146 ssun2 3598 . . . . . . . . . . 11
147146, 116sstri 3441 . . . . . . . . . 10
148 fvex 5875 . . . . . . . . . . 11
149148prid1 4080 . . . . . . . . . 10
150147, 149sselii 3429 . . . . . . . . 9
151141, 145, 150kur14lem1 29929 . . . . . . . 8
15213, 14, 26, 27, 102kur14lem3 29931 . . . . . . . . 9
15399fveq2i 5868 . . . . . . . . . . . 12
154153difeq2i 3548 . . . . . . . . . . 11
15513, 14, 26, 27, 94kur14lem2 29930 . . . . . . . . . . 11
156154, 155eqtr4i 2476 . . . . . . . . . 10
157 fvex 5875 . . . . . . . . . . . 12
158157tpid3 4088 . . . . . . . . . . 11
159117, 158sselii 3429 . . . . . . . . . 10
160156, 159eqeltri 2525 . . . . . . . . 9
16113, 14, 26, 27, 102kur14lem5 29933 . . . . . . . . . 10
162161, 120eqeltri 2525 . . . . . . . . 9
163152, 160, 162kur14lem1 29929 . . . . . . . 8
164 difss 3560 . . . . . . . . . 10
165155, 164eqsstri 3462 . . . . . . . . 9
166156difeq2i 3548 . . . . . . . . . . 11
16713, 14, 26, 27, 152kur14lem4 29932 . . . . . . . . . . 11
168166, 167eqtr3i 2475 . . . . . . . . . 10
169168, 120eqeltri 2525 . . . . . . . . 9
17013, 14, 26, 27, 5, 44kur14lem6 29934 . . . . . . . . . 10
171170, 65eqeltri 2525 . . . . . . . . 9
172165, 169, 171kur14lem1 29929 . . . . . . . 8
173151, 163, 1723jaoi 1331 . . . . . . 7
174139, 173syl 17 . . . . . 6
175 elpri 3985 . . . . . . 7
17613, 14, 26, 27, 141kur14lem3 29931 . . . . . . . . 9
177126fveq2i 5868 . . . . . . . . . . . 12
178177difeq2i 3548 . . . . . . . . . . 11
17913, 14, 26, 27, 122kur14lem2 29930 . . . . . . . . . . 11
180178, 179eqtr4i 2476 . . . . . . . . . 10
181 fvex 5875 . . . . . . . . . . . 12
182181prid2 4081 . . . . . . . . . . 11
183147, 182sselii 3429 . . . . . . . . . 10
184180, 183eqeltri 2525 . . . . . . . . 9
18513, 14, 26, 27, 141kur14lem5 29933 . . . . . . . . . 10
186185, 150eqeltri 2525 . . . . . . . . 9
187176, 184, 186kur14lem1 29929 . . . . . . . 8
188 difss 3560 . . . . . . . . . 10
189179, 188eqsstri 3462 . . . . . . . . 9
190180difeq2i 3548 . . . . . . . . . . 11
19113, 14, 26, 27, 176kur14lem4 29932 . . . . . . . . . . 11
192190, 191eqtr3i 2475 . . . . . . . . . 10
193192, 150eqeltri 2525 . . . . . . . . 9
19413, 14, 26, 27, 18, 68kur14lem6 29934 . . . . . . . . . 10
195194, 87eqeltri 2525 . . . . . . . . 9
196189, 193, 195kur14lem1 29929 . . . . . . . 8
197187, 196jaoi 381 . . . . . . 7
198175, 197syl 17 . . . . . 6
199174, 198jaoi 381 . . . . 5
200138, 199sylbi 199 . . . 4
201137, 200jaoi 381 . . 3
2021, 201sylbi 199 . 2
203202, 9eleq2s 2547 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wo 370   wa 371   w3o 984   wceq 1444   wcel 1887   cdif 3401   cun 3402   wss 3404  cpr 3970  ctp 3972  cuni 4198  cfv 5582  ctop 19917  cnt 20032  ccl 20033 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-int 4235  df-iun 4280  df-iin 4281  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-top 19921  df-cld 20034  df-ntr 20035  df-cls 20036 This theorem is referenced by:  kur14lem9  29937
 Copyright terms: Public domain W3C validator