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

Theorem kur14lem7 27236
Description: Lemma for kur14 27240: 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 27235. (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 3597 . . 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 3597 . . . . 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 3597 . . . . . . 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 4020 . . . . . . . . 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 3619 . . . . . . . . . . . . 13  |-  { A ,  ( X  \  A ) ,  ( K `  A ) }  C_  ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C ,  ( I `
 A ) } )
7 ssun1 3619 . . . . . . . . . . . . . 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 3619 . . . . . . . . . . . . . . 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 3489 . . . . . . . . . . . . . 14  |-  ( ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C , 
( I `  A
) } )  u. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) } ) 
C_  T
117, 10sstri 3465 . . . . . . . . . . . . 13  |-  ( { A ,  ( X 
\  A ) ,  ( K `  A
) }  u.  { B ,  C , 
( I `  A
) } )  C_  T
126, 11sstri 3465 . . . . . . . . . . . 12  |-  { A ,  ( X  \  A ) ,  ( K `  A ) }  C_  T
13 kur14lem.j . . . . . . . . . . . . . . . 16  |-  J  e. 
Top
14 kur14lem.x . . . . . . . . . . . . . . . . 17  |-  X  = 
U. J
1514topopn 18637 . . . . . . . . . . . . . . . 16  |-  ( J  e.  Top  ->  X  e.  J )
1613, 15ax-mp 5 . . . . . . . . . . . . . . 15  |-  X  e.  J
1716elexi 3080 . . . . . . . . . . . . . 14  |-  X  e. 
_V
18 difss 3583 . . . . . . . . . . . . . 14  |-  ( X 
\  A )  C_  X
1917, 18ssexi 4537 . . . . . . . . . . . . 13  |-  ( X 
\  A )  e. 
_V
2019tpid2 4089 . . . . . . . . . . . 12  |-  ( X 
\  A )  e. 
{ A ,  ( X  \  A ) ,  ( K `  A ) }
2112, 20sselii 3453 . . . . . . . . . . 11  |-  ( X 
\  A )  e.  T
22 fvex 5801 . . . . . . . . . . . . 13  |-  ( K `
 A )  e. 
_V
2322tpid3 4091 . . . . . . . . . . . 12  |-  ( K `
 A )  e. 
{ A ,  ( X  \  A ) ,  ( K `  A ) }
2412, 23sselii 3453 . . . . . . . . . . 11  |-  ( K `
 A )  e.  T
255, 21, 24kur14lem1 27230 . . . . . . . . . 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 27233 . . . . . . . . . . . 12  |-  ( X 
\  ( X  \  A ) )  =  A
2917, 5ssexi 4537 . . . . . . . . . . . . . 14  |-  A  e. 
_V
3029tpid1 4088 . . . . . . . . . . . . 13  |-  A  e. 
{ A ,  ( X  \  A ) ,  ( K `  A ) }
3112, 30sselii 3453 . . . . . . . . . . . 12  |-  A  e.  T
3228, 31eqeltri 2535 . . . . . . . . . . 11  |-  ( X 
\  ( X  \  A ) )  e.  T
33 kur14lem.c . . . . . . . . . . . 12  |-  C  =  ( K `  ( X  \  A ) )
34 ssun2 3620 . . . . . . . . . . . . . 14  |-  { B ,  C ,  ( I `
 A ) } 
C_  ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C ,  ( I `
 A ) } )
3534, 11sstri 3465 . . . . . . . . . . . . 13  |-  { B ,  C ,  ( I `
 A ) } 
C_  T
3613, 14, 26, 27, 18kur14lem3 27232 . . . . . . . . . . . . . . . 16  |-  ( K `
 ( X  \  A ) )  C_  X
3733, 36eqsstri 3486 . . . . . . . . . . . . . . 15  |-  C  C_  X
3817, 37ssexi 4537 . . . . . . . . . . . . . 14  |-  C  e. 
_V
3938tpid2 4089 . . . . . . . . . . . . 13  |-  C  e. 
{ B ,  C ,  ( I `  A ) }
4035, 39sselii 3453 . . . . . . . . . . . 12  |-  C  e.  T
4133, 40eqeltrri 2536 . . . . . . . . . . 11  |-  ( K `
 ( X  \  A ) )  e.  T
4218, 32, 41kur14lem1 27230 . . . . . . . . . 10  |-  ( N  =  ( X  \  A )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
4313, 14, 26, 27, 5kur14lem3 27232 . . . . . . . . . . 11  |-  ( K `
 A )  C_  X
44 kur14lem.b . . . . . . . . . . . 12  |-  B  =  ( X  \  ( K `  A )
)
45 difss 3583 . . . . . . . . . . . . . . . 16  |-  ( X 
\  ( K `  A ) )  C_  X
4644, 45eqsstri 3486 . . . . . . . . . . . . . . 15  |-  B  C_  X
4717, 46ssexi 4537 . . . . . . . . . . . . . 14  |-  B  e. 
_V
4847tpid1 4088 . . . . . . . . . . . . 13  |-  B  e. 
{ B ,  C ,  ( I `  A ) }
4935, 48sselii 3453 . . . . . . . . . . . 12  |-  B  e.  T
5044, 49eqeltrri 2536 . . . . . . . . . . 11  |-  ( X 
\  ( K `  A ) )  e.  T
5113, 14, 26, 27, 5kur14lem5 27234 . . . . . . . . . . . 12  |-  ( K `
 ( K `  A ) )  =  ( K `  A
)
5251, 24eqeltri 2535 . . . . . . . . . . 11  |-  ( K `
 ( K `  A ) )  e.  T
5343, 50, 52kur14lem1 27230 . . . . . . . . . 10  |-  ( N  =  ( K `  A )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
5425, 42, 533jaoi 1282 . . . . . . . . 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 4020 . . . . . . . . 9  |-  ( N  e.  { B ,  C ,  ( I `  A ) }  ->  ( N  =  B  \/  N  =  C  \/  N  =  ( I `  A ) ) )
5744difeq2i 3571 . . . . . . . . . . . . 13  |-  ( X 
\  B )  =  ( X  \  ( X  \  ( K `  A ) ) )
5813, 14, 26, 27, 43kur14lem4 27233 . . . . . . . . . . . . 13  |-  ( X 
\  ( X  \ 
( K `  A
) ) )  =  ( K `  A
)
5957, 58eqtri 2480 . . . . . . . . . . . 12  |-  ( X 
\  B )  =  ( K `  A
)
6059, 24eqeltri 2535 . . . . . . . . . . 11  |-  ( X 
\  B )  e.  T
61 ssun2 3620 . . . . . . . . . . . . 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 3465 . . . . . . . . . . . 12  |-  { ( K `  B ) ,  D ,  ( K `  ( I `
 A ) ) }  C_  T
63 fvex 5801 . . . . . . . . . . . . 13  |-  ( K `
 B )  e. 
_V
6463tpid1 4088 . . . . . . . . . . . 12  |-  ( K `
 B )  e. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) }
6562, 64sselii 3453 . . . . . . . . . . 11  |-  ( K `
 B )  e.  T
6646, 60, 65kur14lem1 27230 . . . . . . . . . 10  |-  ( N  =  B  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
6733difeq2i 3571 . . . . . . . . . . . . 13  |-  ( X 
\  C )  =  ( X  \  ( K `  ( X  \  A ) ) )
6813, 14, 26, 27, 5kur14lem2 27231 . . . . . . . . . . . . 13  |-  ( I `
 A )  =  ( X  \  ( K `  ( X  \  A ) ) )
6967, 68eqtr4i 2483 . . . . . . . . . . . 12  |-  ( X 
\  C )  =  ( I `  A
)
70 fvex 5801 . . . . . . . . . . . . . 14  |-  ( I `
 A )  e. 
_V
7170tpid3 4091 . . . . . . . . . . . . 13  |-  ( I `
 A )  e. 
{ B ,  C ,  ( I `  A ) }
7235, 71sselii 3453 . . . . . . . . . . . 12  |-  ( I `
 A )  e.  T
7369, 72eqeltri 2535 . . . . . . . . . . 11  |-  ( X 
\  C )  e.  T
7413, 14, 26, 27, 18kur14lem5 27234 . . . . . . . . . . . . 13  |-  ( K `
 ( K `  ( X  \  A ) ) )  =  ( K `  ( X 
\  A ) )
7533fveq2i 5794 . . . . . . . . . . . . 13  |-  ( K `
 C )  =  ( K `  ( K `  ( X  \  A ) ) )
7674, 75, 333eqtr4i 2490 . . . . . . . . . . . 12  |-  ( K `
 C )  =  C
7776, 40eqeltri 2535 . . . . . . . . . . 11  |-  ( K `
 C )  e.  T
7837, 73, 77kur14lem1 27230 . . . . . . . . . 10  |-  ( N  =  C  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
79 difss 3583 . . . . . . . . . . . 12  |-  ( X 
\  ( K `  ( X  \  A ) ) )  C_  X
8068, 79eqsstri 3486 . . . . . . . . . . 11  |-  ( I `
 A )  C_  X
8169difeq2i 3571 . . . . . . . . . . . . 13  |-  ( X 
\  ( X  \  C ) )  =  ( X  \  (
I `  A )
)
8213, 14, 26, 27, 37kur14lem4 27233 . . . . . . . . . . . . 13  |-  ( X 
\  ( X  \  C ) )  =  C
8381, 82eqtr3i 2482 . . . . . . . . . . . 12  |-  ( X 
\  ( I `  A ) )  =  C
8483, 40eqeltri 2535 . . . . . . . . . . 11  |-  ( X 
\  ( I `  A ) )  e.  T
85 fvex 5801 . . . . . . . . . . . . 13  |-  ( K `
 ( I `  A ) )  e. 
_V
8685tpid3 4091 . . . . . . . . . . . 12  |-  ( K `
 ( I `  A ) )  e. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) }
8762, 86sselii 3453 . . . . . . . . . . 11  |-  ( K `
 ( I `  A ) )  e.  T
8880, 84, 87kur14lem1 27230 . . . . . . . . . 10  |-  ( N  =  ( I `  A )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
8966, 78, 883jaoi 1282 . . . . . . . . 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 379 . . . . . . 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 195 . . . . . 6  |-  ( N  e.  ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C ,  ( I `
 A ) } )  ->  ( N  C_  X  /\  { ( X  \  N ) ,  ( K `  N ) }  C_  T ) )
93 eltpi 4020 . . . . . . 7  |-  ( N  e.  { ( K `
 B ) ,  D ,  ( K `
 ( I `  A ) ) }  ->  ( N  =  ( K `  B
)  \/  N  =  D  \/  N  =  ( K `  (
I `  A )
) ) )
9413, 14, 26, 27, 46kur14lem3 27232 . . . . . . . . 9  |-  ( K `
 B )  C_  X
9513, 14, 26, 27, 43kur14lem2 27231 . . . . . . . . . . 11  |-  ( I `
 ( K `  A ) )  =  ( X  \  ( K `  ( X  \  ( K `  A
) ) ) )
96 kur14lem.d . . . . . . . . . . 11  |-  D  =  ( I `  ( K `  A )
)
9744fveq2i 5794 . . . . . . . . . . . 12  |-  ( K `
 B )  =  ( K `  ( X  \  ( K `  A ) ) )
9897difeq2i 3571 . . . . . . . . . . 11  |-  ( X 
\  ( K `  B ) )  =  ( X  \  ( K `  ( X  \  ( K `  A
) ) ) )
9995, 96, 983eqtr4i 2490 . . . . . . . . . 10  |-  D  =  ( X  \  ( K `  B )
)
10096, 95eqtri 2480 . . . . . . . . . . . . . 14  |-  D  =  ( X  \  ( K `  ( X  \  ( K `  A
) ) ) )
101 difss 3583 . . . . . . . . . . . . . 14  |-  ( X 
\  ( K `  ( X  \  ( K `  A )
) ) )  C_  X
102100, 101eqsstri 3486 . . . . . . . . . . . . 13  |-  D  C_  X
10317, 102ssexi 4537 . . . . . . . . . . . 12  |-  D  e. 
_V
104103tpid2 4089 . . . . . . . . . . 11  |-  D  e. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) }
10562, 104sselii 3453 . . . . . . . . . 10  |-  D  e.  T
10699, 105eqeltrri 2536 . . . . . . . . 9  |-  ( X 
\  ( K `  B ) )  e.  T
10713, 14, 26, 27, 46kur14lem5 27234 . . . . . . . . . 10  |-  ( K `
 ( K `  B ) )  =  ( K `  B
)
108107, 65eqeltri 2535 . . . . . . . . 9  |-  ( K `
 ( K `  B ) )  e.  T
10994, 106, 108kur14lem1 27230 . . . . . . . 8  |-  ( N  =  ( K `  B )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
11099difeq2i 3571 . . . . . . . . . . 11  |-  ( X 
\  D )  =  ( X  \  ( X  \  ( K `  B ) ) )
11113, 14, 26, 27, 94kur14lem4 27233 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  B
) ) )  =  ( K `  B
)
112110, 111eqtri 2480 . . . . . . . . . 10  |-  ( X 
\  D )  =  ( K `  B
)
113112, 65eqeltri 2535 . . . . . . . . 9  |-  ( X 
\  D )  e.  T
114 ssun1 3619 . . . . . . . . . . 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 3620 . . . . . . . . . . . 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 3489 . . . . . . . . . . 11  |-  ( { ( I `  C
) ,  ( K `
 D ) ,  ( I `  ( K `  B )
) }  u.  {
( K `  (
I `  C )
) ,  ( I `
 ( K `  ( I `  A
) ) ) } )  C_  T
117114, 116sstri 3465 . . . . . . . . . 10  |-  { ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `
 B ) ) }  C_  T
118 fvex 5801 . . . . . . . . . . 11  |-  ( K `
 D )  e. 
_V
119118tpid2 4089 . . . . . . . . . 10  |-  ( K `
 D )  e. 
{ ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `  B ) ) }
120117, 119sselii 3453 . . . . . . . . 9  |-  ( K `
 D )  e.  T
121102, 113, 120kur14lem1 27230 . . . . . . . 8  |-  ( N  =  D  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
12213, 14, 26, 27, 80kur14lem3 27232 . . . . . . . . 9  |-  ( K `
 ( I `  A ) )  C_  X
12313, 14, 26, 27, 37kur14lem2 27231 . . . . . . . . . . 11  |-  ( I `
 C )  =  ( X  \  ( K `  ( X  \  C ) ) )
12469fveq2i 5794 . . . . . . . . . . . 12  |-  ( K `
 ( X  \  C ) )  =  ( K `  (
I `  A )
)
125124difeq2i 3571 . . . . . . . . . . 11  |-  ( X 
\  ( K `  ( X  \  C ) ) )  =  ( X  \  ( K `
 ( I `  A ) ) )
126123, 125eqtri 2480 . . . . . . . . . 10  |-  ( I `
 C )  =  ( X  \  ( K `  ( I `  A ) ) )
127 fvex 5801 . . . . . . . . . . . 12  |-  ( I `
 C )  e. 
_V
128127tpid1 4088 . . . . . . . . . . 11  |-  ( I `
 C )  e. 
{ ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `  B ) ) }
129117, 128sselii 3453 . . . . . . . . . 10  |-  ( I `
 C )  e.  T
130126, 129eqeltrri 2536 . . . . . . . . 9  |-  ( X 
\  ( K `  ( I `  A
) ) )  e.  T
13113, 14, 26, 27, 80kur14lem5 27234 . . . . . . . . . 10  |-  ( K `
 ( K `  ( I `  A
) ) )  =  ( K `  (
I `  A )
)
132131, 87eqeltri 2535 . . . . . . . . 9  |-  ( K `
 ( K `  ( I `  A
) ) )  e.  T
133122, 130, 132kur14lem1 27230 . . . . . . . 8  |-  ( N  =  ( K `  ( I `  A
) )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
134109, 121, 1333jaoi 1282 . . . . . . 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 379 . . . . 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 195 . . . 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 3597 . . . . 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 4020 . . . . . . 7  |-  ( N  e.  { ( I `
 C ) ,  ( K `  D
) ,  ( I `
 ( K `  B ) ) }  ->  ( N  =  ( I `  C
)  \/  N  =  ( K `  D
)  \/  N  =  ( I `  ( K `  B )
) ) )
140 difss 3583 . . . . . . . . . 10  |-  ( X 
\  ( K `  ( X  \  C ) ) )  C_  X
141123, 140eqsstri 3486 . . . . . . . . 9  |-  ( I `
 C )  C_  X
142126difeq2i 3571 . . . . . . . . . . 11  |-  ( X 
\  ( I `  C ) )  =  ( X  \  ( X  \  ( K `  ( I `  A
) ) ) )
14313, 14, 26, 27, 122kur14lem4 27233 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  (
I `  A )
) ) )  =  ( K `  (
I `  A )
)
144142, 143eqtri 2480 . . . . . . . . . 10  |-  ( X 
\  ( I `  C ) )  =  ( K `  (
I `  A )
)
145144, 87eqeltri 2535 . . . . . . . . 9  |-  ( X 
\  ( I `  C ) )  e.  T
146 ssun2 3620 . . . . . . . . . . 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 3465 . . . . . . . . . 10  |-  { ( K `  ( I `
 C ) ) ,  ( I `  ( K `  ( I `
 A ) ) ) }  C_  T
148 fvex 5801 . . . . . . . . . . 11  |-  ( K `
 ( I `  C ) )  e. 
_V
149148prid1 4083 . . . . . . . . . 10  |-  ( K `
 ( I `  C ) )  e. 
{ ( K `  ( I `  C
) ) ,  ( I `  ( K `
 ( I `  A ) ) ) }
150147, 149sselii 3453 . . . . . . . . 9  |-  ( K `
 ( I `  C ) )  e.  T
151141, 145, 150kur14lem1 27230 . . . . . . . 8  |-  ( N  =  ( I `  C )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
15213, 14, 26, 27, 102kur14lem3 27232 . . . . . . . . 9  |-  ( K `
 D )  C_  X
15399fveq2i 5794 . . . . . . . . . . . 12  |-  ( K `
 D )  =  ( K `  ( X  \  ( K `  B ) ) )
154153difeq2i 3571 . . . . . . . . . . 11  |-  ( X 
\  ( K `  D ) )  =  ( X  \  ( K `  ( X  \  ( K `  B
) ) ) )
15513, 14, 26, 27, 94kur14lem2 27231 . . . . . . . . . . 11  |-  ( I `
 ( K `  B ) )  =  ( X  \  ( K `  ( X  \  ( K `  B
) ) ) )
156154, 155eqtr4i 2483 . . . . . . . . . 10  |-  ( X 
\  ( K `  D ) )  =  ( I `  ( K `  B )
)
157 fvex 5801 . . . . . . . . . . . 12  |-  ( I `
 ( K `  B ) )  e. 
_V
158157tpid3 4091 . . . . . . . . . . 11  |-  ( I `
 ( K `  B ) )  e. 
{ ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `  B ) ) }
159117, 158sselii 3453 . . . . . . . . . 10  |-  ( I `
 ( K `  B ) )  e.  T
160156, 159eqeltri 2535 . . . . . . . . 9  |-  ( X 
\  ( K `  D ) )  e.  T
16113, 14, 26, 27, 102kur14lem5 27234 . . . . . . . . . 10  |-  ( K `
 ( K `  D ) )  =  ( K `  D
)
162161, 120eqeltri 2535 . . . . . . . . 9  |-  ( K `
 ( K `  D ) )  e.  T
163152, 160, 162kur14lem1 27230 . . . . . . . 8  |-  ( N  =  ( K `  D )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
164 difss 3583 . . . . . . . . . 10  |-  ( X 
\  ( K `  ( X  \  ( K `  B )
) ) )  C_  X
165155, 164eqsstri 3486 . . . . . . . . 9  |-  ( I `
 ( K `  B ) )  C_  X
166156difeq2i 3571 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  D
) ) )  =  ( X  \  (
I `  ( K `  B ) ) )
16713, 14, 26, 27, 152kur14lem4 27233 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  D
) ) )  =  ( K `  D
)
168166, 167eqtr3i 2482 . . . . . . . . . 10  |-  ( X 
\  ( I `  ( K `  B ) ) )  =  ( K `  D )
169168, 120eqeltri 2535 . . . . . . . . 9  |-  ( X 
\  ( I `  ( K `  B ) ) )  e.  T
17013, 14, 26, 27, 5, 44kur14lem6 27235 . . . . . . . . . 10  |-  ( K `
 ( I `  ( K `  B ) ) )  =  ( K `  B )
171170, 65eqeltri 2535 . . . . . . . . 9  |-  ( K `
 ( I `  ( K `  B ) ) )  e.  T
172165, 169, 171kur14lem1 27230 . . . . . . . 8  |-  ( N  =  ( I `  ( K `  B ) )  ->  ( N  C_  X  /\  { ( X  \  N ) ,  ( K `  N ) }  C_  T ) )
173151, 163, 1723jaoi 1282 . . . . . . 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 3997 . . . . . . 7  |-  ( N  e.  { ( K `
 ( I `  C ) ) ,  ( I `  ( K `  ( I `  A ) ) ) }  ->  ( N  =  ( K `  ( I `  C
) )  \/  N  =  ( I `  ( K `  ( I `
 A ) ) ) ) )
17613, 14, 26, 27, 141kur14lem3 27232 . . . . . . . . 9  |-  ( K `
 ( I `  C ) )  C_  X
177126fveq2i 5794 . . . . . . . . . . . 12  |-  ( K `
 ( I `  C ) )  =  ( K `  ( X  \  ( K `  ( I `  A
) ) ) )
178177difeq2i 3571 . . . . . . . . . . 11  |-  ( X 
\  ( K `  ( I `  C
) ) )  =  ( X  \  ( K `  ( X  \  ( K `  (
I `  A )
) ) ) )
17913, 14, 26, 27, 122kur14lem2 27231 . . . . . . . . . . 11  |-  ( I `
 ( K `  ( I `  A
) ) )  =  ( X  \  ( K `  ( X  \  ( K `  (
I `  A )
) ) ) )
180178, 179eqtr4i 2483 . . . . . . . . . 10  |-  ( X 
\  ( K `  ( I `  C
) ) )  =  ( I `  ( K `  ( I `  A ) ) )
181 fvex 5801 . . . . . . . . . . . 12  |-  ( I `
 ( K `  ( I `  A
) ) )  e. 
_V
182181prid2 4084 . . . . . . . . . . 11  |-  ( I `
 ( K `  ( I `  A
) ) )  e. 
{ ( K `  ( I `  C
) ) ,  ( I `  ( K `
 ( I `  A ) ) ) }
183147, 182sselii 3453 . . . . . . . . . 10  |-  ( I `
 ( K `  ( I `  A
) ) )  e.  T
184180, 183eqeltri 2535 . . . . . . . . 9  |-  ( X 
\  ( K `  ( I `  C
) ) )  e.  T
18513, 14, 26, 27, 141kur14lem5 27234 . . . . . . . . . 10  |-  ( K `
 ( K `  ( I `  C
) ) )  =  ( K `  (
I `  C )
)
186185, 150eqeltri 2535 . . . . . . . . 9  |-  ( K `
 ( K `  ( I `  C
) ) )  e.  T
187176, 184, 186kur14lem1 27230 . . . . . . . 8  |-  ( N  =  ( K `  ( I `  C
) )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
188 difss 3583 . . . . . . . . . 10  |-  ( X 
\  ( K `  ( X  \  ( K `  ( I `  A ) ) ) ) )  C_  X
189179, 188eqsstri 3486 . . . . . . . . 9  |-  ( I `
 ( K `  ( I `  A
) ) )  C_  X
190180difeq2i 3571 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  (
I `  C )
) ) )  =  ( X  \  (
I `  ( K `  ( I `  A
) ) ) )
19113, 14, 26, 27, 176kur14lem4 27233 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  (
I `  C )
) ) )  =  ( K `  (
I `  C )
)
192190, 191eqtr3i 2482 . . . . . . . . . 10  |-  ( X 
\  ( I `  ( K `  ( I `
 A ) ) ) )  =  ( K `  ( I `
 C ) )
193192, 150eqeltri 2535 . . . . . . . . 9  |-  ( X 
\  ( I `  ( K `  ( I `
 A ) ) ) )  e.  T
19413, 14, 26, 27, 18, 68kur14lem6 27235 . . . . . . . . . 10  |-  ( K `
 ( I `  ( K `  ( I `
 A ) ) ) )  =  ( K `  ( I `
 A ) )
195194, 87eqeltri 2535 . . . . . . . . 9  |-  ( K `
 ( I `  ( K `  ( I `
 A ) ) ) )  e.  T
196189, 193, 195kur14lem1 27230 . . . . . . . 8  |-  ( N  =  ( I `  ( K `  ( I `
 A ) ) )  ->  ( N  C_  X  /\  { ( X  \  N ) ,  ( K `  N ) }  C_  T ) )
197187, 196jaoi 379 . . . . . . 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 379 . . . . 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 195 . . . 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 379 . . 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 195 . 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 2559 1  |-  ( N  e.  T  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 368    /\ wa 369    \/ w3o 964    = wceq 1370    e. wcel 1758    \ cdif 3425    u. cun 3426    C_ wss 3428   {cpr 3979   {ctp 3981   U.cuni 4191   ` cfv 5518   Topctop 18616   intcnt 18739   clsccl 18740
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-rep 4503  ax-sep 4513  ax-nul 4521  ax-pow 4570  ax-pr 4631  ax-un 6474
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-reu 2802  df-rab 2804  df-v 3072  df-sbc 3287  df-csb 3389  df-dif 3431  df-un 3433  df-in 3435  df-ss 3442  df-nul 3738  df-if 3892  df-pw 3962  df-sn 3978  df-pr 3980  df-tp 3982  df-op 3984  df-uni 4192  df-int 4229  df-iun 4273  df-iin 4274  df-br 4393  df-opab 4451  df-mpt 4452  df-id 4736  df-xp 4946  df-rel 4947  df-cnv 4948  df-co 4949  df-dm 4950  df-rn 4951  df-res 4952  df-ima 4953  df-iota 5481  df-fun 5520  df-fn 5521  df-f 5522  df-f1 5523  df-fo 5524  df-f1o 5525  df-fv 5526  df-top 18621  df-cld 18741  df-ntr 18742  df-cls 18743
This theorem is referenced by:  kur14lem9  27238
  Copyright terms: Public domain W3C validator