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	⊢ 𝐽 ∈ Top
	kur14lem.x	⊢ 𝑋 = ∪ 𝐽
	kur14lem.k	⊢ 𝐾 = ( cls ‘ 𝐽 )
	kur14lem.i	⊢ 𝐼 = ( int ‘ 𝐽 )
	kur14lem.a	⊢ 𝐴 ⊆ 𝑋
	kur14lem.b	⊢ 𝐵 = ( 𝑋 ∖ ( 𝐾 ‘ 𝐴 ) )
	kur14lem.c	⊢ 𝐶 = ( 𝐾 ‘ ( 𝑋 ∖ 𝐴 ) )
	kur14lem.d	⊢ 𝐷 = ( 𝐼 ‘ ( 𝐾 ‘ 𝐴 ) )
	kur14lem.t	⊢ 𝑇 = ( ( ( { 𝐴 , ( 𝑋 ∖ 𝐴 ) , ( 𝐾 ‘ 𝐴 ) } ∪ { 𝐵 , 𝐶 , ( 𝐼 ‘ 𝐴 ) } ) ∪ { ( 𝐾 ‘ 𝐵 ) , 𝐷 , ( 𝐾 ‘ ( 𝐼 ‘ 𝐴 ) ) } ) ∪ ( { ( 𝐼 ‘ 𝐶 ) , ( 𝐾 ‘ 𝐷 ) , ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) } ∪ { ( 𝐾 ‘ ( 𝐼 ‘ 𝐶 ) ) , ( 𝐼 ‘ ( 𝐾 ‘ ( 𝐼 ‘ 𝐴 ) ) ) } ) )
Assertion	kur14lem7	⊢ ( 𝑁 ∈ 𝑇 → ( 𝑁 ⊆ 𝑋 ∧ { ( 𝑋 ∖ 𝑁 ) , ( 𝐾 ‘ 𝑁 ) } ⊆ 𝑇 ) )

Proof

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