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

Theorem kur14lem7 24903
Description: Lemma for kur14 24907: 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 24902. (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 3490 . . 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 3490 . . . . 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 3490 . . . . . . 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 3854 . . . . . . . . 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 3512 . . . . . . . . . . . . 13  |-  { A ,  ( X  \  A ) ,  ( K `  A ) }  C_  ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C ,  ( I `
 A ) } )
7 ssun1 3512 . . . . . . . . . . . . . 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 3512 . . . . . . . . . . . . . . 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 3383 . . . . . . . . . . . . . 14  |-  ( ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C , 
( I `  A
) } )  u. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) } ) 
C_  T
117, 10sstri 3359 . . . . . . . . . . . . 13  |-  ( { A ,  ( X 
\  A ) ,  ( K `  A
) }  u.  { B ,  C , 
( I `  A
) } )  C_  T
126, 11sstri 3359 . . . . . . . . . . . 12  |-  { A ,  ( X  \  A ) ,  ( K `  A ) }  C_  T
13 kur14lem.j . . . . . . . . . . . . . . . 16  |-  J  e. 
Top
14 kur14lem.x . . . . . . . . . . . . . . . . 17  |-  X  = 
U. J
1514topopn 16984 . . . . . . . . . . . . . . . 16  |-  ( J  e.  Top  ->  X  e.  J )
1613, 15ax-mp 5 . . . . . . . . . . . . . . 15  |-  X  e.  J
1716elexi 2967 . . . . . . . . . . . . . 14  |-  X  e. 
_V
18 difss 3476 . . . . . . . . . . . . . 14  |-  ( X 
\  A )  C_  X
1917, 18ssexi 4351 . . . . . . . . . . . . 13  |-  ( X 
\  A )  e. 
_V
2019tpid2 3920 . . . . . . . . . . . 12  |-  ( X 
\  A )  e. 
{ A ,  ( X  \  A ) ,  ( K `  A ) }
2112, 20sselii 3347 . . . . . . . . . . 11  |-  ( X 
\  A )  e.  T
22 fvex 5745 . . . . . . . . . . . . 13  |-  ( K `
 A )  e. 
_V
2322tpid3 3922 . . . . . . . . . . . 12  |-  ( K `
 A )  e. 
{ A ,  ( X  \  A ) ,  ( K `  A ) }
2412, 23sselii 3347 . . . . . . . . . . 11  |-  ( K `
 A )  e.  T
255, 21, 24kur14lem1 24897 . . . . . . . . . 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 24900 . . . . . . . . . . . 12  |-  ( X 
\  ( X  \  A ) )  =  A
2917, 5ssexi 4351 . . . . . . . . . . . . . 14  |-  A  e. 
_V
3029tpid1 3919 . . . . . . . . . . . . 13  |-  A  e. 
{ A ,  ( X  \  A ) ,  ( K `  A ) }
3112, 30sselii 3347 . . . . . . . . . . . 12  |-  A  e.  T
3228, 31eqeltri 2508 . . . . . . . . . . 11  |-  ( X 
\  ( X  \  A ) )  e.  T
33 kur14lem.c . . . . . . . . . . . 12  |-  C  =  ( K `  ( X  \  A ) )
34 ssun2 3513 . . . . . . . . . . . . . 14  |-  { B ,  C ,  ( I `
 A ) } 
C_  ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C ,  ( I `
 A ) } )
3534, 11sstri 3359 . . . . . . . . . . . . 13  |-  { B ,  C ,  ( I `
 A ) } 
C_  T
3613, 14, 26, 27, 18kur14lem3 24899 . . . . . . . . . . . . . . . 16  |-  ( K `
 ( X  \  A ) )  C_  X
3733, 36eqsstri 3380 . . . . . . . . . . . . . . 15  |-  C  C_  X
3817, 37ssexi 4351 . . . . . . . . . . . . . 14  |-  C  e. 
_V
3938tpid2 3920 . . . . . . . . . . . . 13  |-  C  e. 
{ B ,  C ,  ( I `  A ) }
4035, 39sselii 3347 . . . . . . . . . . . 12  |-  C  e.  T
4133, 40eqeltrri 2509 . . . . . . . . . . 11  |-  ( K `
 ( X  \  A ) )  e.  T
4218, 32, 41kur14lem1 24897 . . . . . . . . . 10  |-  ( N  =  ( X  \  A )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
4313, 14, 26, 27, 5kur14lem3 24899 . . . . . . . . . . 11  |-  ( K `
 A )  C_  X
44 kur14lem.b . . . . . . . . . . . 12  |-  B  =  ( X  \  ( K `  A )
)
45 difss 3476 . . . . . . . . . . . . . . . 16  |-  ( X 
\  ( K `  A ) )  C_  X
4644, 45eqsstri 3380 . . . . . . . . . . . . . . 15  |-  B  C_  X
4717, 46ssexi 4351 . . . . . . . . . . . . . 14  |-  B  e. 
_V
4847tpid1 3919 . . . . . . . . . . . . 13  |-  B  e. 
{ B ,  C ,  ( I `  A ) }
4935, 48sselii 3347 . . . . . . . . . . . 12  |-  B  e.  T
5044, 49eqeltrri 2509 . . . . . . . . . . 11  |-  ( X 
\  ( K `  A ) )  e.  T
5113, 14, 26, 27, 5kur14lem5 24901 . . . . . . . . . . . 12  |-  ( K `
 ( K `  A ) )  =  ( K `  A
)
5251, 24eqeltri 2508 . . . . . . . . . . 11  |-  ( K `
 ( K `  A ) )  e.  T
5343, 50, 52kur14lem1 24897 . . . . . . . . . 10  |-  ( N  =  ( K `  A )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
5425, 42, 533jaoi 1248 . . . . . . . . 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 3854 . . . . . . . . 9  |-  ( N  e.  { B ,  C ,  ( I `  A ) }  ->  ( N  =  B  \/  N  =  C  \/  N  =  ( I `  A ) ) )
5744difeq2i 3464 . . . . . . . . . . . . 13  |-  ( X 
\  B )  =  ( X  \  ( X  \  ( K `  A ) ) )
5813, 14, 26, 27, 43kur14lem4 24900 . . . . . . . . . . . . 13  |-  ( X 
\  ( X  \ 
( K `  A
) ) )  =  ( K `  A
)
5957, 58eqtri 2458 . . . . . . . . . . . 12  |-  ( X 
\  B )  =  ( K `  A
)
6059, 24eqeltri 2508 . . . . . . . . . . 11  |-  ( X 
\  B )  e.  T
61 ssun2 3513 . . . . . . . . . . . . 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 3359 . . . . . . . . . . . 12  |-  { ( K `  B ) ,  D ,  ( K `  ( I `
 A ) ) }  C_  T
63 fvex 5745 . . . . . . . . . . . . 13  |-  ( K `
 B )  e. 
_V
6463tpid1 3919 . . . . . . . . . . . 12  |-  ( K `
 B )  e. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) }
6562, 64sselii 3347 . . . . . . . . . . 11  |-  ( K `
 B )  e.  T
6646, 60, 65kur14lem1 24897 . . . . . . . . . 10  |-  ( N  =  B  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
6733difeq2i 3464 . . . . . . . . . . . . 13  |-  ( X 
\  C )  =  ( X  \  ( K `  ( X  \  A ) ) )
6813, 14, 26, 27, 5kur14lem2 24898 . . . . . . . . . . . . 13  |-  ( I `
 A )  =  ( X  \  ( K `  ( X  \  A ) ) )
6967, 68eqtr4i 2461 . . . . . . . . . . . 12  |-  ( X 
\  C )  =  ( I `  A
)
70 fvex 5745 . . . . . . . . . . . . . 14  |-  ( I `
 A )  e. 
_V
7170tpid3 3922 . . . . . . . . . . . . 13  |-  ( I `
 A )  e. 
{ B ,  C ,  ( I `  A ) }
7235, 71sselii 3347 . . . . . . . . . . . 12  |-  ( I `
 A )  e.  T
7369, 72eqeltri 2508 . . . . . . . . . . 11  |-  ( X 
\  C )  e.  T
7413, 14, 26, 27, 18kur14lem5 24901 . . . . . . . . . . . . 13  |-  ( K `
 ( K `  ( X  \  A ) ) )  =  ( K `  ( X 
\  A ) )
7533fveq2i 5734 . . . . . . . . . . . . 13  |-  ( K `
 C )  =  ( K `  ( K `  ( X  \  A ) ) )
7674, 75, 333eqtr4i 2468 . . . . . . . . . . . 12  |-  ( K `
 C )  =  C
7776, 40eqeltri 2508 . . . . . . . . . . 11  |-  ( K `
 C )  e.  T
7837, 73, 77kur14lem1 24897 . . . . . . . . . 10  |-  ( N  =  C  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
79 difss 3476 . . . . . . . . . . . 12  |-  ( X 
\  ( K `  ( X  \  A ) ) )  C_  X
8068, 79eqsstri 3380 . . . . . . . . . . 11  |-  ( I `
 A )  C_  X
8169difeq2i 3464 . . . . . . . . . . . . 13  |-  ( X 
\  ( X  \  C ) )  =  ( X  \  (
I `  A )
)
8213, 14, 26, 27, 37kur14lem4 24900 . . . . . . . . . . . . 13  |-  ( X 
\  ( X  \  C ) )  =  C
8381, 82eqtr3i 2460 . . . . . . . . . . . 12  |-  ( X 
\  ( I `  A ) )  =  C
8483, 40eqeltri 2508 . . . . . . . . . . 11  |-  ( X 
\  ( I `  A ) )  e.  T
85 fvex 5745 . . . . . . . . . . . . 13  |-  ( K `
 ( I `  A ) )  e. 
_V
8685tpid3 3922 . . . . . . . . . . . 12  |-  ( K `
 ( I `  A ) )  e. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) }
8762, 86sselii 3347 . . . . . . . . . . 11  |-  ( K `
 ( I `  A ) )  e.  T
8880, 84, 87kur14lem1 24897 . . . . . . . . . 10  |-  ( N  =  ( I `  A )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
8966, 78, 883jaoi 1248 . . . . . . . . 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 370 . . . . . . 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 189 . . . . . 6  |-  ( N  e.  ( { A ,  ( X  \  A ) ,  ( K `  A ) }  u.  { B ,  C ,  ( I `
 A ) } )  ->  ( N  C_  X  /\  { ( X  \  N ) ,  ( K `  N ) }  C_  T ) )
93 eltpi 3854 . . . . . . 7  |-  ( N  e.  { ( K `
 B ) ,  D ,  ( K `
 ( I `  A ) ) }  ->  ( N  =  ( K `  B
)  \/  N  =  D  \/  N  =  ( K `  (
I `  A )
) ) )
9413, 14, 26, 27, 46kur14lem3 24899 . . . . . . . . 9  |-  ( K `
 B )  C_  X
9513, 14, 26, 27, 43kur14lem2 24898 . . . . . . . . . . 11  |-  ( I `
 ( K `  A ) )  =  ( X  \  ( K `  ( X  \  ( K `  A
) ) ) )
96 kur14lem.d . . . . . . . . . . 11  |-  D  =  ( I `  ( K `  A )
)
9744fveq2i 5734 . . . . . . . . . . . 12  |-  ( K `
 B )  =  ( K `  ( X  \  ( K `  A ) ) )
9897difeq2i 3464 . . . . . . . . . . 11  |-  ( X 
\  ( K `  B ) )  =  ( X  \  ( K `  ( X  \  ( K `  A
) ) ) )
9995, 96, 983eqtr4i 2468 . . . . . . . . . 10  |-  D  =  ( X  \  ( K `  B )
)
10096, 95eqtri 2458 . . . . . . . . . . . . . 14  |-  D  =  ( X  \  ( K `  ( X  \  ( K `  A
) ) ) )
101 difss 3476 . . . . . . . . . . . . . 14  |-  ( X 
\  ( K `  ( X  \  ( K `  A )
) ) )  C_  X
102100, 101eqsstri 3380 . . . . . . . . . . . . 13  |-  D  C_  X
10317, 102ssexi 4351 . . . . . . . . . . . 12  |-  D  e. 
_V
104103tpid2 3920 . . . . . . . . . . 11  |-  D  e. 
{ ( K `  B ) ,  D ,  ( K `  ( I `  A
) ) }
10562, 104sselii 3347 . . . . . . . . . 10  |-  D  e.  T
10699, 105eqeltrri 2509 . . . . . . . . 9  |-  ( X 
\  ( K `  B ) )  e.  T
10713, 14, 26, 27, 46kur14lem5 24901 . . . . . . . . . 10  |-  ( K `
 ( K `  B ) )  =  ( K `  B
)
108107, 65eqeltri 2508 . . . . . . . . 9  |-  ( K `
 ( K `  B ) )  e.  T
10994, 106, 108kur14lem1 24897 . . . . . . . 8  |-  ( N  =  ( K `  B )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
11099difeq2i 3464 . . . . . . . . . . 11  |-  ( X 
\  D )  =  ( X  \  ( X  \  ( K `  B ) ) )
11113, 14, 26, 27, 94kur14lem4 24900 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  B
) ) )  =  ( K `  B
)
112110, 111eqtri 2458 . . . . . . . . . 10  |-  ( X 
\  D )  =  ( K `  B
)
113112, 65eqeltri 2508 . . . . . . . . 9  |-  ( X 
\  D )  e.  T
114 ssun1 3512 . . . . . . . . . . 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 3513 . . . . . . . . . . . 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 3383 . . . . . . . . . . 11  |-  ( { ( I `  C
) ,  ( K `
 D ) ,  ( I `  ( K `  B )
) }  u.  {
( K `  (
I `  C )
) ,  ( I `
 ( K `  ( I `  A
) ) ) } )  C_  T
117114, 116sstri 3359 . . . . . . . . . 10  |-  { ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `
 B ) ) }  C_  T
118 fvex 5745 . . . . . . . . . . 11  |-  ( K `
 D )  e. 
_V
119118tpid2 3920 . . . . . . . . . 10  |-  ( K `
 D )  e. 
{ ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `  B ) ) }
120117, 119sselii 3347 . . . . . . . . 9  |-  ( K `
 D )  e.  T
121102, 113, 120kur14lem1 24897 . . . . . . . 8  |-  ( N  =  D  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
12213, 14, 26, 27, 80kur14lem3 24899 . . . . . . . . 9  |-  ( K `
 ( I `  A ) )  C_  X
12313, 14, 26, 27, 37kur14lem2 24898 . . . . . . . . . . 11  |-  ( I `
 C )  =  ( X  \  ( K `  ( X  \  C ) ) )
12469fveq2i 5734 . . . . . . . . . . . 12  |-  ( K `
 ( X  \  C ) )  =  ( K `  (
I `  A )
)
125124difeq2i 3464 . . . . . . . . . . 11  |-  ( X 
\  ( K `  ( X  \  C ) ) )  =  ( X  \  ( K `
 ( I `  A ) ) )
126123, 125eqtri 2458 . . . . . . . . . 10  |-  ( I `
 C )  =  ( X  \  ( K `  ( I `  A ) ) )
127 fvex 5745 . . . . . . . . . . . 12  |-  ( I `
 C )  e. 
_V
128127tpid1 3919 . . . . . . . . . . 11  |-  ( I `
 C )  e. 
{ ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `  B ) ) }
129117, 128sselii 3347 . . . . . . . . . 10  |-  ( I `
 C )  e.  T
130126, 129eqeltrri 2509 . . . . . . . . 9  |-  ( X 
\  ( K `  ( I `  A
) ) )  e.  T
13113, 14, 26, 27, 80kur14lem5 24901 . . . . . . . . . 10  |-  ( K `
 ( K `  ( I `  A
) ) )  =  ( K `  (
I `  A )
)
132131, 87eqeltri 2508 . . . . . . . . 9  |-  ( K `
 ( K `  ( I `  A
) ) )  e.  T
133122, 130, 132kur14lem1 24897 . . . . . . . 8  |-  ( N  =  ( K `  ( I `  A
) )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
134109, 121, 1333jaoi 1248 . . . . . . 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 370 . . . . 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 189 . . . 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 3490 . . . . 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 3854 . . . . . . 7  |-  ( N  e.  { ( I `
 C ) ,  ( K `  D
) ,  ( I `
 ( K `  B ) ) }  ->  ( N  =  ( I `  C
)  \/  N  =  ( K `  D
)  \/  N  =  ( I `  ( K `  B )
) ) )
140 difss 3476 . . . . . . . . . 10  |-  ( X 
\  ( K `  ( X  \  C ) ) )  C_  X
141123, 140eqsstri 3380 . . . . . . . . 9  |-  ( I `
 C )  C_  X
142126difeq2i 3464 . . . . . . . . . . 11  |-  ( X 
\  ( I `  C ) )  =  ( X  \  ( X  \  ( K `  ( I `  A
) ) ) )
14313, 14, 26, 27, 122kur14lem4 24900 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  (
I `  A )
) ) )  =  ( K `  (
I `  A )
)
144142, 143eqtri 2458 . . . . . . . . . 10  |-  ( X 
\  ( I `  C ) )  =  ( K `  (
I `  A )
)
145144, 87eqeltri 2508 . . . . . . . . 9  |-  ( X 
\  ( I `  C ) )  e.  T
146 ssun2 3513 . . . . . . . . . . 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 3359 . . . . . . . . . 10  |-  { ( K `  ( I `
 C ) ) ,  ( I `  ( K `  ( I `
 A ) ) ) }  C_  T
148 fvex 5745 . . . . . . . . . . 11  |-  ( K `
 ( I `  C ) )  e. 
_V
149148prid1 3914 . . . . . . . . . 10  |-  ( K `
 ( I `  C ) )  e. 
{ ( K `  ( I `  C
) ) ,  ( I `  ( K `
 ( I `  A ) ) ) }
150147, 149sselii 3347 . . . . . . . . 9  |-  ( K `
 ( I `  C ) )  e.  T
151141, 145, 150kur14lem1 24897 . . . . . . . 8  |-  ( N  =  ( I `  C )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
15213, 14, 26, 27, 102kur14lem3 24899 . . . . . . . . 9  |-  ( K `
 D )  C_  X
15399fveq2i 5734 . . . . . . . . . . . 12  |-  ( K `
 D )  =  ( K `  ( X  \  ( K `  B ) ) )
154153difeq2i 3464 . . . . . . . . . . 11  |-  ( X 
\  ( K `  D ) )  =  ( X  \  ( K `  ( X  \  ( K `  B
) ) ) )
15513, 14, 26, 27, 94kur14lem2 24898 . . . . . . . . . . 11  |-  ( I `
 ( K `  B ) )  =  ( X  \  ( K `  ( X  \  ( K `  B
) ) ) )
156154, 155eqtr4i 2461 . . . . . . . . . 10  |-  ( X 
\  ( K `  D ) )  =  ( I `  ( K `  B )
)
157 fvex 5745 . . . . . . . . . . . 12  |-  ( I `
 ( K `  B ) )  e. 
_V
158157tpid3 3922 . . . . . . . . . . 11  |-  ( I `
 ( K `  B ) )  e. 
{ ( I `  C ) ,  ( K `  D ) ,  ( I `  ( K `  B ) ) }
159117, 158sselii 3347 . . . . . . . . . 10  |-  ( I `
 ( K `  B ) )  e.  T
160156, 159eqeltri 2508 . . . . . . . . 9  |-  ( X 
\  ( K `  D ) )  e.  T
16113, 14, 26, 27, 102kur14lem5 24901 . . . . . . . . . 10  |-  ( K `
 ( K `  D ) )  =  ( K `  D
)
162161, 120eqeltri 2508 . . . . . . . . 9  |-  ( K `
 ( K `  D ) )  e.  T
163152, 160, 162kur14lem1 24897 . . . . . . . 8  |-  ( N  =  ( K `  D )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
164 difss 3476 . . . . . . . . . 10  |-  ( X 
\  ( K `  ( X  \  ( K `  B )
) ) )  C_  X
165155, 164eqsstri 3380 . . . . . . . . 9  |-  ( I `
 ( K `  B ) )  C_  X
166156difeq2i 3464 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  D
) ) )  =  ( X  \  (
I `  ( K `  B ) ) )
16713, 14, 26, 27, 152kur14lem4 24900 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  D
) ) )  =  ( K `  D
)
168166, 167eqtr3i 2460 . . . . . . . . . 10  |-  ( X 
\  ( I `  ( K `  B ) ) )  =  ( K `  D )
169168, 120eqeltri 2508 . . . . . . . . 9  |-  ( X 
\  ( I `  ( K `  B ) ) )  e.  T
17013, 14, 26, 27, 5, 44kur14lem6 24902 . . . . . . . . . 10  |-  ( K `
 ( I `  ( K `  B ) ) )  =  ( K `  B )
171170, 65eqeltri 2508 . . . . . . . . 9  |-  ( K `
 ( I `  ( K `  B ) ) )  e.  T
172165, 169, 171kur14lem1 24897 . . . . . . . 8  |-  ( N  =  ( I `  ( K `  B ) )  ->  ( N  C_  X  /\  { ( X  \  N ) ,  ( K `  N ) }  C_  T ) )
173151, 163, 1723jaoi 1248 . . . . . . 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 3836 . . . . . . 7  |-  ( N  e.  { ( K `
 ( I `  C ) ) ,  ( I `  ( K `  ( I `  A ) ) ) }  ->  ( N  =  ( K `  ( I `  C
) )  \/  N  =  ( I `  ( K `  ( I `
 A ) ) ) ) )
17613, 14, 26, 27, 141kur14lem3 24899 . . . . . . . . 9  |-  ( K `
 ( I `  C ) )  C_  X
177126fveq2i 5734 . . . . . . . . . . . 12  |-  ( K `
 ( I `  C ) )  =  ( K `  ( X  \  ( K `  ( I `  A
) ) ) )
178177difeq2i 3464 . . . . . . . . . . 11  |-  ( X 
\  ( K `  ( I `  C
) ) )  =  ( X  \  ( K `  ( X  \  ( K `  (
I `  A )
) ) ) )
17913, 14, 26, 27, 122kur14lem2 24898 . . . . . . . . . . 11  |-  ( I `
 ( K `  ( I `  A
) ) )  =  ( X  \  ( K `  ( X  \  ( K `  (
I `  A )
) ) ) )
180178, 179eqtr4i 2461 . . . . . . . . . 10  |-  ( X 
\  ( K `  ( I `  C
) ) )  =  ( I `  ( K `  ( I `  A ) ) )
181 fvex 5745 . . . . . . . . . . . 12  |-  ( I `
 ( K `  ( I `  A
) ) )  e. 
_V
182181prid2 3915 . . . . . . . . . . 11  |-  ( I `
 ( K `  ( I `  A
) ) )  e. 
{ ( K `  ( I `  C
) ) ,  ( I `  ( K `
 ( I `  A ) ) ) }
183147, 182sselii 3347 . . . . . . . . . 10  |-  ( I `
 ( K `  ( I `  A
) ) )  e.  T
184180, 183eqeltri 2508 . . . . . . . . 9  |-  ( X 
\  ( K `  ( I `  C
) ) )  e.  T
18513, 14, 26, 27, 141kur14lem5 24901 . . . . . . . . . 10  |-  ( K `
 ( K `  ( I `  C
) ) )  =  ( K `  (
I `  C )
)
186185, 150eqeltri 2508 . . . . . . . . 9  |-  ( K `
 ( K `  ( I `  C
) ) )  e.  T
187176, 184, 186kur14lem1 24897 . . . . . . . 8  |-  ( N  =  ( K `  ( I `  C
) )  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
188 difss 3476 . . . . . . . . . 10  |-  ( X 
\  ( K `  ( X  \  ( K `  ( I `  A ) ) ) ) )  C_  X
189179, 188eqsstri 3380 . . . . . . . . 9  |-  ( I `
 ( K `  ( I `  A
) ) )  C_  X
190180difeq2i 3464 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  (
I `  C )
) ) )  =  ( X  \  (
I `  ( K `  ( I `  A
) ) ) )
19113, 14, 26, 27, 176kur14lem4 24900 . . . . . . . . . . 11  |-  ( X 
\  ( X  \ 
( K `  (
I `  C )
) ) )  =  ( K `  (
I `  C )
)
192190, 191eqtr3i 2460 . . . . . . . . . 10  |-  ( X 
\  ( I `  ( K `  ( I `
 A ) ) ) )  =  ( K `  ( I `
 C ) )
193192, 150eqeltri 2508 . . . . . . . . 9  |-  ( X 
\  ( I `  ( K `  ( I `
 A ) ) ) )  e.  T
19413, 14, 26, 27, 18, 68kur14lem6 24902 . . . . . . . . . 10  |-  ( K `
 ( I `  ( K `  ( I `
 A ) ) ) )  =  ( K `  ( I `
 A ) )
195194, 87eqeltri 2508 . . . . . . . . 9  |-  ( K `
 ( I `  ( K `  ( I `
 A ) ) ) )  e.  T
196189, 193, 195kur14lem1 24897 . . . . . . . 8  |-  ( N  =  ( I `  ( K `  ( I `
 A ) ) )  ->  ( N  C_  X  /\  { ( X  \  N ) ,  ( K `  N ) }  C_  T ) )
197187, 196jaoi 370 . . . . . . 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 370 . . . . 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 189 . . . 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 370 . . 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 189 . 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 2530 1  |-  ( N  e.  T  ->  ( N  C_  X  /\  {
( X  \  N
) ,  ( K `
 N ) } 
C_  T ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 359    /\ wa 360    \/ w3o 936    = wceq 1653    e. wcel 1726    \ cdif 3319    u. cun 3320    C_ wss 3322   {cpr 3817   {ctp 3818   U.cuni 4017   ` cfv 5457   Topctop 16963   intcnt 17086   clsccl 17087
This theorem is referenced by:  kur14lem9  24905
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4323  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-int 4053  df-iun 4097  df-iin 4098  df-br 4216  df-opab 4270  df-mpt 4271  df-id 4501  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-top 16968  df-cld 17088  df-ntr 17089  df-cls 17090
  Copyright terms: Public domain W3C validator