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

Theorem kur14lem7 23743
Description: Lemma for kur14 23747: 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 23742. (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 3316 . . 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 3316 . . . . 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 3316 . . . . . . 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 3677 . . . . . . . . 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 3338 . . . . . . . . . . . . 13  |-  { A ,  ( X  \  A ) ,  ( K `  A ) }  C_  ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C ,  ( I `
 A ) } )
7 ssun1 3338 . . . . . . . . . . . . . 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 3338 . . . . . . . . . . . . . . 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 3211 . . . . . . . . . . . . . 14  |-  ( ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C , 
( I `  A
) } )  u. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) } ) 
C_  T
117, 10sstri 3188 . . . . . . . . . . . . 13  |-  ( { A ,  ( X 
\  A ) ,  ( K `  A
) }  u.  { B ,  C , 
( I `  A
) } )  C_  T
126, 11sstri 3188 . . . . . . . . . . . 12  |-  { A ,  ( X  \  A ) ,  ( K `  A ) }  C_  T
13 kur14lem.j . . . . . . . . . . . . . . . 16  |-  J  e. 
Top
14 kur14lem.x . . . . . . . . . . . . . . . . 17  |-  X  = 
U. J
1514topopn 16652 . . . . . . . . . . . . . . . 16  |-  ( J  e.  Top  ->  X  e.  J )
1613, 15ax-mp 8 . . . . . . . . . . . . . . 15  |-  X  e.  J
1716elexi 2797 . . . . . . . . . . . . . 14  |-  X  e. 
_V
18 difss 3303 . . . . . . . . . . . . . 14  |-  ( X 
\  A )  C_  X
1917, 18ssexi 4159 . . . . . . . . . . . . 13  |-  ( X 
\  A )  e. 
_V
2019tpid2 3740 . . . . . . . . . . . 12  |-  ( X 
\  A )  e. 
{ A ,  ( X  \  A ) ,  ( K `  A ) }
2112, 20sselii 3177 . . . . . . . . . . 11  |-  ( X 
\  A )  e.  T
22 fvex 5539 . . . . . . . . . . . . 13  |-  ( K `
 A )  e. 
_V
2322tpid3 3742 . . . . . . . . . . . 12  |-  ( K `
 A )  e. 
{ A ,  ( X  \  A ) ,  ( K `  A ) }
2412, 23sselii 3177 . . . . . . . . . . 11  |-  ( K `
 A )  e.  T
255, 21, 24kur14lem1 23737 . . . . . . . . . 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 23740 . . . . . . . . . . . 12  |-  ( X 
\  ( X  \  A ) )  =  A
2917, 5ssexi 4159 . . . . . . . . . . . . . 14  |-  A  e. 
_V
3029tpid1 3739 . . . . . . . . . . . . 13  |-  A  e. 
{ A ,  ( X  \  A ) ,  ( K `  A ) }
3112, 30sselii 3177 . . . . . . . . . . . 12  |-  A  e.  T
3228, 31eqeltri 2353 . . . . . . . . . . 11  |-  ( X 
\  ( X  \  A ) )  e.  T
33 kur14lem.c . . . . . . . . . . . 12  |-  C  =  ( K `  ( X  \  A ) )
34 ssun2 3339 . . . . . . . . . . . . . 14  |-  { B ,  C ,  ( I `
 A ) } 
C_  ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C ,  ( I `
 A ) } )
3534, 11sstri 3188 . . . . . . . . . . . . 13  |-  { B ,  C ,  ( I `
 A ) } 
C_  T
3613, 14, 26, 27, 18kur14lem3 23739 . . . . . . . . . . . . . . . 16  |-  ( K `
 ( X  \  A ) )  C_  X
3733, 36eqsstri 3208 . . . . . . . . . . . . . . 15  |-  C  C_  X
3817, 37ssexi 4159 . . . . . . . . . . . . . 14  |-  C  e. 
_V
3938tpid2 3740 . . . . . . . . . . . . 13  |-  C  e. 
{ B ,  C ,  ( I `  A ) }
4035, 39sselii 3177 . . . . . . . . . . . 12  |-  C  e.  T
4133, 40eqeltrri 2354 . . . . . . . . . . 11  |-  ( K `
 ( X  \  A ) )  e.  T
4218, 32, 41kur14lem1 23737 . . . . . . . . . 10  |-  ( N  =  ( X  \  A )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
4313, 14, 26, 27, 5kur14lem3 23739 . . . . . . . . . . 11  |-  ( K `
 A )  C_  X
44 kur14lem.b . . . . . . . . . . . 12  |-  B  =  ( X  \  ( K `  A )
)
45 difss 3303 . . . . . . . . . . . . . . . 16  |-  ( X 
\  ( K `  A ) )  C_  X
4644, 45eqsstri 3208 . . . . . . . . . . . . . . 15  |-  B  C_  X
4717, 46ssexi 4159 . . . . . . . . . . . . . 14  |-  B  e. 
_V
4847tpid1 3739 . . . . . . . . . . . . 13  |-  B  e. 
{ B ,  C ,  ( I `  A ) }
4935, 48sselii 3177 . . . . . . . . . . . 12  |-  B  e.  T
5044, 49eqeltrri 2354 . . . . . . . . . . 11  |-  ( X 
\  ( K `  A ) )  e.  T
5113, 14, 26, 27, 5kur14lem5 23741 . . . . . . . . . . . 12  |-  ( K `
 ( K `  A ) )  =  ( K `  A
)
5251, 24eqeltri 2353 . . . . . . . . . . 11  |-  ( K `
 ( K `  A ) )  e.  T
5343, 50, 52kur14lem1 23737 . . . . . . . . . 10  |-  ( N  =  ( K `  A )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
5425, 42, 533jaoi 1245 . . . . . . . . 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 3677 . . . . . . . . 9  |-  ( N  e.  { B ,  C ,  ( I `  A ) }  ->  ( N  =  B  \/  N  =  C  \/  N  =  ( I `  A ) ) )
5744difeq2i 3291 . . . . . . . . . . . . 13  |-  ( X 
\  B )  =  ( X  \  ( X  \  ( K `  A ) ) )
5813, 14, 26, 27, 43kur14lem4 23740 . . . . . . . . . . . . 13  |-  ( X 
\  ( X  \ 
( K `  A
) ) )  =  ( K `  A
)
5957, 58eqtri 2303 . . . . . . . . . . . 12  |-  ( X 
\  B )  =  ( K `  A
)
6059, 24eqeltri 2353 . . . . . . . . . . 11  |-  ( X 
\  B )  e.  T
61 ssun2 3339 . . . . . . . . . . . . 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 3188 . . . . . . . . . . . 12  |-  { ( K `  B ) ,  D ,  ( K `  ( I `
 A ) ) }  C_  T
63 fvex 5539 . . . . . . . . . . . . 13  |-  ( K `
 B )  e. 
_V
6463tpid1 3739 . . . . . . . . . . . 12  |-  ( K `
 B )  e. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) }
6562, 64sselii 3177 . . . . . . . . . . 11  |-  ( K `
 B )  e.  T
6646, 60, 65kur14lem1 23737 . . . . . . . . . 10  |-  ( N  =  B  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
6733difeq2i 3291 . . . . . . . . . . . . 13  |-  ( X 
\  C )  =  ( X  \  ( K `  ( X  \  A ) ) )
6813, 14, 26, 27, 5kur14lem2 23738 . . . . . . . . . . . . 13  |-  ( I `
 A )  =  ( X  \  ( K `  ( X  \  A ) ) )
6967, 68eqtr4i 2306 . . . . . . . . . . . 12  |-  ( X 
\  C )  =  ( I `  A
)
70 fvex 5539 . . . . . . . . . . . . . 14  |-  ( I `
 A )  e. 
_V
7170tpid3 3742 . . . . . . . . . . . . 13  |-  ( I `
 A )  e. 
{ B ,  C ,  ( I `  A ) }
7235, 71sselii 3177 . . . . . . . . . . . 12  |-  ( I `
 A )  e.  T
7369, 72eqeltri 2353 . . . . . . . . . . 11  |-  ( X 
\  C )  e.  T
7413, 14, 26, 27, 18kur14lem5 23741 . . . . . . . . . . . . 13  |-  ( K `
 ( K `  ( X  \  A ) ) )  =  ( K `  ( X 
\  A ) )
7533fveq2i 5528 . . . . . . . . . . . . 13  |-  ( K `
 C )  =  ( K `  ( K `  ( X  \  A ) ) )
7674, 75, 333eqtr4i 2313 . . . . . . . . . . . 12  |-  ( K `
 C )  =  C
7776, 40eqeltri 2353 . . . . . . . . . . 11  |-  ( K `
 C )  e.  T
7837, 73, 77kur14lem1 23737 . . . . . . . . . 10  |-  ( N  =  C  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
79 difss 3303 . . . . . . . . . . . 12  |-  ( X 
\  ( K `  ( X  \  A ) ) )  C_  X
8068, 79eqsstri 3208 . . . . . . . . . . 11  |-  ( I `
 A )  C_  X
8169difeq2i 3291 . . . . . . . . . . . . 13  |-  ( X 
\  ( X  \  C ) )  =  ( X  \  (
I `  A )
)
8213, 14, 26, 27, 37kur14lem4 23740 . . . . . . . . . . . . 13  |-  ( X 
\  ( X  \  C ) )  =  C
8381, 82eqtr3i 2305 . . . . . . . . . . . 12  |-  ( X 
\  ( I `  A ) )  =  C
8483, 40eqeltri 2353 . . . . . . . . . . 11  |-  ( X 
\  ( I `  A ) )  e.  T
85 fvex 5539 . . . . . . . . . . . . 13  |-  ( K `
 ( I `  A ) )  e. 
_V
8685tpid3 3742 . . . . . . . . . . . 12  |-  ( K `
 ( I `  A ) )  e. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) }
8762, 86sselii 3177 . . . . . . . . . . 11  |-  ( K `
 ( I `  A ) )  e.  T
8880, 84, 87kur14lem1 23737 . . . . . . . . . 10  |-  ( N  =  ( I `  A )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
8966, 78, 883jaoi 1245 . . . . . . . . 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 3677 . . . . . . 7  |-  ( N  e.  { ( K `
 B ) ,  D ,  ( K `
 ( I `  A ) ) }  ->  ( N  =  ( K `  B
)  \/  N  =  D  \/  N  =  ( K `  (
I `  A )
) ) )
9413, 14, 26, 27, 46kur14lem3 23739 . . . . . . . . 9  |-  ( K `
 B )  C_  X
9513, 14, 26, 27, 43kur14lem2 23738 . . . . . . . . . . 11  |-  ( I `
 ( K `  A ) )  =  ( X  \  ( K `  ( X  \  ( K `  A
) ) ) )
96 kur14lem.d . . . . . . . . . . 11  |-  D  =  ( I `  ( K `  A )
)
9744fveq2i 5528 . . . . . . . . . . . 12  |-  ( K `
 B )  =  ( K `  ( X  \  ( K `  A ) ) )
9897difeq2i 3291 . . . . . . . . . . 11  |-  ( X 
\  ( K `  B ) )  =  ( X  \  ( K `  ( X  \  ( K `  A
) ) ) )
9995, 96, 983eqtr4i 2313 . . . . . . . . . 10  |-  D  =  ( X  \  ( K `  B )
)
10096, 95eqtri 2303 . . . . . . . . . . . . . 14  |-  D  =  ( X  \  ( K `  ( X  \  ( K `  A
) ) ) )
101 difss 3303 . . . . . . . . . . . . . 14  |-  ( X 
\  ( K `  ( X  \  ( K `  A )
) ) )  C_  X
102100, 101eqsstri 3208 . . . . . . . . . . . . 13  |-  D  C_  X
10317, 102ssexi 4159 . . . . . . . . . . . 12  |-  D  e. 
_V
104103tpid2 3740 . . . . . . . . . . 11  |-  D  e. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) }
10562, 104sselii 3177 . . . . . . . . . 10  |-  D  e.  T
10699, 105eqeltrri 2354 . . . . . . . . 9  |-  ( X 
\  ( K `  B ) )  e.  T
10713, 14, 26, 27, 46kur14lem5 23741 . . . . . . . . . 10  |-  ( K `
 ( K `  B ) )  =  ( K `  B
)
108107, 65eqeltri 2353 . . . . . . . . 9  |-  ( K `
 ( K `  B ) )  e.  T
10994, 106, 108kur14lem1 23737 . . . . . . . 8  |-  ( N  =  ( K `  B )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
11099difeq2i 3291 . . . . . . . . . . 11  |-  ( X 
\  D )  =  ( X  \  ( X  \  ( K `  B ) ) )
11113, 14, 26, 27, 94kur14lem4 23740 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  B
) ) )  =  ( K `  B
)
112110, 111eqtri 2303 . . . . . . . . . 10  |-  ( X 
\  D )  =  ( K `  B
)
113112, 65eqeltri 2353 . . . . . . . . 9  |-  ( X 
\  D )  e.  T
114 ssun1 3338 . . . . . . . . . . 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 3339 . . . . . . . . . . . 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 3211 . . . . . . . . . . 11  |-  ( { ( I `  C
) ,  ( K `
 D ) ,  ( I `  ( K `  B )
) }  u.  {
( K `  (
I `  C )
) ,  ( I `
 ( K `  ( I `  A
) ) ) } )  C_  T
117114, 116sstri 3188 . . . . . . . . . 10  |-  { ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `
 B ) ) }  C_  T
118 fvex 5539 . . . . . . . . . . 11  |-  ( K `
 D )  e. 
_V
119118tpid2 3740 . . . . . . . . . 10  |-  ( K `
 D )  e. 
{ ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `  B ) ) }
120117, 119sselii 3177 . . . . . . . . 9  |-  ( K `
 D )  e.  T
121102, 113, 120kur14lem1 23737 . . . . . . . 8  |-  ( N  =  D  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
12213, 14, 26, 27, 80kur14lem3 23739 . . . . . . . . 9  |-  ( K `
 ( I `  A ) )  C_  X
12313, 14, 26, 27, 37kur14lem2 23738 . . . . . . . . . . 11  |-  ( I `
 C )  =  ( X  \  ( K `  ( X  \  C ) ) )
12469fveq2i 5528 . . . . . . . . . . . 12  |-  ( K `
 ( X  \  C ) )  =  ( K `  (
I `  A )
)
125124difeq2i 3291 . . . . . . . . . . 11  |-  ( X 
\  ( K `  ( X  \  C ) ) )  =  ( X  \  ( K `
 ( I `  A ) ) )
126123, 125eqtri 2303 . . . . . . . . . 10  |-  ( I `
 C )  =  ( X  \  ( K `  ( I `  A ) ) )
127 fvex 5539 . . . . . . . . . . . 12  |-  ( I `
 C )  e. 
_V
128127tpid1 3739 . . . . . . . . . . 11  |-  ( I `
 C )  e. 
{ ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `  B ) ) }
129117, 128sselii 3177 . . . . . . . . . 10  |-  ( I `
 C )  e.  T
130126, 129eqeltrri 2354 . . . . . . . . 9  |-  ( X 
\  ( K `  ( I `  A
) ) )  e.  T
13113, 14, 26, 27, 80kur14lem5 23741 . . . . . . . . . 10  |-  ( K `
 ( K `  ( I `  A
) ) )  =  ( K `  (
I `  A )
)
132131, 87eqeltri 2353 . . . . . . . . 9  |-  ( K `
 ( K `  ( I `  A
) ) )  e.  T
133122, 130, 132kur14lem1 23737 . . . . . . . 8  |-  ( N  =  ( K `  ( I `  A
) )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
134109, 121, 1333jaoi 1245 . . . . . . 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 3316 . . . . 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 3677 . . . . . . 7  |-  ( N  e.  { ( I `
 C ) ,  ( K `  D
) ,  ( I `
 ( K `  B ) ) }  ->  ( N  =  ( I `  C
)  \/  N  =  ( K `  D
)  \/  N  =  ( I `  ( K `  B )
) ) )
140 difss 3303 . . . . . . . . . 10  |-  ( X 
\  ( K `  ( X  \  C ) ) )  C_  X
141123, 140eqsstri 3208 . . . . . . . . 9  |-  ( I `
 C )  C_  X
142126difeq2i 3291 . . . . . . . . . . 11  |-  ( X 
\  ( I `  C ) )  =  ( X  \  ( X  \  ( K `  ( I `  A
) ) ) )
14313, 14, 26, 27, 122kur14lem4 23740 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  (
I `  A )
) ) )  =  ( K `  (
I `  A )
)
144142, 143eqtri 2303 . . . . . . . . . 10  |-  ( X 
\  ( I `  C ) )  =  ( K `  (
I `  A )
)
145144, 87eqeltri 2353 . . . . . . . . 9  |-  ( X 
\  ( I `  C ) )  e.  T
146 ssun2 3339 . . . . . . . . . . 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 3188 . . . . . . . . . 10  |-  { ( K `  ( I `
 C ) ) ,  ( I `  ( K `  ( I `
 A ) ) ) }  C_  T
148 fvex 5539 . . . . . . . . . . 11  |-  ( K `
 ( I `  C ) )  e. 
_V
149148prid1 3734 . . . . . . . . . 10  |-  ( K `
 ( I `  C ) )  e. 
{ ( K `  ( I `  C
) ) ,  ( I `  ( K `
 ( I `  A ) ) ) }
150147, 149sselii 3177 . . . . . . . . 9  |-  ( K `
 ( I `  C ) )  e.  T
151141, 145, 150kur14lem1 23737 . . . . . . . 8  |-  ( N  =  ( I `  C )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
15213, 14, 26, 27, 102kur14lem3 23739 . . . . . . . . 9  |-  ( K `
 D )  C_  X
15399fveq2i 5528 . . . . . . . . . . . 12  |-  ( K `
 D )  =  ( K `  ( X  \  ( K `  B ) ) )
154153difeq2i 3291 . . . . . . . . . . 11  |-  ( X 
\  ( K `  D ) )  =  ( X  \  ( K `  ( X  \  ( K `  B
) ) ) )
15513, 14, 26, 27, 94kur14lem2 23738 . . . . . . . . . . 11  |-  ( I `
 ( K `  B ) )  =  ( X  \  ( K `  ( X  \  ( K `  B
) ) ) )
156154, 155eqtr4i 2306 . . . . . . . . . 10  |-  ( X 
\  ( K `  D ) )  =  ( I `  ( K `  B )
)
157 fvex 5539 . . . . . . . . . . . 12  |-  ( I `
 ( K `  B ) )  e. 
_V
158157tpid3 3742 . . . . . . . . . . 11  |-  ( I `
 ( K `  B ) )  e. 
{ ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `  B ) ) }
159117, 158sselii 3177 . . . . . . . . . 10  |-  ( I `
 ( K `  B ) )  e.  T
160156, 159eqeltri 2353 . . . . . . . . 9  |-  ( X 
\  ( K `  D ) )  e.  T
16113, 14, 26, 27, 102kur14lem5 23741 . . . . . . . . . 10  |-  ( K `
 ( K `  D ) )  =  ( K `  D
)
162161, 120eqeltri 2353 . . . . . . . . 9  |-  ( K `
 ( K `  D ) )  e.  T
163152, 160, 162kur14lem1 23737 . . . . . . . 8  |-  ( N  =  ( K `  D )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
164 difss 3303 . . . . . . . . . 10  |-  ( X 
\  ( K `  ( X  \  ( K `  B )
) ) )  C_  X
165155, 164eqsstri 3208 . . . . . . . . 9  |-  ( I `
 ( K `  B ) )  C_  X
166156difeq2i 3291 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  D
) ) )  =  ( X  \  (
I `  ( K `  B ) ) )
16713, 14, 26, 27, 152kur14lem4 23740 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  D
) ) )  =  ( K `  D
)
168166, 167eqtr3i 2305 . . . . . . . . . 10  |-  ( X 
\  ( I `  ( K `  B ) ) )  =  ( K `  D )
169168, 120eqeltri 2353 . . . . . . . . 9  |-  ( X 
\  ( I `  ( K `  B ) ) )  e.  T
17013, 14, 26, 27, 5, 44kur14lem6 23742 . . . . . . . . . 10  |-  ( K `
 ( I `  ( K `  B ) ) )  =  ( K `  B )
171170, 65eqeltri 2353 . . . . . . . . 9  |-  ( K `
 ( I `  ( K `  B ) ) )  e.  T
172165, 169, 171kur14lem1 23737 . . . . . . . 8  |-  ( N  =  ( I `  ( K `  B ) )  ->  ( N  C_  X  /\  { ( X  \  N ) ,  ( K `  N ) }  C_  T ) )
173151, 163, 1723jaoi 1245 . . . . . . 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 3660 . . . . . . 7  |-  ( N  e.  { ( K `
 ( I `  C ) ) ,  ( I `  ( K `  ( I `  A ) ) ) }  ->  ( N  =  ( K `  ( I `  C
) )  \/  N  =  ( I `  ( K `  ( I `
 A ) ) ) ) )
17613, 14, 26, 27, 141kur14lem3 23739 . . . . . . . . 9  |-  ( K `
 ( I `  C ) )  C_  X
177126fveq2i 5528 . . . . . . . . . . . 12  |-  ( K `
 ( I `  C ) )  =  ( K `  ( X  \  ( K `  ( I `  A
) ) ) )
178177difeq2i 3291 . . . . . . . . . . 11  |-  ( X 
\  ( K `  ( I `  C
) ) )  =  ( X  \  ( K `  ( X  \  ( K `  (
I `  A )
) ) ) )
17913, 14, 26, 27, 122kur14lem2 23738 . . . . . . . . . . 11  |-  ( I `
 ( K `  ( I `  A
) ) )  =  ( X  \  ( K `  ( X  \  ( K `  (
I `  A )
) ) ) )
180178, 179eqtr4i 2306 . . . . . . . . . 10  |-  ( X 
\  ( K `  ( I `  C
) ) )  =  ( I `  ( K `  ( I `  A ) ) )
181 fvex 5539 . . . . . . . . . . . 12  |-  ( I `
 ( K `  ( I `  A
) ) )  e. 
_V
182181prid2 3735 . . . . . . . . . . 11  |-  ( I `
 ( K `  ( I `  A
) ) )  e. 
{ ( K `  ( I `  C
) ) ,  ( I `  ( K `
 ( I `  A ) ) ) }
183147, 182sselii 3177 . . . . . . . . . 10  |-  ( I `
 ( K `  ( I `  A
) ) )  e.  T
184180, 183eqeltri 2353 . . . . . . . . 9  |-  ( X 
\  ( K `  ( I `  C
) ) )  e.  T
18513, 14, 26, 27, 141kur14lem5 23741 . . . . . . . . . 10  |-  ( K `
 ( K `  ( I `  C
) ) )  =  ( K `  (
I `  C )
)
186185, 150eqeltri 2353 . . . . . . . . 9  |-  ( K `
 ( K `  ( I `  C
) ) )  e.  T
187176, 184, 186kur14lem1 23737 . . . . . . . 8  |-  ( N  =  ( K `  ( I `  C
) )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
188 difss 3303 . . . . . . . . . 10  |-  ( X 
\  ( K `  ( X  \  ( K `  ( I `  A ) ) ) ) )  C_  X
189179, 188eqsstri 3208 . . . . . . . . 9  |-  ( I `
 ( K `  ( I `  A
) ) )  C_  X
190180difeq2i 3291 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  (
I `  C )
) ) )  =  ( X  \  (
I `  ( K `  ( I `  A
) ) ) )
19113, 14, 26, 27, 176kur14lem4 23740 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  (
I `  C )
) ) )  =  ( K `  (
I `  C )
)
192190, 191eqtr3i 2305 . . . . . . . . . 10  |-  ( X 
\  ( I `  ( K `  ( I `
 A ) ) ) )  =  ( K `  ( I `
 C ) )
193192, 150eqeltri 2353 . . . . . . . . 9  |-  ( X 
\  ( I `  ( K `  ( I `
 A ) ) ) )  e.  T
19413, 14, 26, 27, 18, 68kur14lem6 23742 . . . . . . . . . 10  |-  ( K `
 ( I `  ( K `  ( I `
 A ) ) ) )  =  ( K `  ( I `
 A ) )
195194, 87eqeltri 2353 . . . . . . . . 9  |-  ( K `
 ( I `  ( K `  ( I `
 A ) ) ) )  e.  T
196189, 193, 195kur14lem1 23737 . . . . . . . 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 2375 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 933    = wceq 1623    e. wcel 1684    \ cdif 3149    u. cun 3150    C_ wss 3152   {cpr 3641   {ctp 3642   U.cuni 3827   ` cfv 5255   Topctop 16631   intcnt 16754   clsccl 16755
This theorem is referenced by:  kur14lem9  23745
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-int 3863  df-iun 3907  df-iin 3908  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-top 16636  df-cld 16756  df-ntr 16757  df-cls 16758
  Copyright terms: Public domain W3C validator