Theorem kur14lem7

Description: Lemma for kur14 : 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 element 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 . (Contributed by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Hypotheses	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	kur14lem7	|- ( N e. T -> ( N C_ X /\ { ( X \ N ) , ( K ` N ) } C_ T ) )

Proof

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