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 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 . (Contributed by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Hypotheses	kur14lem.j	$$⊢J\in \mathrm{Top}$$
	kur14lem.x	$$⊢X=\bigcup J$$
	kur14lem.k	$$⊢K=\mathrm{cls}\left(J\right)$$
	kur14lem.i	$$⊢I=\mathrm{int}\left(J\right)$$
	kur14lem.a	$$⊢A\subseteq X$$
	kur14lem.b	$$⊢B=X\setminus K\left(A\right)$$
	kur14lem.c	$$⊢C=K\left(X\setminus A\right)$$
	kur14lem.d	$$⊢D=I\left(K\left(A\right)\right)$$
	kur14lem.t	$$⊢T=\left(\left(\left\{A,X\setminus A,K\left(A\right)\right\}\cup \left\{B,C,I\left(A\right)\right\}\right)\cup \left\{K\left(B\right),D,K\left(I\left(A\right)\right)\right\}\right)\cup \left(\left\{I\left(C\right),K\left(D\right),I\left(K\left(B\right)\right)\right\}\cup \left\{K\left(I\left(C\right)\right),I\left(K\left(I\left(A\right)\right)\right)\right\}\right)$$
Assertion	kur14lem7	$$⊢N\in T\to \left(N\subseteq X\wedge \left\{X\setminus N,K\left(N\right)\right\}\subseteq T\right)$$

Proof

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