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

Theorem kur14lem7 24859
Description: Lemma for kur14 24863: 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 24858. (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 3456 . . 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 3456 . . . . 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 3456 . . . . . . 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 3820 . . . . . . . . 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 3478 . . . . . . . . . . . . 13  |-  { A ,  ( X  \  A ) ,  ( K `  A ) }  C_  ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C ,  ( I `
 A ) } )
7 ssun1 3478 . . . . . . . . . . . . . 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 3478 . . . . . . . . . . . . . . 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 3349 . . . . . . . . . . . . . 14  |-  ( ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C , 
( I `  A
) } )  u. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) } ) 
C_  T
117, 10sstri 3325 . . . . . . . . . . . . 13  |-  ( { A ,  ( X 
\  A ) ,  ( K `  A
) }  u.  { B ,  C , 
( I `  A
) } )  C_  T
126, 11sstri 3325 . . . . . . . . . . . 12  |-  { A ,  ( X  \  A ) ,  ( K `  A ) }  C_  T
13 kur14lem.j . . . . . . . . . . . . . . . 16  |-  J  e. 
Top
14 kur14lem.x . . . . . . . . . . . . . . . . 17  |-  X  = 
U. J
1514topopn 16942 . . . . . . . . . . . . . . . 16  |-  ( J  e.  Top  ->  X  e.  J )
1613, 15ax-mp 8 . . . . . . . . . . . . . . 15  |-  X  e.  J
1716elexi 2933 . . . . . . . . . . . . . 14  |-  X  e. 
_V
18 difss 3442 . . . . . . . . . . . . . 14  |-  ( X 
\  A )  C_  X
1917, 18ssexi 4316 . . . . . . . . . . . . 13  |-  ( X 
\  A )  e. 
_V
2019tpid2 3886 . . . . . . . . . . . 12  |-  ( X 
\  A )  e. 
{ A ,  ( X  \  A ) ,  ( K `  A ) }
2112, 20sselii 3313 . . . . . . . . . . 11  |-  ( X 
\  A )  e.  T
22 fvex 5709 . . . . . . . . . . . . 13  |-  ( K `
 A )  e. 
_V
2322tpid3 3888 . . . . . . . . . . . 12  |-  ( K `
 A )  e. 
{ A ,  ( X  \  A ) ,  ( K `  A ) }
2412, 23sselii 3313 . . . . . . . . . . 11  |-  ( K `
 A )  e.  T
255, 21, 24kur14lem1 24853 . . . . . . . . . 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 24856 . . . . . . . . . . . 12  |-  ( X 
\  ( X  \  A ) )  =  A
2917, 5ssexi 4316 . . . . . . . . . . . . . 14  |-  A  e. 
_V
3029tpid1 3885 . . . . . . . . . . . . 13  |-  A  e. 
{ A ,  ( X  \  A ) ,  ( K `  A ) }
3112, 30sselii 3313 . . . . . . . . . . . 12  |-  A  e.  T
3228, 31eqeltri 2482 . . . . . . . . . . 11  |-  ( X 
\  ( X  \  A ) )  e.  T
33 kur14lem.c . . . . . . . . . . . 12  |-  C  =  ( K `  ( X  \  A ) )
34 ssun2 3479 . . . . . . . . . . . . . 14  |-  { B ,  C ,  ( I `
 A ) } 
C_  ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C ,  ( I `
 A ) } )
3534, 11sstri 3325 . . . . . . . . . . . . 13  |-  { B ,  C ,  ( I `
 A ) } 
C_  T
3613, 14, 26, 27, 18kur14lem3 24855 . . . . . . . . . . . . . . . 16  |-  ( K `
 ( X  \  A ) )  C_  X
3733, 36eqsstri 3346 . . . . . . . . . . . . . . 15  |-  C  C_  X
3817, 37ssexi 4316 . . . . . . . . . . . . . 14  |-  C  e. 
_V
3938tpid2 3886 . . . . . . . . . . . . 13  |-  C  e. 
{ B ,  C ,  ( I `  A ) }
4035, 39sselii 3313 . . . . . . . . . . . 12  |-  C  e.  T
4133, 40eqeltrri 2483 . . . . . . . . . . 11  |-  ( K `
 ( X  \  A ) )  e.  T
4218, 32, 41kur14lem1 24853 . . . . . . . . . 10  |-  ( N  =  ( X  \  A )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
4313, 14, 26, 27, 5kur14lem3 24855 . . . . . . . . . . 11  |-  ( K `
 A )  C_  X
44 kur14lem.b . . . . . . . . . . . 12  |-  B  =  ( X  \  ( K `  A )
)
45 difss 3442 . . . . . . . . . . . . . . . 16  |-  ( X 
\  ( K `  A ) )  C_  X
4644, 45eqsstri 3346 . . . . . . . . . . . . . . 15  |-  B  C_  X
4717, 46ssexi 4316 . . . . . . . . . . . . . 14  |-  B  e. 
_V
4847tpid1 3885 . . . . . . . . . . . . 13  |-  B  e. 
{ B ,  C ,  ( I `  A ) }
4935, 48sselii 3313 . . . . . . . . . . . 12  |-  B  e.  T
5044, 49eqeltrri 2483 . . . . . . . . . . 11  |-  ( X 
\  ( K `  A ) )  e.  T
5113, 14, 26, 27, 5kur14lem5 24857 . . . . . . . . . . . 12  |-  ( K `
 ( K `  A ) )  =  ( K `  A
)
5251, 24eqeltri 2482 . . . . . . . . . . 11  |-  ( K `
 ( K `  A ) )  e.  T
5343, 50, 52kur14lem1 24853 . . . . . . . . . 10  |-  ( N  =  ( K `  A )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
5425, 42, 533jaoi 1247 . . . . . . . . 9  |-  ( ( N  =  A  \/  N  =  ( X  \  A )  \/  N  =  ( K `  A ) )  -> 
( N  C_  X  /\  { ( X  \  N ) ,  ( K `  N ) }  C_  T )
)
554, 54syl 16 . . . . . . . 8  |-  ( N  e.  { A , 
( X  \  A
) ,  ( K `
 A ) }  ->  ( N  C_  X  /\  { ( X 
\  N ) ,  ( K `  N
) }  C_  T
) )
56 eltpi 3820 . . . . . . . . 9  |-  ( N  e.  { B ,  C ,  ( I `  A ) }  ->  ( N  =  B  \/  N  =  C  \/  N  =  ( I `  A ) ) )
5744difeq2i 3430 . . . . . . . . . . . . 13  |-  ( X 
\  B )  =  ( X  \  ( X  \  ( K `  A ) ) )
5813, 14, 26, 27, 43kur14lem4 24856 . . . . . . . . . . . . 13  |-  ( X 
\  ( X  \ 
( K `  A
) ) )  =  ( K `  A
)
5957, 58eqtri 2432 . . . . . . . . . . . 12  |-  ( X 
\  B )  =  ( K `  A
)
6059, 24eqeltri 2482 . . . . . . . . . . 11  |-  ( X 
\  B )  e.  T
61 ssun2 3479 . . . . . . . . . . . . 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 3325 . . . . . . . . . . . 12  |-  { ( K `  B ) ,  D ,  ( K `  ( I `
 A ) ) }  C_  T
63 fvex 5709 . . . . . . . . . . . . 13  |-  ( K `
 B )  e. 
_V
6463tpid1 3885 . . . . . . . . . . . 12  |-  ( K `
 B )  e. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) }
6562, 64sselii 3313 . . . . . . . . . . 11  |-  ( K `
 B )  e.  T
6646, 60, 65kur14lem1 24853 . . . . . . . . . 10  |-  ( N  =  B  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
6733difeq2i 3430 . . . . . . . . . . . . 13  |-  ( X 
\  C )  =  ( X  \  ( K `  ( X  \  A ) ) )
6813, 14, 26, 27, 5kur14lem2 24854 . . . . . . . . . . . . 13  |-  ( I `
 A )  =  ( X  \  ( K `  ( X  \  A ) ) )
6967, 68eqtr4i 2435 . . . . . . . . . . . 12  |-  ( X 
\  C )  =  ( I `  A
)
70 fvex 5709 . . . . . . . . . . . . . 14  |-  ( I `
 A )  e. 
_V
7170tpid3 3888 . . . . . . . . . . . . 13  |-  ( I `
 A )  e. 
{ B ,  C ,  ( I `  A ) }
7235, 71sselii 3313 . . . . . . . . . . . 12  |-  ( I `
 A )  e.  T
7369, 72eqeltri 2482 . . . . . . . . . . 11  |-  ( X 
\  C )  e.  T
7413, 14, 26, 27, 18kur14lem5 24857 . . . . . . . . . . . . 13  |-  ( K `
 ( K `  ( X  \  A ) ) )  =  ( K `  ( X 
\  A ) )
7533fveq2i 5698 . . . . . . . . . . . . 13  |-  ( K `
 C )  =  ( K `  ( K `  ( X  \  A ) ) )
7674, 75, 333eqtr4i 2442 . . . . . . . . . . . 12  |-  ( K `
 C )  =  C
7776, 40eqeltri 2482 . . . . . . . . . . 11  |-  ( K `
 C )  e.  T
7837, 73, 77kur14lem1 24853 . . . . . . . . . 10  |-  ( N  =  C  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
79 difss 3442 . . . . . . . . . . . 12  |-  ( X 
\  ( K `  ( X  \  A ) ) )  C_  X
8068, 79eqsstri 3346 . . . . . . . . . . 11  |-  ( I `
 A )  C_  X
8169difeq2i 3430 . . . . . . . . . . . . 13  |-  ( X 
\  ( X  \  C ) )  =  ( X  \  (
I `  A )
)
8213, 14, 26, 27, 37kur14lem4 24856 . . . . . . . . . . . . 13  |-  ( X 
\  ( X  \  C ) )  =  C
8381, 82eqtr3i 2434 . . . . . . . . . . . 12  |-  ( X 
\  ( I `  A ) )  =  C
8483, 40eqeltri 2482 . . . . . . . . . . 11  |-  ( X 
\  ( I `  A ) )  e.  T
85 fvex 5709 . . . . . . . . . . . . 13  |-  ( K `
 ( I `  A ) )  e. 
_V
8685tpid3 3888 . . . . . . . . . . . 12  |-  ( K `
 ( I `  A ) )  e. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) }
8762, 86sselii 3313 . . . . . . . . . . 11  |-  ( K `
 ( I `  A ) )  e.  T
8880, 84, 87kur14lem1 24853 . . . . . . . . . 10  |-  ( N  =  ( I `  A )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
8966, 78, 883jaoi 1247 . . . . . . . . 9  |-  ( ( N  =  B  \/  N  =  C  \/  N  =  ( I `  A ) )  -> 
( N  C_  X  /\  { ( X  \  N ) ,  ( K `  N ) }  C_  T )
)
9056, 89syl 16 . . . . . . . 8  |-  ( N  e.  { B ,  C ,  ( I `  A ) }  ->  ( N  C_  X  /\  { ( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
9155, 90jaoi 369 . . . . . . 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 188 . . . . . 6  |-  ( N  e.  ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C ,  ( I `
 A ) } )  ->  ( N  C_  X  /\  { ( X  \  N ) ,  ( K `  N ) }  C_  T ) )
93 eltpi 3820 . . . . . . 7  |-  ( N  e.  { ( K `
 B ) ,  D ,  ( K `
 ( I `  A ) ) }  ->  ( N  =  ( K `  B
)  \/  N  =  D  \/  N  =  ( K `  (
I `  A )
) ) )
9413, 14, 26, 27, 46kur14lem3 24855 . . . . . . . . 9  |-  ( K `
 B )  C_  X
9513, 14, 26, 27, 43kur14lem2 24854 . . . . . . . . . . 11  |-  ( I `
 ( K `  A ) )  =  ( X  \  ( K `  ( X  \  ( K `  A
) ) ) )
96 kur14lem.d . . . . . . . . . . 11  |-  D  =  ( I `  ( K `  A )
)
9744fveq2i 5698 . . . . . . . . . . . 12  |-  ( K `
 B )  =  ( K `  ( X  \  ( K `  A ) ) )
9897difeq2i 3430 . . . . . . . . . . 11  |-  ( X 
\  ( K `  B ) )  =  ( X  \  ( K `  ( X  \  ( K `  A
) ) ) )
9995, 96, 983eqtr4i 2442 . . . . . . . . . 10  |-  D  =  ( X  \  ( K `  B )
)
10096, 95eqtri 2432 . . . . . . . . . . . . . 14  |-  D  =  ( X  \  ( K `  ( X  \  ( K `  A
) ) ) )
101 difss 3442 . . . . . . . . . . . . . 14  |-  ( X 
\  ( K `  ( X  \  ( K `  A )
) ) )  C_  X
102100, 101eqsstri 3346 . . . . . . . . . . . . 13  |-  D  C_  X
10317, 102ssexi 4316 . . . . . . . . . . . 12  |-  D  e. 
_V
104103tpid2 3886 . . . . . . . . . . 11  |-  D  e. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) }
10562, 104sselii 3313 . . . . . . . . . 10  |-  D  e.  T
10699, 105eqeltrri 2483 . . . . . . . . 9  |-  ( X 
\  ( K `  B ) )  e.  T
10713, 14, 26, 27, 46kur14lem5 24857 . . . . . . . . . 10  |-  ( K `
 ( K `  B ) )  =  ( K `  B
)
108107, 65eqeltri 2482 . . . . . . . . 9  |-  ( K `
 ( K `  B ) )  e.  T
10994, 106, 108kur14lem1 24853 . . . . . . . 8  |-  ( N  =  ( K `  B )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
11099difeq2i 3430 . . . . . . . . . . 11  |-  ( X 
\  D )  =  ( X  \  ( X  \  ( K `  B ) ) )
11113, 14, 26, 27, 94kur14lem4 24856 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  B
) ) )  =  ( K `  B
)
112110, 111eqtri 2432 . . . . . . . . . 10  |-  ( X 
\  D )  =  ( K `  B
)
113112, 65eqeltri 2482 . . . . . . . . 9  |-  ( X 
\  D )  e.  T
114 ssun1 3478 . . . . . . . . . . 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 3479 . . . . . . . . . . . 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 3349 . . . . . . . . . . 11  |-  ( { ( I `  C
) ,  ( K `
 D ) ,  ( I `  ( K `  B )
) }  u.  {
( K `  (
I `  C )
) ,  ( I `
 ( K `  ( I `  A
) ) ) } )  C_  T
117114, 116sstri 3325 . . . . . . . . . 10  |-  { ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `
 B ) ) }  C_  T
118 fvex 5709 . . . . . . . . . . 11  |-  ( K `
 D )  e. 
_V
119118tpid2 3886 . . . . . . . . . 10  |-  ( K `
 D )  e. 
{ ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `  B ) ) }
120117, 119sselii 3313 . . . . . . . . 9  |-  ( K `
 D )  e.  T
121102, 113, 120kur14lem1 24853 . . . . . . . 8  |-  ( N  =  D  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
12213, 14, 26, 27, 80kur14lem3 24855 . . . . . . . . 9  |-  ( K `
 ( I `  A ) )  C_  X
12313, 14, 26, 27, 37kur14lem2 24854 . . . . . . . . . . 11  |-  ( I `
 C )  =  ( X  \  ( K `  ( X  \  C ) ) )
12469fveq2i 5698 . . . . . . . . . . . 12  |-  ( K `
 ( X  \  C ) )  =  ( K `  (
I `  A )
)
125124difeq2i 3430 . . . . . . . . . . 11  |-  ( X 
\  ( K `  ( X  \  C ) ) )  =  ( X  \  ( K `
 ( I `  A ) ) )
126123, 125eqtri 2432 . . . . . . . . . 10  |-  ( I `
 C )  =  ( X  \  ( K `  ( I `  A ) ) )
127 fvex 5709 . . . . . . . . . . . 12  |-  ( I `
 C )  e. 
_V
128127tpid1 3885 . . . . . . . . . . 11  |-  ( I `
 C )  e. 
{ ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `  B ) ) }
129117, 128sselii 3313 . . . . . . . . . 10  |-  ( I `
 C )  e.  T
130126, 129eqeltrri 2483 . . . . . . . . 9  |-  ( X 
\  ( K `  ( I `  A
) ) )  e.  T
13113, 14, 26, 27, 80kur14lem5 24857 . . . . . . . . . 10  |-  ( K `
 ( K `  ( I `  A
) ) )  =  ( K `  (
I `  A )
)
132131, 87eqeltri 2482 . . . . . . . . 9  |-  ( K `
 ( K `  ( I `  A
) ) )  e.  T
133122, 130, 132kur14lem1 24853 . . . . . . . 8  |-  ( N  =  ( K `  ( I `  A
) )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
134109, 121, 1333jaoi 1247 . . . . . . 7  |-  ( ( N  =  ( K `
 B )  \/  N  =  D  \/  N  =  ( K `  ( I `  A
) ) )  -> 
( N  C_  X  /\  { ( X  \  N ) ,  ( K `  N ) }  C_  T )
)
13593, 134syl 16 . . . . . 6  |-  ( N  e.  { ( K `
 B ) ,  D ,  ( K `
 ( I `  A ) ) }  ->  ( N  C_  X  /\  { ( X 
\  N ) ,  ( K `  N
) }  C_  T
) )
13692, 135jaoi 369 . . . . 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 188 . . . 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 3456 . . . . 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 3820 . . . . . . 7  |-  ( N  e.  { ( I `
 C ) ,  ( K `  D
) ,  ( I `
 ( K `  B ) ) }  ->  ( N  =  ( I `  C
)  \/  N  =  ( K `  D
)  \/  N  =  ( I `  ( K `  B )
) ) )
140 difss 3442 . . . . . . . . . 10  |-  ( X 
\  ( K `  ( X  \  C ) ) )  C_  X
141123, 140eqsstri 3346 . . . . . . . . 9  |-  ( I `
 C )  C_  X
142126difeq2i 3430 . . . . . . . . . . 11  |-  ( X 
\  ( I `  C ) )  =  ( X  \  ( X  \  ( K `  ( I `  A
) ) ) )
14313, 14, 26, 27, 122kur14lem4 24856 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  (
I `  A )
) ) )  =  ( K `  (
I `  A )
)
144142, 143eqtri 2432 . . . . . . . . . 10  |-  ( X 
\  ( I `  C ) )  =  ( K `  (
I `  A )
)
145144, 87eqeltri 2482 . . . . . . . . 9  |-  ( X 
\  ( I `  C ) )  e.  T
146 ssun2 3479 . . . . . . . . . . 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 3325 . . . . . . . . . 10  |-  { ( K `  ( I `
 C ) ) ,  ( I `  ( K `  ( I `
 A ) ) ) }  C_  T
148 fvex 5709 . . . . . . . . . . 11  |-  ( K `
 ( I `  C ) )  e. 
_V
149148prid1 3880 . . . . . . . . . 10  |-  ( K `
 ( I `  C ) )  e. 
{ ( K `  ( I `  C
) ) ,  ( I `  ( K `
 ( I `  A ) ) ) }
150147, 149sselii 3313 . . . . . . . . 9  |-  ( K `
 ( I `  C ) )  e.  T
151141, 145, 150kur14lem1 24853 . . . . . . . 8  |-  ( N  =  ( I `  C )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
15213, 14, 26, 27, 102kur14lem3 24855 . . . . . . . . 9  |-  ( K `
 D )  C_  X
15399fveq2i 5698 . . . . . . . . . . . 12  |-  ( K `
 D )  =  ( K `  ( X  \  ( K `  B ) ) )
154153difeq2i 3430 . . . . . . . . . . 11  |-  ( X 
\  ( K `  D ) )  =  ( X  \  ( K `  ( X  \  ( K `  B
) ) ) )
15513, 14, 26, 27, 94kur14lem2 24854 . . . . . . . . . . 11  |-  ( I `
 ( K `  B ) )  =  ( X  \  ( K `  ( X  \  ( K `  B
) ) ) )
156154, 155eqtr4i 2435 . . . . . . . . . 10  |-  ( X 
\  ( K `  D ) )  =  ( I `  ( K `  B )
)
157 fvex 5709 . . . . . . . . . . . 12  |-  ( I `
 ( K `  B ) )  e. 
_V
158157tpid3 3888 . . . . . . . . . . 11  |-  ( I `
 ( K `  B ) )  e. 
{ ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `  B ) ) }
159117, 158sselii 3313 . . . . . . . . . 10  |-  ( I `
 ( K `  B ) )  e.  T
160156, 159eqeltri 2482 . . . . . . . . 9  |-  ( X 
\  ( K `  D ) )  e.  T
16113, 14, 26, 27, 102kur14lem5 24857 . . . . . . . . . 10  |-  ( K `
 ( K `  D ) )  =  ( K `  D
)
162161, 120eqeltri 2482 . . . . . . . . 9  |-  ( K `
 ( K `  D ) )  e.  T
163152, 160, 162kur14lem1 24853 . . . . . . . 8  |-  ( N  =  ( K `  D )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
164 difss 3442 . . . . . . . . . 10  |-  ( X 
\  ( K `  ( X  \  ( K `  B )
) ) )  C_  X
165155, 164eqsstri 3346 . . . . . . . . 9  |-  ( I `
 ( K `  B ) )  C_  X
166156difeq2i 3430 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  D
) ) )  =  ( X  \  (
I `  ( K `  B ) ) )
16713, 14, 26, 27, 152kur14lem4 24856 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  D
) ) )  =  ( K `  D
)
168166, 167eqtr3i 2434 . . . . . . . . . 10  |-  ( X 
\  ( I `  ( K `  B ) ) )  =  ( K `  D )
169168, 120eqeltri 2482 . . . . . . . . 9  |-  ( X 
\  ( I `  ( K `  B ) ) )  e.  T
17013, 14, 26, 27, 5, 44kur14lem6 24858 . . . . . . . . . 10  |-  ( K `
 ( I `  ( K `  B ) ) )  =  ( K `  B )
171170, 65eqeltri 2482 . . . . . . . . 9  |-  ( K `
 ( I `  ( K `  B ) ) )  e.  T
172165, 169, 171kur14lem1 24853 . . . . . . . 8  |-  ( N  =  ( I `  ( K `  B ) )  ->  ( N  C_  X  /\  { ( X  \  N ) ,  ( K `  N ) }  C_  T ) )
173151, 163, 1723jaoi 1247 . . . . . . 7  |-  ( ( N  =  ( I `
 C )  \/  N  =  ( K `
 D )  \/  N  =  ( I `
 ( K `  B ) ) )  ->  ( N  C_  X  /\  { ( X 
\  N ) ,  ( K `  N
) }  C_  T
) )
174139, 173syl 16 . . . . . 6  |-  ( N  e.  { ( I `
 C ) ,  ( K `  D
) ,  ( I `
 ( K `  B ) ) }  ->  ( N  C_  X  /\  { ( X 
\  N ) ,  ( K `  N
) }  C_  T
) )
175 elpri 3802 . . . . . . 7  |-  ( N  e.  { ( K `
 ( I `  C ) ) ,  ( I `  ( K `  ( I `  A ) ) ) }  ->  ( N  =  ( K `  ( I `  C
) )  \/  N  =  ( I `  ( K `  ( I `
 A ) ) ) ) )
17613, 14, 26, 27, 141kur14lem3 24855 . . . . . . . . 9  |-  ( K `
 ( I `  C ) )  C_  X
177126fveq2i 5698 . . . . . . . . . . . 12  |-  ( K `
 ( I `  C ) )  =  ( K `  ( X  \  ( K `  ( I `  A
) ) ) )
178177difeq2i 3430 . . . . . . . . . . 11  |-  ( X 
\  ( K `  ( I `  C
) ) )  =  ( X  \  ( K `  ( X  \  ( K `  (
I `  A )
) ) ) )
17913, 14, 26, 27, 122kur14lem2 24854 . . . . . . . . . . 11  |-  ( I `
 ( K `  ( I `  A
) ) )  =  ( X  \  ( K `  ( X  \  ( K `  (
I `  A )
) ) ) )
180178, 179eqtr4i 2435 . . . . . . . . . 10  |-  ( X 
\  ( K `  ( I `  C
) ) )  =  ( I `  ( K `  ( I `  A ) ) )
181 fvex 5709 . . . . . . . . . . . 12  |-  ( I `
 ( K `  ( I `  A
) ) )  e. 
_V
182181prid2 3881 . . . . . . . . . . 11  |-  ( I `
 ( K `  ( I `  A
) ) )  e. 
{ ( K `  ( I `  C
) ) ,  ( I `  ( K `
 ( I `  A ) ) ) }
183147, 182sselii 3313 . . . . . . . . . 10  |-  ( I `
 ( K `  ( I `  A
) ) )  e.  T
184180, 183eqeltri 2482 . . . . . . . . 9  |-  ( X 
\  ( K `  ( I `  C
) ) )  e.  T
18513, 14, 26, 27, 141kur14lem5 24857 . . . . . . . . . 10  |-  ( K `
 ( K `  ( I `  C
) ) )  =  ( K `  (
I `  C )
)
186185, 150eqeltri 2482 . . . . . . . . 9  |-  ( K `
 ( K `  ( I `  C
) ) )  e.  T
187176, 184, 186kur14lem1 24853 . . . . . . . 8  |-  ( N  =  ( K `  ( I `  C
) )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
188 difss 3442 . . . . . . . . . 10  |-  ( X 
\  ( K `  ( X  \  ( K `  ( I `  A ) ) ) ) )  C_  X
189179, 188eqsstri 3346 . . . . . . . . 9  |-  ( I `
 ( K `  ( I `  A
) ) )  C_  X
190180difeq2i 3430 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  (
I `  C )
) ) )  =  ( X  \  (
I `  ( K `  ( I `  A
) ) ) )
19113, 14, 26, 27, 176kur14lem4 24856 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  (
I `  C )
) ) )  =  ( K `  (
I `  C )
)
192190, 191eqtr3i 2434 . . . . . . . . . 10  |-  ( X 
\  ( I `  ( K `  ( I `
 A ) ) ) )  =  ( K `  ( I `
 C ) )
193192, 150eqeltri 2482 . . . . . . . . 9  |-  ( X 
\  ( I `  ( K `  ( I `
 A ) ) ) )  e.  T
19413, 14, 26, 27, 18, 68kur14lem6 24858 . . . . . . . . . 10  |-  ( K `
 ( I `  ( K `  ( I `
 A ) ) ) )  =  ( K `  ( I `
 A ) )
195194, 87eqeltri 2482 . . . . . . . . 9  |-  ( K `
 ( I `  ( K `  ( I `
 A ) ) ) )  e.  T
196189, 193, 195kur14lem1 24853 . . . . . . . 8  |-  ( N  =  ( I `  ( K `  ( I `
 A ) ) )  ->  ( N  C_  X  /\  { ( X  \  N ) ,  ( K `  N ) }  C_  T ) )
197187, 196jaoi 369 . . . . . . 7  |-  ( ( N  =  ( K `
 ( I `  C ) )  \/  N  =  ( I `
 ( K `  ( I `  A
) ) ) )  ->  ( N  C_  X  /\  { ( X 
\  N ) ,  ( K `  N
) }  C_  T
) )
198175, 197syl 16 . . . . . 6  |-  ( N  e.  { ( K `
 ( I `  C ) ) ,  ( I `  ( K `  ( I `  A ) ) ) }  ->  ( N  C_  X  /\  { ( X  \  N ) ,  ( K `  N ) }  C_  T ) )
199174, 198jaoi 369 . . . . 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 188 . . . 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 369 . . 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 188 . 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 2504 1  |-  ( N  e.  T  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 358    /\ wa 359    \/ w3o 935    = wceq 1649    e. wcel 1721    \ cdif 3285    u. cun 3286    C_ wss 3288   {cpr 3783   {ctp 3784   U.cuni 3983   ` cfv 5421   Topctop 16921   intcnt 17044   clsccl 17045
This theorem is referenced by:  kur14lem9  24861
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-rep 4288  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-reu 2681  df-rab 2683  df-v 2926  df-sbc 3130  df-csb 3220  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-tp 3790  df-op 3791  df-uni 3984  df-int 4019  df-iun 4063  df-iin 4064  df-br 4181  df-opab 4235  df-mpt 4236  df-id 4466  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-top 16926  df-cld 17046  df-ntr 17047  df-cls 17048
  Copyright terms: Public domain W3C validator