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

Theorem kur14lem7 24346
Description: Lemma for kur14 24350: 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 24345. (Contributed by Mario Carneiro, 11-Feb-2015.)
Hypotheses
Ref Expression
kur14lem.j  |-  J  e. 
Top
kur14lem.x  |-  X  = 
U. J
kur14lem.k  |-  K  =  ( cls `  J
)
kur14lem.i  |-  I  =  ( int `  J
)
kur14lem.a  |-  A  C_  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
) }  u.  { B ,  C , 
( I `  A
) } )  u. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) } )  u.  ( { ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `
 B ) ) }  u.  { ( K `  ( I `
 C ) ) ,  ( I `  ( K `  ( I `
 A ) ) ) } ) )
Assertion
Ref Expression
kur14lem7  |-  ( N  e.  T  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )

Proof of Theorem kur14lem7
StepHypRef Expression
1 elun 3404 . . 3  |-  ( N  e.  ( ( ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C , 
( I `  A
) } )  u. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) } )  u.  ( { ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `
 B ) ) }  u.  { ( K `  ( I `
 C ) ) ,  ( I `  ( K `  ( I `
 A ) ) ) } ) )  <-> 
( N  e.  ( ( { A , 
( X  \  A
) ,  ( K `
 A ) }  u.  { B ,  C ,  ( I `  A ) } )  u.  { ( K `
 B ) ,  D ,  ( K `
 ( I `  A ) ) } )  \/  N  e.  ( { ( I `
 C ) ,  ( K `  D
) ,  ( I `
 ( K `  B ) ) }  u.  { ( K `
 ( I `  C ) ) ,  ( I `  ( K `  ( I `  A ) ) ) } ) ) )
2 elun 3404 . . . . 5  |-  ( N  e.  ( ( { A ,  ( X 
\  A ) ,  ( K `  A
) }  u.  { B ,  C , 
( I `  A
) } )  u. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) } )  <-> 
( N  e.  ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C , 
( I `  A
) } )  \/  N  e.  { ( K `  B ) ,  D ,  ( K `  ( I `
 A ) ) } ) )
3 elun 3404 . . . . . . 7  |-  ( N  e.  ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C ,  ( I `
 A ) } )  <->  ( N  e. 
{ A ,  ( X  \  A ) ,  ( K `  A ) }  \/  N  e.  { B ,  C ,  ( I `
 A ) } ) )
4 eltpi 3767 . . . . . . . . 9  |-  ( N  e.  { A , 
( X  \  A
) ,  ( K `
 A ) }  ->  ( N  =  A  \/  N  =  ( X  \  A
)  \/  N  =  ( K `  A
) ) )
5 kur14lem.a . . . . . . . . . . 11  |-  A  C_  X
6 ssun1 3426 . . . . . . . . . . . . 13  |-  { A ,  ( X  \  A ) ,  ( K `  A ) }  C_  ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C ,  ( I `
 A ) } )
7 ssun1 3426 . . . . . . . . . . . . . 14  |-  ( { A ,  ( X 
\  A ) ,  ( K `  A
) }  u.  { B ,  C , 
( I `  A
) } )  C_  ( ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C ,  ( I `
 A ) } )  u.  { ( K `  B ) ,  D ,  ( K `  ( I `
 A ) ) } )
8 ssun1 3426 . . . . . . . . . . . . . . 15  |-  ( ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C , 
( I `  A
) } )  u. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) } ) 
C_  ( ( ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C , 
( I `  A
) } )  u. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) } )  u.  ( { ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `
 B ) ) }  u.  { ( K `  ( I `
 C ) ) ,  ( I `  ( K `  ( I `
 A ) ) ) } ) )
9 kur14lem.t . . . . . . . . . . . . . . 15  |-  T  =  ( ( ( { A ,  ( X 
\  A ) ,  ( K `  A
) }  u.  { B ,  C , 
( I `  A
) } )  u. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) } )  u.  ( { ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `
 B ) ) }  u.  { ( K `  ( I `
 C ) ) ,  ( I `  ( K `  ( I `
 A ) ) ) } ) )
108, 9sseqtr4i 3297 . . . . . . . . . . . . . 14  |-  ( ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C , 
( I `  A
) } )  u. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) } ) 
C_  T
117, 10sstri 3274 . . . . . . . . . . . . 13  |-  ( { A ,  ( X 
\  A ) ,  ( K `  A
) }  u.  { B ,  C , 
( I `  A
) } )  C_  T
126, 11sstri 3274 . . . . . . . . . . . 12  |-  { A ,  ( X  \  A ) ,  ( K `  A ) }  C_  T
13 kur14lem.j . . . . . . . . . . . . . . . 16  |-  J  e. 
Top
14 kur14lem.x . . . . . . . . . . . . . . . . 17  |-  X  = 
U. J
1514topopn 16869 . . . . . . . . . . . . . . . 16  |-  ( J  e.  Top  ->  X  e.  J )
1613, 15ax-mp 8 . . . . . . . . . . . . . . 15  |-  X  e.  J
1716elexi 2882 . . . . . . . . . . . . . 14  |-  X  e. 
_V
18 difss 3390 . . . . . . . . . . . . . 14  |-  ( X 
\  A )  C_  X
1917, 18ssexi 4261 . . . . . . . . . . . . 13  |-  ( X 
\  A )  e. 
_V
2019tpid2 3833 . . . . . . . . . . . 12  |-  ( X 
\  A )  e. 
{ A ,  ( X  \  A ) ,  ( K `  A ) }
2112, 20sselii 3263 . . . . . . . . . . 11  |-  ( X 
\  A )  e.  T
22 fvex 5646 . . . . . . . . . . . . 13  |-  ( K `
 A )  e. 
_V
2322tpid3 3835 . . . . . . . . . . . 12  |-  ( K `
 A )  e. 
{ A ,  ( X  \  A ) ,  ( K `  A ) }
2412, 23sselii 3263 . . . . . . . . . . 11  |-  ( K `
 A )  e.  T
255, 21, 24kur14lem1 24340 . . . . . . . . . 10  |-  ( N  =  A  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
26 kur14lem.k . . . . . . . . . . . . 13  |-  K  =  ( cls `  J
)
27 kur14lem.i . . . . . . . . . . . . 13  |-  I  =  ( int `  J
)
2813, 14, 26, 27, 5kur14lem4 24343 . . . . . . . . . . . 12  |-  ( X 
\  ( X  \  A ) )  =  A
2917, 5ssexi 4261 . . . . . . . . . . . . . 14  |-  A  e. 
_V
3029tpid1 3832 . . . . . . . . . . . . 13  |-  A  e. 
{ A ,  ( X  \  A ) ,  ( K `  A ) }
3112, 30sselii 3263 . . . . . . . . . . . 12  |-  A  e.  T
3228, 31eqeltri 2436 . . . . . . . . . . 11  |-  ( X 
\  ( X  \  A ) )  e.  T
33 kur14lem.c . . . . . . . . . . . 12  |-  C  =  ( K `  ( X  \  A ) )
34 ssun2 3427 . . . . . . . . . . . . . 14  |-  { B ,  C ,  ( I `
 A ) } 
C_  ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C ,  ( I `
 A ) } )
3534, 11sstri 3274 . . . . . . . . . . . . 13  |-  { B ,  C ,  ( I `
 A ) } 
C_  T
3613, 14, 26, 27, 18kur14lem3 24342 . . . . . . . . . . . . . . . 16  |-  ( K `
 ( X  \  A ) )  C_  X
3733, 36eqsstri 3294 . . . . . . . . . . . . . . 15  |-  C  C_  X
3817, 37ssexi 4261 . . . . . . . . . . . . . 14  |-  C  e. 
_V
3938tpid2 3833 . . . . . . . . . . . . 13  |-  C  e. 
{ B ,  C ,  ( I `  A ) }
4035, 39sselii 3263 . . . . . . . . . . . 12  |-  C  e.  T
4133, 40eqeltrri 2437 . . . . . . . . . . 11  |-  ( K `
 ( X  \  A ) )  e.  T
4218, 32, 41kur14lem1 24340 . . . . . . . . . 10  |-  ( N  =  ( X  \  A )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
4313, 14, 26, 27, 5kur14lem3 24342 . . . . . . . . . . 11  |-  ( K `
 A )  C_  X
44 kur14lem.b . . . . . . . . . . . 12  |-  B  =  ( X  \  ( K `  A )
)
45 difss 3390 . . . . . . . . . . . . . . . 16  |-  ( X 
\  ( K `  A ) )  C_  X
4644, 45eqsstri 3294 . . . . . . . . . . . . . . 15  |-  B  C_  X
4717, 46ssexi 4261 . . . . . . . . . . . . . 14  |-  B  e. 
_V
4847tpid1 3832 . . . . . . . . . . . . 13  |-  B  e. 
{ B ,  C ,  ( I `  A ) }
4935, 48sselii 3263 . . . . . . . . . . . 12  |-  B  e.  T
5044, 49eqeltrri 2437 . . . . . . . . . . 11  |-  ( X 
\  ( K `  A ) )  e.  T
5113, 14, 26, 27, 5kur14lem5 24344 . . . . . . . . . . . 12  |-  ( K `
 ( K `  A ) )  =  ( K `  A
)
5251, 24eqeltri 2436 . . . . . . . . . . 11  |-  ( K `
 ( K `  A ) )  e.  T
5343, 50, 52kur14lem1 24340 . . . . . . . . . 10  |-  ( N  =  ( K `  A )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
5425, 42, 533jaoi 1246 . . . . . . . . 9  |-  ( ( N  =  A  \/  N  =  ( X  \  A )  \/  N  =  ( K `  A ) )  -> 
( N  C_  X  /\  { ( X  \  N ) ,  ( K `  N ) }  C_  T )
)
554, 54syl 15 . . . . . . . 8  |-  ( N  e.  { A , 
( X  \  A
) ,  ( K `
 A ) }  ->  ( N  C_  X  /\  { ( X 
\  N ) ,  ( K `  N
) }  C_  T
) )
56 eltpi 3767 . . . . . . . . 9  |-  ( N  e.  { B ,  C ,  ( I `  A ) }  ->  ( N  =  B  \/  N  =  C  \/  N  =  ( I `  A ) ) )
5744difeq2i 3378 . . . . . . . . . . . . 13  |-  ( X 
\  B )  =  ( X  \  ( X  \  ( K `  A ) ) )
5813, 14, 26, 27, 43kur14lem4 24343 . . . . . . . . . . . . 13  |-  ( X 
\  ( X  \ 
( K `  A
) ) )  =  ( K `  A
)
5957, 58eqtri 2386 . . . . . . . . . . . 12  |-  ( X 
\  B )  =  ( K `  A
)
6059, 24eqeltri 2436 . . . . . . . . . . 11  |-  ( X 
\  B )  e.  T
61 ssun2 3427 . . . . . . . . . . . . 13  |-  { ( K `  B ) ,  D ,  ( K `  ( I `
 A ) ) }  C_  ( ( { A ,  ( X 
\  A ) ,  ( K `  A
) }  u.  { B ,  C , 
( I `  A
) } )  u. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) } )
6261, 10sstri 3274 . . . . . . . . . . . 12  |-  { ( K `  B ) ,  D ,  ( K `  ( I `
 A ) ) }  C_  T
63 fvex 5646 . . . . . . . . . . . . 13  |-  ( K `
 B )  e. 
_V
6463tpid1 3832 . . . . . . . . . . . 12  |-  ( K `
 B )  e. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) }
6562, 64sselii 3263 . . . . . . . . . . 11  |-  ( K `
 B )  e.  T
6646, 60, 65kur14lem1 24340 . . . . . . . . . 10  |-  ( N  =  B  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
6733difeq2i 3378 . . . . . . . . . . . . 13  |-  ( X 
\  C )  =  ( X  \  ( K `  ( X  \  A ) ) )
6813, 14, 26, 27, 5kur14lem2 24341 . . . . . . . . . . . . 13  |-  ( I `
 A )  =  ( X  \  ( K `  ( X  \  A ) ) )
6967, 68eqtr4i 2389 . . . . . . . . . . . 12  |-  ( X 
\  C )  =  ( I `  A
)
70 fvex 5646 . . . . . . . . . . . . . 14  |-  ( I `
 A )  e. 
_V
7170tpid3 3835 . . . . . . . . . . . . 13  |-  ( I `
 A )  e. 
{ B ,  C ,  ( I `  A ) }
7235, 71sselii 3263 . . . . . . . . . . . 12  |-  ( I `
 A )  e.  T
7369, 72eqeltri 2436 . . . . . . . . . . 11  |-  ( X 
\  C )  e.  T
7413, 14, 26, 27, 18kur14lem5 24344 . . . . . . . . . . . . 13  |-  ( K `
 ( K `  ( X  \  A ) ) )  =  ( K `  ( X 
\  A ) )
7533fveq2i 5635 . . . . . . . . . . . . 13  |-  ( K `
 C )  =  ( K `  ( K `  ( X  \  A ) ) )
7674, 75, 333eqtr4i 2396 . . . . . . . . . . . 12  |-  ( K `
 C )  =  C
7776, 40eqeltri 2436 . . . . . . . . . . 11  |-  ( K `
 C )  e.  T
7837, 73, 77kur14lem1 24340 . . . . . . . . . 10  |-  ( N  =  C  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
79 difss 3390 . . . . . . . . . . . 12  |-  ( X 
\  ( K `  ( X  \  A ) ) )  C_  X
8068, 79eqsstri 3294 . . . . . . . . . . 11  |-  ( I `
 A )  C_  X
8169difeq2i 3378 . . . . . . . . . . . . 13  |-  ( X 
\  ( X  \  C ) )  =  ( X  \  (
I `  A )
)
8213, 14, 26, 27, 37kur14lem4 24343 . . . . . . . . . . . . 13  |-  ( X 
\  ( X  \  C ) )  =  C
8381, 82eqtr3i 2388 . . . . . . . . . . . 12  |-  ( X 
\  ( I `  A ) )  =  C
8483, 40eqeltri 2436 . . . . . . . . . . 11  |-  ( X 
\  ( I `  A ) )  e.  T
85 fvex 5646 . . . . . . . . . . . . 13  |-  ( K `
 ( I `  A ) )  e. 
_V
8685tpid3 3835 . . . . . . . . . . . 12  |-  ( K `
 ( I `  A ) )  e. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) }
8762, 86sselii 3263 . . . . . . . . . . 11  |-  ( K `
 ( I `  A ) )  e.  T
8880, 84, 87kur14lem1 24340 . . . . . . . . . 10  |-  ( N  =  ( I `  A )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
8966, 78, 883jaoi 1246 . . . . . . . . 9  |-  ( ( N  =  B  \/  N  =  C  \/  N  =  ( I `  A ) )  -> 
( N  C_  X  /\  { ( X  \  N ) ,  ( K `  N ) }  C_  T )
)
9056, 89syl 15 . . . . . . . 8  |-  ( N  e.  { B ,  C ,  ( I `  A ) }  ->  ( N  C_  X  /\  { ( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
9155, 90jaoi 368 . . . . . . 7  |-  ( ( N  e.  { A ,  ( X  \  A ) ,  ( K `  A ) }  \/  N  e. 
{ B ,  C ,  ( I `  A ) } )  ->  ( N  C_  X  /\  { ( X 
\  N ) ,  ( K `  N
) }  C_  T
) )
923, 91sylbi 187 . . . . . 6  |-  ( N  e.  ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C ,  ( I `
 A ) } )  ->  ( N  C_  X  /\  { ( X  \  N ) ,  ( K `  N ) }  C_  T ) )
93 eltpi 3767 . . . . . . 7  |-  ( N  e.  { ( K `
 B ) ,  D ,  ( K `
 ( I `  A ) ) }  ->  ( N  =  ( K `  B
)  \/  N  =  D  \/  N  =  ( K `  (
I `  A )
) ) )
9413, 14, 26, 27, 46kur14lem3 24342 . . . . . . . . 9  |-  ( K `
 B )  C_  X
9513, 14, 26, 27, 43kur14lem2 24341 . . . . . . . . . . 11  |-  ( I `
 ( K `  A ) )  =  ( X  \  ( K `  ( X  \  ( K `  A
) ) ) )
96 kur14lem.d . . . . . . . . . . 11  |-  D  =  ( I `  ( K `  A )
)
9744fveq2i 5635 . . . . . . . . . . . 12  |-  ( K `
 B )  =  ( K `  ( X  \  ( K `  A ) ) )
9897difeq2i 3378 . . . . . . . . . . 11  |-  ( X 
\  ( K `  B ) )  =  ( X  \  ( K `  ( X  \  ( K `  A
) ) ) )
9995, 96, 983eqtr4i 2396 . . . . . . . . . 10  |-  D  =  ( X  \  ( K `  B )
)
10096, 95eqtri 2386 . . . . . . . . . . . . . 14  |-  D  =  ( X  \  ( K `  ( X  \  ( K `  A
) ) ) )
101 difss 3390 . . . . . . . . . . . . . 14  |-  ( X 
\  ( K `  ( X  \  ( K `  A )
) ) )  C_  X
102100, 101eqsstri 3294 . . . . . . . . . . . . 13  |-  D  C_  X
10317, 102ssexi 4261 . . . . . . . . . . . 12  |-  D  e. 
_V
104103tpid2 3833 . . . . . . . . . . 11  |-  D  e. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) }
10562, 104sselii 3263 . . . . . . . . . 10  |-  D  e.  T
10699, 105eqeltrri 2437 . . . . . . . . 9  |-  ( X 
\  ( K `  B ) )  e.  T
10713, 14, 26, 27, 46kur14lem5 24344 . . . . . . . . . 10  |-  ( K `
 ( K `  B ) )  =  ( K `  B
)
108107, 65eqeltri 2436 . . . . . . . . 9  |-  ( K `
 ( K `  B ) )  e.  T
10994, 106, 108kur14lem1 24340 . . . . . . . 8  |-  ( N  =  ( K `  B )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
11099difeq2i 3378 . . . . . . . . . . 11  |-  ( X 
\  D )  =  ( X  \  ( X  \  ( K `  B ) ) )
11113, 14, 26, 27, 94kur14lem4 24343 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  B
) ) )  =  ( K `  B
)
112110, 111eqtri 2386 . . . . . . . . . 10  |-  ( X 
\  D )  =  ( K `  B
)
113112, 65eqeltri 2436 . . . . . . . . 9  |-  ( X 
\  D )  e.  T
114 ssun1 3426 . . . . . . . . . . 11  |-  { ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `
 B ) ) }  C_  ( {
( I `  C
) ,  ( K `
 D ) ,  ( I `  ( K `  B )
) }  u.  {
( K `  (
I `  C )
) ,  ( I `
 ( K `  ( I `  A
) ) ) } )
115 ssun2 3427 . . . . . . . . . . . 12  |-  ( { ( I `  C
) ,  ( K `
 D ) ,  ( I `  ( K `  B )
) }  u.  {
( K `  (
I `  C )
) ,  ( I `
 ( K `  ( I `  A
) ) ) } )  C_  ( (
( { A , 
( X  \  A
) ,  ( K `
 A ) }  u.  { B ,  C ,  ( I `  A ) } )  u.  { ( K `
 B ) ,  D ,  ( K `
 ( I `  A ) ) } )  u.  ( { ( I `  C
) ,  ( K `
 D ) ,  ( I `  ( K `  B )
) }  u.  {
( K `  (
I `  C )
) ,  ( I `
 ( K `  ( I `  A
) ) ) } ) )
116115, 9sseqtr4i 3297 . . . . . . . . . . 11  |-  ( { ( I `  C
) ,  ( K `
 D ) ,  ( I `  ( K `  B )
) }  u.  {
( K `  (
I `  C )
) ,  ( I `
 ( K `  ( I `  A
) ) ) } )  C_  T
117114, 116sstri 3274 . . . . . . . . . 10  |-  { ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `
 B ) ) }  C_  T
118 fvex 5646 . . . . . . . . . . 11  |-  ( K `
 D )  e. 
_V
119118tpid2 3833 . . . . . . . . . 10  |-  ( K `
 D )  e. 
{ ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `  B ) ) }
120117, 119sselii 3263 . . . . . . . . 9  |-  ( K `
 D )  e.  T
121102, 113, 120kur14lem1 24340 . . . . . . . 8  |-  ( N  =  D  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
12213, 14, 26, 27, 80kur14lem3 24342 . . . . . . . . 9  |-  ( K `
 ( I `  A ) )  C_  X
12313, 14, 26, 27, 37kur14lem2 24341 . . . . . . . . . . 11  |-  ( I `
 C )  =  ( X  \  ( K `  ( X  \  C ) ) )
12469fveq2i 5635 . . . . . . . . . . . 12  |-  ( K `
 ( X  \  C ) )  =  ( K `  (
I `  A )
)
125124difeq2i 3378 . . . . . . . . . . 11  |-  ( X 
\  ( K `  ( X  \  C ) ) )  =  ( X  \  ( K `
 ( I `  A ) ) )
126123, 125eqtri 2386 . . . . . . . . . 10  |-  ( I `
 C )  =  ( X  \  ( K `  ( I `  A ) ) )
127 fvex 5646 . . . . . . . . . . . 12  |-  ( I `
 C )  e. 
_V
128127tpid1 3832 . . . . . . . . . . 11  |-  ( I `
 C )  e. 
{ ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `  B ) ) }
129117, 128sselii 3263 . . . . . . . . . 10  |-  ( I `
 C )  e.  T
130126, 129eqeltrri 2437 . . . . . . . . 9  |-  ( X 
\  ( K `  ( I `  A
) ) )  e.  T
13113, 14, 26, 27, 80kur14lem5 24344 . . . . . . . . . 10  |-  ( K `
 ( K `  ( I `  A
) ) )  =  ( K `  (
I `  A )
)
132131, 87eqeltri 2436 . . . . . . . . 9  |-  ( K `
 ( K `  ( I `  A
) ) )  e.  T
133122, 130, 132kur14lem1 24340 . . . . . . . 8  |-  ( N  =  ( K `  ( I `  A
) )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
134109, 121, 1333jaoi 1246 . . . . . . 7  |-  ( ( N  =  ( K `
 B )  \/  N  =  D  \/  N  =  ( K `  ( I `  A
) ) )  -> 
( N  C_  X  /\  { ( X  \  N ) ,  ( K `  N ) }  C_  T )
)
13593, 134syl 15 . . . . . 6  |-  ( N  e.  { ( K `
 B ) ,  D ,  ( K `
 ( I `  A ) ) }  ->  ( N  C_  X  /\  { ( X 
\  N ) ,  ( K `  N
) }  C_  T
) )
13692, 135jaoi 368 . . . . 5  |-  ( ( N  e.  ( { A ,  ( X 
\  A ) ,  ( K `  A
) }  u.  { B ,  C , 
( I `  A
) } )  \/  N  e.  { ( K `  B ) ,  D ,  ( K `  ( I `
 A ) ) } )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
1372, 136sylbi 187 . . . 4  |-  ( N  e.  ( ( { A ,  ( X 
\  A ) ,  ( K `  A
) }  u.  { B ,  C , 
( I `  A
) } )  u. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) } )  ->  ( N  C_  X  /\  { ( X 
\  N ) ,  ( K `  N
) }  C_  T
) )
138 elun 3404 . . . . 5  |-  ( N  e.  ( { ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `
 B ) ) }  u.  { ( K `  ( I `
 C ) ) ,  ( I `  ( K `  ( I `
 A ) ) ) } )  <->  ( N  e.  { ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `  B ) ) }  \/  N  e.  { ( K `  ( I `  C
) ) ,  ( I `  ( K `
 ( I `  A ) ) ) } ) )
139 eltpi 3767 . . . . . . 7  |-  ( N  e.  { ( I `
 C ) ,  ( K `  D
) ,  ( I `
 ( K `  B ) ) }  ->  ( N  =  ( I `  C
)  \/  N  =  ( K `  D
)  \/  N  =  ( I `  ( K `  B )
) ) )
140 difss 3390 . . . . . . . . . 10  |-  ( X 
\  ( K `  ( X  \  C ) ) )  C_  X
141123, 140eqsstri 3294 . . . . . . . . 9  |-  ( I `
 C )  C_  X
142126difeq2i 3378 . . . . . . . . . . 11  |-  ( X 
\  ( I `  C ) )  =  ( X  \  ( X  \  ( K `  ( I `  A
) ) ) )
14313, 14, 26, 27, 122kur14lem4 24343 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  (
I `  A )
) ) )  =  ( K `  (
I `  A )
)
144142, 143eqtri 2386 . . . . . . . . . 10  |-  ( X 
\  ( I `  C ) )  =  ( K `  (
I `  A )
)
145144, 87eqeltri 2436 . . . . . . . . 9  |-  ( X 
\  ( I `  C ) )  e.  T
146 ssun2 3427 . . . . . . . . . . 11  |-  { ( K `  ( I `
 C ) ) ,  ( I `  ( K `  ( I `
 A ) ) ) }  C_  ( { ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `  B ) ) }  u.  {
( K `  (
I `  C )
) ,  ( I `
 ( K `  ( I `  A
) ) ) } )
147146, 116sstri 3274 . . . . . . . . . 10  |-  { ( K `  ( I `
 C ) ) ,  ( I `  ( K `  ( I `
 A ) ) ) }  C_  T
148 fvex 5646 . . . . . . . . . . 11  |-  ( K `
 ( I `  C ) )  e. 
_V
149148prid1 3827 . . . . . . . . . 10  |-  ( K `
 ( I `  C ) )  e. 
{ ( K `  ( I `  C
) ) ,  ( I `  ( K `
 ( I `  A ) ) ) }
150147, 149sselii 3263 . . . . . . . . 9  |-  ( K `
 ( I `  C ) )  e.  T
151141, 145, 150kur14lem1 24340 . . . . . . . 8  |-  ( N  =  ( I `  C )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
15213, 14, 26, 27, 102kur14lem3 24342 . . . . . . . . 9  |-  ( K `
 D )  C_  X
15399fveq2i 5635 . . . . . . . . . . . 12  |-  ( K `
 D )  =  ( K `  ( X  \  ( K `  B ) ) )
154153difeq2i 3378 . . . . . . . . . . 11  |-  ( X 
\  ( K `  D ) )  =  ( X  \  ( K `  ( X  \  ( K `  B
) ) ) )
15513, 14, 26, 27, 94kur14lem2 24341 . . . . . . . . . . 11  |-  ( I `
 ( K `  B ) )  =  ( X  \  ( K `  ( X  \  ( K `  B
) ) ) )
156154, 155eqtr4i 2389 . . . . . . . . . 10  |-  ( X 
\  ( K `  D ) )  =  ( I `  ( K `  B )
)
157 fvex 5646 . . . . . . . . . . . 12  |-  ( I `
 ( K `  B ) )  e. 
_V
158157tpid3 3835 . . . . . . . . . . 11  |-  ( I `
 ( K `  B ) )  e. 
{ ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `  B ) ) }
159117, 158sselii 3263 . . . . . . . . . 10  |-  ( I `
 ( K `  B ) )  e.  T
160156, 159eqeltri 2436 . . . . . . . . 9  |-  ( X 
\  ( K `  D ) )  e.  T
16113, 14, 26, 27, 102kur14lem5 24344 . . . . . . . . . 10  |-  ( K `
 ( K `  D ) )  =  ( K `  D
)
162161, 120eqeltri 2436 . . . . . . . . 9  |-  ( K `
 ( K `  D ) )  e.  T
163152, 160, 162kur14lem1 24340 . . . . . . . 8  |-  ( N  =  ( K `  D )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
164 difss 3390 . . . . . . . . . 10  |-  ( X 
\  ( K `  ( X  \  ( K `  B )
) ) )  C_  X
165155, 164eqsstri 3294 . . . . . . . . 9  |-  ( I `
 ( K `  B ) )  C_  X
166156difeq2i 3378 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  D
) ) )  =  ( X  \  (
I `  ( K `  B ) ) )
16713, 14, 26, 27, 152kur14lem4 24343 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  D
) ) )  =  ( K `  D
)
168166, 167eqtr3i 2388 . . . . . . . . . 10  |-  ( X 
\  ( I `  ( K `  B ) ) )  =  ( K `  D )
169168, 120eqeltri 2436 . . . . . . . . 9  |-  ( X 
\  ( I `  ( K `  B ) ) )  e.  T
17013, 14, 26, 27, 5, 44kur14lem6 24345 . . . . . . . . . 10  |-  ( K `
 ( I `  ( K `  B ) ) )  =  ( K `  B )
171170, 65eqeltri 2436 . . . . . . . . 9  |-  ( K `
 ( I `  ( K `  B ) ) )  e.  T
172165, 169, 171kur14lem1 24340 . . . . . . . 8  |-  ( N  =  ( I `  ( K `  B ) )  ->  ( N  C_  X  /\  { ( X  \  N ) ,  ( K `  N ) }  C_  T ) )
173151, 163, 1723jaoi 1246 . . . . . . 7  |-  ( ( N  =  ( I `
 C )  \/  N  =  ( K `
 D )  \/  N  =  ( I `
 ( K `  B ) ) )  ->  ( N  C_  X  /\  { ( X 
\  N ) ,  ( K `  N
) }  C_  T
) )
174139, 173syl 15 . . . . . 6  |-  ( N  e.  { ( I `
 C ) ,  ( K `  D
) ,  ( I `
 ( K `  B ) ) }  ->  ( N  C_  X  /\  { ( X 
\  N ) ,  ( K `  N
) }  C_  T
) )
175 elpri 3749 . . . . . . 7  |-  ( N  e.  { ( K `
 ( I `  C ) ) ,  ( I `  ( K `  ( I `  A ) ) ) }  ->  ( N  =  ( K `  ( I `  C
) )  \/  N  =  ( I `  ( K `  ( I `
 A ) ) ) ) )
17613, 14, 26, 27, 141kur14lem3 24342 . . . . . . . . 9  |-  ( K `
 ( I `  C ) )  C_  X
177126fveq2i 5635 . . . . . . . . . . . 12  |-  ( K `
 ( I `  C ) )  =  ( K `  ( X  \  ( K `  ( I `  A
) ) ) )
178177difeq2i 3378 . . . . . . . . . . 11  |-  ( X 
\  ( K `  ( I `  C
) ) )  =  ( X  \  ( K `  ( X  \  ( K `  (
I `  A )
) ) ) )
17913, 14, 26, 27, 122kur14lem2 24341 . . . . . . . . . . 11  |-  ( I `
 ( K `  ( I `  A
) ) )  =  ( X  \  ( K `  ( X  \  ( K `  (
I `  A )
) ) ) )
180178, 179eqtr4i 2389 . . . . . . . . . 10  |-  ( X 
\  ( K `  ( I `  C
) ) )  =  ( I `  ( K `  ( I `  A ) ) )
181 fvex 5646 . . . . . . . . . . . 12  |-  ( I `
 ( K `  ( I `  A
) ) )  e. 
_V
182181prid2 3828 . . . . . . . . . . 11  |-  ( I `
 ( K `  ( I `  A
) ) )  e. 
{ ( K `  ( I `  C
) ) ,  ( I `  ( K `
 ( I `  A ) ) ) }
183147, 182sselii 3263 . . . . . . . . . 10  |-  ( I `
 ( K `  ( I `  A
) ) )  e.  T
184180, 183eqeltri 2436 . . . . . . . . 9  |-  ( X 
\  ( K `  ( I `  C
) ) )  e.  T
18513, 14, 26, 27, 141kur14lem5 24344 . . . . . . . . . 10  |-  ( K `
 ( K `  ( I `  C
) ) )  =  ( K `  (
I `  C )
)
186185, 150eqeltri 2436 . . . . . . . . 9  |-  ( K `
 ( K `  ( I `  C
) ) )  e.  T
187176, 184, 186kur14lem1 24340 . . . . . . . 8  |-  ( N  =  ( K `  ( I `  C
) )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
188 difss 3390 . . . . . . . . . 10  |-  ( X 
\  ( K `  ( X  \  ( K `  ( I `  A ) ) ) ) )  C_  X
189179, 188eqsstri 3294 . . . . . . . . 9  |-  ( I `
 ( K `  ( I `  A
) ) )  C_  X
190180difeq2i 3378 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  (
I `  C )
) ) )  =  ( X  \  (
I `  ( K `  ( I `  A
) ) ) )
19113, 14, 26, 27, 176kur14lem4 24343 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  (
I `  C )
) ) )  =  ( K `  (
I `  C )
)
192190, 191eqtr3i 2388 . . . . . . . . . 10  |-  ( X 
\  ( I `  ( K `  ( I `
 A ) ) ) )  =  ( K `  ( I `
 C ) )
193192, 150eqeltri 2436 . . . . . . . . 9  |-  ( X 
\  ( I `  ( K `  ( I `
 A ) ) ) )  e.  T
19413, 14, 26, 27, 18, 68kur14lem6 24345 . . . . . . . . . 10  |-  ( K `
 ( I `  ( K `  ( I `
 A ) ) ) )  =  ( K `  ( I `
 A ) )
195194, 87eqeltri 2436 . . . . . . . . 9  |-  ( K `
 ( I `  ( K `  ( I `
 A ) ) ) )  e.  T
196189, 193, 195kur14lem1 24340 . . . . . . . 8  |-  ( N  =  ( I `  ( K `  ( I `
 A ) ) )  ->  ( N  C_  X  /\  { ( X  \  N ) ,  ( K `  N ) }  C_  T ) )
197187, 196jaoi 368 . . . . . . 7  |-  ( ( N  =  ( K `
 ( I `  C ) )  \/  N  =  ( I `
 ( K `  ( I `  A
) ) ) )  ->  ( N  C_  X  /\  { ( X 
\  N ) ,  ( K `  N
) }  C_  T
) )
198175, 197syl 15 . . . . . 6  |-  ( N  e.  { ( K `
 ( I `  C ) ) ,  ( I `  ( K `  ( I `  A ) ) ) }  ->  ( N  C_  X  /\  { ( X  \  N ) ,  ( K `  N ) }  C_  T ) )
199174, 198jaoi 368 . . . . 5  |-  ( ( N  e.  { ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `
 B ) ) }  \/  N  e. 
{ ( K `  ( I `  C
) ) ,  ( I `  ( K `
 ( I `  A ) ) ) } )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
200138, 199sylbi 187 . . . 4  |-  ( N  e.  ( { ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `
 B ) ) }  u.  { ( K `  ( I `
 C ) ) ,  ( I `  ( K `  ( I `
 A ) ) ) } )  -> 
( N  C_  X  /\  { ( X  \  N ) ,  ( K `  N ) }  C_  T )
)
201137, 200jaoi 368 . . 3  |-  ( ( N  e.  ( ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C , 
( I `  A
) } )  u. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) } )  \/  N  e.  ( { ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `  B ) ) }  u.  {
( K `  (
I `  C )
) ,  ( I `
 ( K `  ( I `  A
) ) ) } ) )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
2021, 201sylbi 187 . 2  |-  ( N  e.  ( ( ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C , 
( I `  A
) } )  u. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) } )  u.  ( { ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `
 B ) ) }  u.  { ( K `  ( I `
 C ) ) ,  ( I `  ( K `  ( I `
 A ) ) ) } ) )  ->  ( N  C_  X  /\  { ( X 
\  N ) ,  ( K `  N
) }  C_  T
) )
203202, 9eleq2s 2458 1  |-  ( N  e.  T  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357    /\ wa 358    \/ w3o 934    = wceq 1647    e. wcel 1715    \ cdif 3235    u. cun 3236    C_ wss 3238   {cpr 3730   {ctp 3731   U.cuni 3929   ` cfv 5358   Topctop 16848   intcnt 16971   clsccl 16972
This theorem is referenced by:  kur14lem9  24348
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-13 1717  ax-14 1719  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-rep 4233  ax-sep 4243  ax-nul 4251  ax-pow 4290  ax-pr 4316  ax-un 4615
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 936  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-eu 2221  df-mo 2222  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-ral 2633  df-rex 2634  df-reu 2635  df-rab 2637  df-v 2875  df-sbc 3078  df-csb 3168  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-pw 3716  df-sn 3735  df-pr 3736  df-tp 3737  df-op 3738  df-uni 3930  df-int 3965  df-iun 4009  df-iin 4010  df-br 4126  df-opab 4180  df-mpt 4181  df-id 4412  df-xp 4798  df-rel 4799  df-cnv 4800  df-co 4801  df-dm 4802  df-rn 4803  df-res 4804  df-ima 4805  df-iota 5322  df-fun 5360  df-fn 5361  df-f 5362  df-f1 5363  df-fo 5364  df-f1o 5365  df-fv 5366  df-top 16853  df-cld 16973  df-ntr 16974  df-cls 16975
  Copyright terms: Public domain W3C validator