Theorem kur14lem7 31194

Description: Lemma for kur14 31198: 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 31193. (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

Step	Hyp	Ref	Expression
1		elun 3753	. . 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 3753	. . . . 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 3753	. . . . . . 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 4229	. . . . . . . . 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 3776	. . . . . . . . . . . . 13 |- { A , ( X \ A ) , ( K ` A ) } C_ ( { A , ( X \ A ) , ( K ` A ) } u. { B , C , ( I ` A ) } )
7		ssun1 3776	. . . . . . . . . . . . . 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 3776	. . . . . . . . . . . . . . 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 ) ) ) } ) )
10	8, 9	sseqtr4i 3638	. . . . . . . . . . . . . 14 |- ( ( { A , ( X \ A ) , ( K ` A ) } u. { B , C , ( I ` A ) } ) u. { ( K ` B ) , D , ( K ` ( I ` A ) ) } ) C_ T
11	7, 10	sstri 3612	. . . . . . . . . . . . 13 |- ( { A , ( X \ A ) , ( K ` A ) } u. { B , C , ( I ` A ) } ) C_ T
12	6, 11	sstri 3612	. . . . . . . . . . . 12 |- { A , ( X \ A ) , ( K ` A ) } C_ T
13		kur14lem.j	. . . . . . . . . . . . . . . 16 |- J e. Top
14		kur14lem.x	. . . . . . . . . . . . . . . . 17 |- X = U. J
15	14	topopn 20711	. . . . . . . . . . . . . . . 16 |- ( J e. Top -> X e. J )
16	13, 15	ax-mp 5	. . . . . . . . . . . . . . 15 |- X e. J
17	16	elexi 3213	. . . . . . . . . . . . . 14 |- X e. _V
18		difss 3737	. . . . . . . . . . . . . 14 |- ( X \ A ) C_ X
19	17, 18	ssexi 4803	. . . . . . . . . . . . 13 |- ( X \ A ) e. _V
20	19	tpid2 4304	. . . . . . . . . . . 12 |- ( X \ A ) e. { A , ( X \ A ) , ( K ` A ) }
21	12, 20	sselii 3600	. . . . . . . . . . 11 |- ( X \ A ) e. T
22		fvex 6201	. . . . . . . . . . . . 13 |- ( K ` A ) e. _V
23	22	tpid3 4307	. . . . . . . . . . . 12 |- ( K ` A ) e. { A , ( X \ A ) , ( K ` A ) }
24	12, 23	sselii 3600	. . . . . . . . . . 11 |- ( K ` A ) e. T
25	5, 21, 24	kur14lem1 31188	. . . . . . . . . 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 )
28	13, 14, 26, 27, 5	kur14lem4 31191	. . . . . . . . . . . 12 |- ( X \ ( X \ A ) ) = A
29	17, 5	ssexi 4803	. . . . . . . . . . . . . 14 |- A e. _V
30	29	tpid1 4303	. . . . . . . . . . . . 13 |- A e. { A , ( X \ A ) , ( K ` A ) }
31	12, 30	sselii 3600	. . . . . . . . . . . 12 |- A e. T
32	28, 31	eqeltri 2697	. . . . . . . . . . 11 |- ( X \ ( X \ A ) ) e. T
33		kur14lem.c	. . . . . . . . . . . 12 |- C = ( K ` ( X \ A ) )
34		ssun2 3777	. . . . . . . . . . . . . 14 |- { B , C , ( I ` A ) } C_ ( { A , ( X \ A ) , ( K ` A ) } u. { B , C , ( I ` A ) } )
35	34, 11	sstri 3612	. . . . . . . . . . . . 13 |- { B , C , ( I ` A ) } C_ T
36	13, 14, 26, 27, 18	kur14lem3 31190	. . . . . . . . . . . . . . . 16 |- ( K ` ( X \ A ) ) C_ X
37	33, 36	eqsstri 3635	. . . . . . . . . . . . . . 15 |- C C_ X
38	17, 37	ssexi 4803	. . . . . . . . . . . . . 14 |- C e. _V
39	38	tpid2 4304	. . . . . . . . . . . . 13 |- C e. { B , C , ( I ` A ) }
40	35, 39	sselii 3600	. . . . . . . . . . . 12 |- C e. T
41	33, 40	eqeltrri 2698	. . . . . . . . . . 11 |- ( K ` ( X \ A ) ) e. T
42	18, 32, 41	kur14lem1 31188	. . . . . . . . . 10 |- ( N = ( X \ A ) -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )
43	13, 14, 26, 27, 5	kur14lem3 31190	. . . . . . . . . . 11 |- ( K ` A ) C_ X
44		kur14lem.b	. . . . . . . . . . . 12 |- B = ( X \ ( K ` A ) )
45		difss 3737	. . . . . . . . . . . . . . . 16 |- ( X \ ( K ` A ) ) C_ X
46	44, 45	eqsstri 3635	. . . . . . . . . . . . . . 15 |- B C_ X
47	17, 46	ssexi 4803	. . . . . . . . . . . . . 14 |- B e. _V
48	47	tpid1 4303	. . . . . . . . . . . . 13 |- B e. { B , C , ( I ` A ) }
49	35, 48	sselii 3600	. . . . . . . . . . . 12 |- B e. T
50	44, 49	eqeltrri 2698	. . . . . . . . . . 11 |- ( X \ ( K ` A ) ) e. T
51	13, 14, 26, 27, 5	kur14lem5 31192	. . . . . . . . . . . 12 |- ( K ` ( K ` A ) ) = ( K ` A )
52	51, 24	eqeltri 2697	. . . . . . . . . . 11 |- ( K ` ( K ` A ) ) e. T
53	43, 50, 52	kur14lem1 31188	. . . . . . . . . 10 |- ( N = ( K ` A ) -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )
54	25, 42, 53	3jaoi 1391	. . . . . . . . 9 |- ( ( N = A \/ N = ( X \ A ) \/ N = ( K ` A ) ) -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )
55	4, 54	syl 17	. . . . . . . 8 |- ( N e. { A , ( X \ A ) , ( K ` A ) } -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )
56		eltpi 4229	. . . . . . . . 9 |- ( N e. { B , C , ( I ` A ) } -> ( N = B \/ N = C \/ N = ( I ` A ) ) )
57	44	difeq2i 3725	. . . . . . . . . . . . 13 |- ( X \ B ) = ( X \ ( X \ ( K ` A ) ) )
58	13, 14, 26, 27, 43	kur14lem4 31191	. . . . . . . . . . . . 13 |- ( X \ ( X \ ( K ` A ) ) ) = ( K ` A )
59	57, 58	eqtri 2644	. . . . . . . . . . . 12 |- ( X \ B ) = ( K ` A )
60	59, 24	eqeltri 2697	. . . . . . . . . . 11 |- ( X \ B ) e. T
61		ssun2 3777	. . . . . . . . . . . . 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 ) ) } )
62	61, 10	sstri 3612	. . . . . . . . . . . 12 |- { ( K ` B ) , D , ( K ` ( I ` A ) ) } C_ T
63		fvex 6201	. . . . . . . . . . . . 13 |- ( K ` B ) e. _V
64	63	tpid1 4303	. . . . . . . . . . . 12 |- ( K ` B ) e. { ( K ` B ) , D , ( K ` ( I ` A ) ) }
65	62, 64	sselii 3600	. . . . . . . . . . 11 |- ( K ` B ) e. T
66	46, 60, 65	kur14lem1 31188	. . . . . . . . . 10 |- ( N = B -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )
67	33	difeq2i 3725	. . . . . . . . . . . . 13 |- ( X \ C ) = ( X \ ( K ` ( X \ A ) ) )
68	13, 14, 26, 27, 5	kur14lem2 31189	. . . . . . . . . . . . 13 |- ( I ` A ) = ( X \ ( K ` ( X \ A ) ) )
69	67, 68	eqtr4i 2647	. . . . . . . . . . . 12 |- ( X \ C ) = ( I ` A )
70		fvex 6201	. . . . . . . . . . . . . 14 |- ( I ` A ) e. _V
71	70	tpid3 4307	. . . . . . . . . . . . 13 |- ( I ` A ) e. { B , C , ( I ` A ) }
72	35, 71	sselii 3600	. . . . . . . . . . . 12 |- ( I ` A ) e. T
73	69, 72	eqeltri 2697	. . . . . . . . . . 11 |- ( X \ C ) e. T
74	13, 14, 26, 27, 18	kur14lem5 31192	. . . . . . . . . . . . 13 |- ( K ` ( K ` ( X \ A ) ) ) = ( K ` ( X \ A ) )
75	33	fveq2i 6194	. . . . . . . . . . . . 13 |- ( K ` C ) = ( K ` ( K ` ( X \ A ) ) )
76	74, 75, 33	3eqtr4i 2654	. . . . . . . . . . . 12 |- ( K ` C ) = C
77	76, 40	eqeltri 2697	. . . . . . . . . . 11 |- ( K ` C ) e. T
78	37, 73, 77	kur14lem1 31188	. . . . . . . . . 10 |- ( N = C -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )
79		difss 3737	. . . . . . . . . . . 12 |- ( X \ ( K ` ( X \ A ) ) ) C_ X
80	68, 79	eqsstri 3635	. . . . . . . . . . 11 |- ( I ` A ) C_ X
81	69	difeq2i 3725	. . . . . . . . . . . . 13 |- ( X \ ( X \ C ) ) = ( X \ ( I ` A ) )
82	13, 14, 26, 27, 37	kur14lem4 31191	. . . . . . . . . . . . 13 |- ( X \ ( X \ C ) ) = C
83	81, 82	eqtr3i 2646	. . . . . . . . . . . 12 |- ( X \ ( I ` A ) ) = C
84	83, 40	eqeltri 2697	. . . . . . . . . . 11 |- ( X \ ( I ` A ) ) e. T
85		fvex 6201	. . . . . . . . . . . . 13 |- ( K ` ( I ` A ) ) e. _V
86	85	tpid3 4307	. . . . . . . . . . . 12 |- ( K ` ( I ` A ) ) e. { ( K ` B ) , D , ( K ` ( I ` A ) ) }
87	62, 86	sselii 3600	. . . . . . . . . . 11 |- ( K ` ( I ` A ) ) e. T
88	80, 84, 87	kur14lem1 31188	. . . . . . . . . 10 |- ( N = ( I ` A ) -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )
89	66, 78, 88	3jaoi 1391	. . . . . . . . 9 |- ( ( N = B \/ N = C \/ N = ( I ` A ) ) -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )
90	56, 89	syl 17	. . . . . . . 8 |- ( N e. { B , C , ( I ` A ) } -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )
91	55, 90	jaoi 394	. . . . . . 7 |- ( ( N e. { A , ( X \ A ) , ( K ` A ) } \/ N e. { B , C , ( I ` A ) } ) -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )
92	3, 91	sylbi 207	. . . . . 6 |- ( N e. ( { A , ( X \ A ) , ( K ` A ) } u. { B , C , ( I ` A ) } ) -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )
93		eltpi 4229	. . . . . . 7 |- ( N e. { ( K ` B ) , D , ( K ` ( I ` A ) ) } -> ( N = ( K ` B ) \/ N = D \/ N = ( K ` ( I ` A ) ) ) )
94	13, 14, 26, 27, 46	kur14lem3 31190	. . . . . . . . 9 |- ( K ` B ) C_ X
95	13, 14, 26, 27, 43	kur14lem2 31189	. . . . . . . . . . 11 |- ( I ` ( K ` A ) ) = ( X \ ( K ` ( X \ ( K ` A ) ) ) )
96		kur14lem.d	. . . . . . . . . . 11 |- D = ( I ` ( K ` A ) )
97	44	fveq2i 6194	. . . . . . . . . . . 12 |- ( K ` B ) = ( K ` ( X \ ( K ` A ) ) )
98	97	difeq2i 3725	. . . . . . . . . . 11 |- ( X \ ( K ` B ) ) = ( X \ ( K ` ( X \ ( K ` A ) ) ) )
99	95, 96, 98	3eqtr4i 2654	. . . . . . . . . 10 |- D = ( X \ ( K ` B ) )
100	96, 95	eqtri 2644	. . . . . . . . . . . . . 14 |- D = ( X \ ( K ` ( X \ ( K ` A ) ) ) )
101		difss 3737	. . . . . . . . . . . . . 14 |- ( X \ ( K ` ( X \ ( K ` A ) ) ) ) C_ X
102	100, 101	eqsstri 3635	. . . . . . . . . . . . 13 |- D C_ X
103	17, 102	ssexi 4803	. . . . . . . . . . . 12 |- D e. _V
104	103	tpid2 4304	. . . . . . . . . . 11 |- D e. { ( K ` B ) , D , ( K ` ( I ` A ) ) }
105	62, 104	sselii 3600	. . . . . . . . . 10 |- D e. T
106	99, 105	eqeltrri 2698	. . . . . . . . 9 |- ( X \ ( K ` B ) ) e. T
107	13, 14, 26, 27, 46	kur14lem5 31192	. . . . . . . . . 10 |- ( K ` ( K ` B ) ) = ( K ` B )
108	107, 65	eqeltri 2697	. . . . . . . . 9 |- ( K ` ( K ` B ) ) e. T
109	94, 106, 108	kur14lem1 31188	. . . . . . . 8 |- ( N = ( K ` B ) -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )
110	99	difeq2i 3725	. . . . . . . . . . 11 |- ( X \ D ) = ( X \ ( X \ ( K ` B ) ) )
111	13, 14, 26, 27, 94	kur14lem4 31191	. . . . . . . . . . 11 |- ( X \ ( X \ ( K ` B ) ) ) = ( K ` B )
112	110, 111	eqtri 2644	. . . . . . . . . 10 |- ( X \ D ) = ( K ` B )
113	112, 65	eqeltri 2697	. . . . . . . . 9 |- ( X \ D ) e. T
114		ssun1 3776	. . . . . . . . . . 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 3777	. . . . . . . . . . . 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 ) ) ) } ) )
116	115, 9	sseqtr4i 3638	. . . . . . . . . . 11 |- ( { ( I ` C ) , ( K ` D ) , ( I ` ( K ` B ) ) } u. { ( K ` ( I ` C ) ) , ( I ` ( K ` ( I ` A ) ) ) } ) C_ T
117	114, 116	sstri 3612	. . . . . . . . . 10 |- { ( I ` C ) , ( K ` D ) , ( I ` ( K ` B ) ) } C_ T
118		fvex 6201	. . . . . . . . . . 11 |- ( K ` D ) e. _V
119	118	tpid2 4304	. . . . . . . . . 10 |- ( K ` D ) e. { ( I ` C ) , ( K ` D ) , ( I ` ( K ` B ) ) }
120	117, 119	sselii 3600	. . . . . . . . 9 |- ( K ` D ) e. T
121	102, 113, 120	kur14lem1 31188	. . . . . . . 8 |- ( N = D -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )
122	13, 14, 26, 27, 80	kur14lem3 31190	. . . . . . . . 9 |- ( K ` ( I ` A ) ) C_ X
123	13, 14, 26, 27, 37	kur14lem2 31189	. . . . . . . . . . 11 |- ( I ` C ) = ( X \ ( K ` ( X \ C ) ) )
124	69	fveq2i 6194	. . . . . . . . . . . 12 |- ( K ` ( X \ C ) ) = ( K ` ( I ` A ) )
125	124	difeq2i 3725	. . . . . . . . . . 11 |- ( X \ ( K ` ( X \ C ) ) ) = ( X \ ( K ` ( I ` A ) ) )
126	123, 125	eqtri 2644	. . . . . . . . . 10 |- ( I ` C ) = ( X \ ( K ` ( I ` A ) ) )
127		fvex 6201	. . . . . . . . . . . 12 |- ( I ` C ) e. _V
128	127	tpid1 4303	. . . . . . . . . . 11 |- ( I ` C ) e. { ( I ` C ) , ( K ` D ) , ( I ` ( K ` B ) ) }
129	117, 128	sselii 3600	. . . . . . . . . 10 |- ( I ` C ) e. T
130	126, 129	eqeltrri 2698	. . . . . . . . 9 |- ( X \ ( K ` ( I ` A ) ) ) e. T
131	13, 14, 26, 27, 80	kur14lem5 31192	. . . . . . . . . 10 |- ( K ` ( K ` ( I ` A ) ) ) = ( K ` ( I ` A ) )
132	131, 87	eqeltri 2697	. . . . . . . . 9 |- ( K ` ( K ` ( I ` A ) ) ) e. T
133	122, 130, 132	kur14lem1 31188	. . . . . . . 8 |- ( N = ( K ` ( I ` A ) ) -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )
134	109, 121, 133	3jaoi 1391	. . . . . . 7 |- ( ( N = ( K ` B ) \/ N = D \/ N = ( K ` ( I ` A ) ) ) -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )
135	93, 134	syl 17	. . . . . 6 |- ( N e. { ( K ` B ) , D , ( K ` ( I ` A ) ) } -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )
136	92, 135	jaoi 394	. . . . 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 ) )
137	2, 136	sylbi 207	. . . 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 3753	. . . . 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 4229	. . . . . . 7 |- ( N e. { ( I ` C ) , ( K ` D ) , ( I ` ( K ` B ) ) } -> ( N = ( I ` C ) \/ N = ( K ` D ) \/ N = ( I ` ( K ` B ) ) ) )
140		difss 3737	. . . . . . . . . 10 |- ( X \ ( K ` ( X \ C ) ) ) C_ X
141	123, 140	eqsstri 3635	. . . . . . . . 9 |- ( I ` C ) C_ X
142	126	difeq2i 3725	. . . . . . . . . . 11 |- ( X \ ( I ` C ) ) = ( X \ ( X \ ( K ` ( I ` A ) ) ) )
143	13, 14, 26, 27, 122	kur14lem4 31191	. . . . . . . . . . 11 |- ( X \ ( X \ ( K ` ( I ` A ) ) ) ) = ( K ` ( I ` A ) )
144	142, 143	eqtri 2644	. . . . . . . . . 10 |- ( X \ ( I ` C ) ) = ( K ` ( I ` A ) )
145	144, 87	eqeltri 2697	. . . . . . . . 9 |- ( X \ ( I ` C ) ) e. T
146		ssun2 3777	. . . . . . . . . . 11 |- { ( K ` ( I ` C ) ) , ( I ` ( K ` ( I ` A ) ) ) } C_ ( { ( I ` C ) , ( K ` D ) , ( I ` ( K ` B ) ) } u. { ( K ` ( I ` C ) ) , ( I ` ( K ` ( I ` A ) ) ) } )
147	146, 116	sstri 3612	. . . . . . . . . 10 |- { ( K ` ( I ` C ) ) , ( I ` ( K ` ( I ` A ) ) ) } C_ T
148		fvex 6201	. . . . . . . . . . 11 |- ( K ` ( I ` C ) ) e. _V
149	148	prid1 4297	. . . . . . . . . 10 |- ( K ` ( I ` C ) ) e. { ( K ` ( I ` C ) ) , ( I ` ( K ` ( I ` A ) ) ) }
150	147, 149	sselii 3600	. . . . . . . . 9 |- ( K ` ( I ` C ) ) e. T
151	141, 145, 150	kur14lem1 31188	. . . . . . . 8 |- ( N = ( I ` C ) -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )
152	13, 14, 26, 27, 102	kur14lem3 31190	. . . . . . . . 9 |- ( K ` D ) C_ X
153	99	fveq2i 6194	. . . . . . . . . . . 12 |- ( K ` D ) = ( K ` ( X \ ( K ` B ) ) )
154	153	difeq2i 3725	. . . . . . . . . . 11 |- ( X \ ( K ` D ) ) = ( X \ ( K ` ( X \ ( K ` B ) ) ) )
155	13, 14, 26, 27, 94	kur14lem2 31189	. . . . . . . . . . 11 |- ( I ` ( K ` B ) ) = ( X \ ( K ` ( X \ ( K ` B ) ) ) )
156	154, 155	eqtr4i 2647	. . . . . . . . . 10 |- ( X \ ( K ` D ) ) = ( I ` ( K ` B ) )
157		fvex 6201	. . . . . . . . . . . 12 |- ( I ` ( K ` B ) ) e. _V
158	157	tpid3 4307	. . . . . . . . . . 11 |- ( I ` ( K ` B ) ) e. { ( I ` C ) , ( K ` D ) , ( I ` ( K ` B ) ) }
159	117, 158	sselii 3600	. . . . . . . . . 10 |- ( I ` ( K ` B ) ) e. T
160	156, 159	eqeltri 2697	. . . . . . . . 9 |- ( X \ ( K ` D ) ) e. T
161	13, 14, 26, 27, 102	kur14lem5 31192	. . . . . . . . . 10 |- ( K ` ( K ` D ) ) = ( K ` D )
162	161, 120	eqeltri 2697	. . . . . . . . 9 |- ( K ` ( K ` D ) ) e. T
163	152, 160, 162	kur14lem1 31188	. . . . . . . 8 |- ( N = ( K ` D ) -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )
164		difss 3737	. . . . . . . . . 10 |- ( X \ ( K ` ( X \ ( K ` B ) ) ) ) C_ X
165	155, 164	eqsstri 3635	. . . . . . . . 9 |- ( I ` ( K ` B ) ) C_ X
166	156	difeq2i 3725	. . . . . . . . . . 11 |- ( X \ ( X \ ( K ` D ) ) ) = ( X \ ( I ` ( K ` B ) ) )
167	13, 14, 26, 27, 152	kur14lem4 31191	. . . . . . . . . . 11 |- ( X \ ( X \ ( K ` D ) ) ) = ( K ` D )
168	166, 167	eqtr3i 2646	. . . . . . . . . 10 |- ( X \ ( I ` ( K ` B ) ) ) = ( K ` D )
169	168, 120	eqeltri 2697	. . . . . . . . 9 |- ( X \ ( I ` ( K ` B ) ) ) e. T
170	13, 14, 26, 27, 5, 44	kur14lem6 31193	. . . . . . . . . 10 |- ( K ` ( I ` ( K ` B ) ) ) = ( K ` B )
171	170, 65	eqeltri 2697	. . . . . . . . 9 |- ( K ` ( I ` ( K ` B ) ) ) e. T
172	165, 169, 171	kur14lem1 31188	. . . . . . . 8 |- ( N = ( I ` ( K ` B ) ) -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )
173	151, 163, 172	3jaoi 1391	. . . . . . 7 |- ( ( N = ( I ` C ) \/ N = ( K ` D ) \/ N = ( I ` ( K ` B ) ) ) -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )
174	139, 173	syl 17	. . . . . 6 |- ( N e. { ( I ` C ) , ( K ` D ) , ( I ` ( K ` B ) ) } -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )
175		elpri 4197	. . . . . . 7 |- ( N e. { ( K ` ( I ` C ) ) , ( I ` ( K ` ( I ` A ) ) ) } -> ( N = ( K ` ( I ` C ) ) \/ N = ( I ` ( K ` ( I ` A ) ) ) ) )
176	13, 14, 26, 27, 141	kur14lem3 31190	. . . . . . . . 9 |- ( K ` ( I ` C ) ) C_ X
177	126	fveq2i 6194	. . . . . . . . . . . 12 |- ( K ` ( I ` C ) ) = ( K ` ( X \ ( K ` ( I ` A ) ) ) )
178	177	difeq2i 3725	. . . . . . . . . . 11 |- ( X \ ( K ` ( I ` C ) ) ) = ( X \ ( K ` ( X \ ( K ` ( I ` A ) ) ) ) )
179	13, 14, 26, 27, 122	kur14lem2 31189	. . . . . . . . . . 11 |- ( I ` ( K ` ( I ` A ) ) ) = ( X \ ( K ` ( X \ ( K ` ( I ` A ) ) ) ) )
180	178, 179	eqtr4i 2647	. . . . . . . . . 10 |- ( X \ ( K ` ( I ` C ) ) ) = ( I ` ( K ` ( I ` A ) ) )
181		fvex 6201	. . . . . . . . . . . 12 |- ( I ` ( K ` ( I ` A ) ) ) e. _V
182	181	prid2 4298	. . . . . . . . . . 11 |- ( I ` ( K ` ( I ` A ) ) ) e. { ( K ` ( I ` C ) ) , ( I ` ( K ` ( I ` A ) ) ) }
183	147, 182	sselii 3600	. . . . . . . . . 10 |- ( I ` ( K ` ( I ` A ) ) ) e. T
184	180, 183	eqeltri 2697	. . . . . . . . 9 |- ( X \ ( K ` ( I ` C ) ) ) e. T
185	13, 14, 26, 27, 141	kur14lem5 31192	. . . . . . . . . 10 |- ( K ` ( K ` ( I ` C ) ) ) = ( K ` ( I ` C ) )
186	185, 150	eqeltri 2697	. . . . . . . . 9 |- ( K ` ( K ` ( I ` C ) ) ) e. T
187	176, 184, 186	kur14lem1 31188	. . . . . . . 8 |- ( N = ( K ` ( I ` C ) ) -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )
188		difss 3737	. . . . . . . . . 10 |- ( X \ ( K ` ( X \ ( K ` ( I ` A ) ) ) ) ) C_ X
189	179, 188	eqsstri 3635	. . . . . . . . 9 |- ( I ` ( K ` ( I ` A ) ) ) C_ X
190	180	difeq2i 3725	. . . . . . . . . . 11 |- ( X \ ( X \ ( K ` ( I ` C ) ) ) ) = ( X \ ( I ` ( K ` ( I ` A ) ) ) )
191	13, 14, 26, 27, 176	kur14lem4 31191	. . . . . . . . . . 11 |- ( X \ ( X \ ( K ` ( I ` C ) ) ) ) = ( K ` ( I ` C ) )
192	190, 191	eqtr3i 2646	. . . . . . . . . 10 |- ( X \ ( I ` ( K ` ( I ` A ) ) ) ) = ( K ` ( I ` C ) )
193	192, 150	eqeltri 2697	. . . . . . . . 9 |- ( X \ ( I ` ( K ` ( I ` A ) ) ) ) e. T
194	13, 14, 26, 27, 18, 68	kur14lem6 31193	. . . . . . . . . 10 |- ( K ` ( I ` ( K ` ( I ` A ) ) ) ) = ( K ` ( I ` A ) )
195	194, 87	eqeltri 2697	. . . . . . . . 9 |- ( K ` ( I ` ( K ` ( I ` A ) ) ) ) e. T
196	189, 193, 195	kur14lem1 31188	. . . . . . . 8 |- ( N = ( I ` ( K ` ( I ` A ) ) ) -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )
197	187, 196	jaoi 394	. . . . . . 7 |- ( ( N = ( K ` ( I ` C ) ) \/ N = ( I ` ( K ` ( I ` A ) ) ) ) -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )
198	175, 197	syl 17	. . . . . 6 |- ( N e. { ( K ` ( I ` C ) ) , ( I ` ( K ` ( I ` A ) ) ) } -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )
199	174, 198	jaoi 394	. . . . 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 ) )
200	138, 199	sylbi 207	. . . 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 ) )
201	137, 200	jaoi 394	. . 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 ) )
202	1, 201	sylbi 207	. 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 ) )
203	202, 9	eleq2s 2719	1 |- ( N e. T -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )

Syntax hints:   -> wi 4   \/ wo 383   /\ wa 384   \/ w3o 1036   = wceq 1483   e. wcel 1990   \ cdif 3571   u. cun 3572   C_ wss 3574   {cpr 4179   {ctp 4181   U.cuni 4436   ` cfv 5888   Topctop 20698   intcnt 20821   clsccl 20822

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-top 20699  df-cld 20823  df-ntr 20824  df-cls 20825

This theorem is referenced by:  kur14lem9  31196