Metamath Proof Explorer

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 ∈ Top
kur14lem.x ⊢ X = ⋃ J
kur14lem.k ⊢ K = cls ⁡ J
kur14lem.i ⊢ I = int ⁡ J
kur14lem.a ⊢ A ⊆ 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 ∪ B C I ⁡ A ∪ K ⁡ B D K ⁡ I ⁡ A ∪ I ⁡ C K ⁡ D I ⁡ K ⁡ B ∪ K ⁡ I ⁡ C I ⁡ K ⁡ I ⁡ A
Assertion kur14lem7 ⊢ N ∈ T → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T

Proof

Step Hyp Ref Expression
1 kur14lem.j ⊢ J ∈ Top
2 kur14lem.x ⊢ X = ⋃ J
3 kur14lem.k ⊢ K = cls ⁡ J
4 kur14lem.i ⊢ I = int ⁡ J
5 kur14lem.a ⊢ A ⊆ 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 ∪ B C I ⁡ A ∪ K ⁡ B D K ⁡ I ⁡ A ∪ I ⁡ C K ⁡ D I ⁡ K ⁡ B ∪ K ⁡ I ⁡ C I ⁡ K ⁡ I ⁡ A
10 elun ⊢ N ∈ A X ∖ A K ⁡ A ∪ B C I ⁡ A ∪ K ⁡ B D K ⁡ I ⁡ A ∪ I ⁡ C K ⁡ D I ⁡ K ⁡ B ∪ K ⁡ I ⁡ C I ⁡ K ⁡ I ⁡ A ↔ N ∈ A X ∖ A K ⁡ A ∪ B C I ⁡ A ∪ K ⁡ B D K ⁡ I ⁡ A ∨ N ∈ I ⁡ C K ⁡ D I ⁡ K ⁡ B ∪ K ⁡ I ⁡ C I ⁡ K ⁡ I ⁡ A
11 elun ⊢ N ∈ A X ∖ A K ⁡ A ∪ B C I ⁡ A ∪ K ⁡ B D K ⁡ I ⁡ A ↔ N ∈ A X ∖ A K ⁡ A ∪ B C I ⁡ A ∨ N ∈ K ⁡ B D K ⁡ I ⁡ A
12 elun ⊢ N ∈ A X ∖ A K ⁡ A ∪ B C I ⁡ A ↔ N ∈ A X ∖ A K ⁡ A ∨ N ∈ B C I ⁡ A
13 eltpi ⊢ N ∈ A X ∖ A K ⁡ A → N = A ∨ N = X ∖ A ∨ N = K ⁡ A
14 ssun1 ⊢ A X ∖ A K ⁡ A ⊆ A X ∖ A K ⁡ A ∪ B C I ⁡ A
15 ssun1 ⊢ A X ∖ A K ⁡ A ∪ B C I ⁡ A ⊆ A X ∖ A K ⁡ A ∪ B C I ⁡ A ∪ K ⁡ B D K ⁡ I ⁡ A
16 ssun1 ⊢ A X ∖ A K ⁡ A ∪ B C I ⁡ A ∪ K ⁡ B D K ⁡ I ⁡ A ⊆ A X ∖ A K ⁡ A ∪ B C I ⁡ A ∪ K ⁡ B D K ⁡ I ⁡ A ∪ I ⁡ C K ⁡ D I ⁡ K ⁡ B ∪ K ⁡ I ⁡ C I ⁡ K ⁡ I ⁡ A
17 16 9 sseqtrri ⊢ A X ∖ A K ⁡ A ∪ B C I ⁡ A ∪ K ⁡ B D K ⁡ I ⁡ A ⊆ T
18 15 17 sstri ⊢ A X ∖ A K ⁡ A ∪ B C I ⁡ A ⊆ T
19 14 18 sstri ⊢ A X ∖ A K ⁡ A ⊆ T
20 2 topopn ⊢ J ∈ Top → X ∈ J
21 1 20 ax-mp ⊢ X ∈ J
22 21 elexi ⊢ X ∈ V
23 difss ⊢ X ∖ A ⊆ X
24 22 23 ssexi ⊢ X ∖ A ∈ V
25 24 tpid2 ⊢ X ∖ A ∈ A X ∖ A K ⁡ A
26 19 25 sselii ⊢ X ∖ A ∈ T
27 fvex ⊢ K ⁡ A ∈ V
28 27 tpid3 ⊢ K ⁡ A ∈ A X ∖ A K ⁡ A
29 19 28 sselii ⊢ K ⁡ A ∈ T
30 5 26 29 kur14lem1 ⊢ N = A → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
31 1 2 3 4 5 kur14lem4 ⊢ X ∖ X ∖ A = A
32 22 5 ssexi ⊢ A ∈ V
33 32 tpid1 ⊢ A ∈ A X ∖ A K ⁡ A
34 19 33 sselii ⊢ A ∈ T
35 31 34 eqeltri ⊢ X ∖ X ∖ A ∈ T
36 ssun2 ⊢ B C I ⁡ A ⊆ A X ∖ A K ⁡ A ∪ B C I ⁡ A
37 36 18 sstri ⊢ B C I ⁡ A ⊆ T
38 1 2 3 4 23 kur14lem3 ⊢ K ⁡ X ∖ A ⊆ X
39 7 38 eqsstri ⊢ C ⊆ X
40 22 39 ssexi ⊢ C ∈ V
41 40 tpid2 ⊢ C ∈ B C I ⁡ A
42 37 41 sselii ⊢ C ∈ T
43 7 42 eqeltrri ⊢ K ⁡ X ∖ A ∈ T
44 23 35 43 kur14lem1 ⊢ N = X ∖ A → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
45 1 2 3 4 5 kur14lem3 ⊢ K ⁡ A ⊆ X
46 difss ⊢ X ∖ K ⁡ A ⊆ X
47 6 46 eqsstri ⊢ B ⊆ X
48 22 47 ssexi ⊢ B ∈ V
49 48 tpid1 ⊢ B ∈ B C I ⁡ A
50 37 49 sselii ⊢ B ∈ T
51 6 50 eqeltrri ⊢ X ∖ K ⁡ A ∈ T
52 1 2 3 4 5 kur14lem5 ⊢ K ⁡ K ⁡ A = K ⁡ A
53 52 29 eqeltri ⊢ K ⁡ K ⁡ A ∈ T
54 45 51 53 kur14lem1 ⊢ N = K ⁡ A → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
55 30 44 54 3jaoi ⊢ N = A ∨ N = X ∖ A ∨ N = K ⁡ A → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
56 13 55 syl ⊢ N ∈ A X ∖ A K ⁡ A → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
57 eltpi ⊢ N ∈ 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 ∈ T
62 ssun2 ⊢ K ⁡ B D K ⁡ I ⁡ A ⊆ A X ∖ A K ⁡ A ∪ B C I ⁡ A ∪ K ⁡ B D K ⁡ I ⁡ A
63 62 17 sstri ⊢ K ⁡ B D K ⁡ I ⁡ A ⊆ T
64 fvex ⊢ K ⁡ B ∈ V
65 64 tpid1 ⊢ K ⁡ B ∈ K ⁡ B D K ⁡ I ⁡ A
66 63 65 sselii ⊢ K ⁡ B ∈ T
67 47 61 66 kur14lem1 ⊢ N = B → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ 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 ∈ V
72 71 tpid3 ⊢ I ⁡ A ∈ B C I ⁡ A
73 37 72 sselii ⊢ I ⁡ A ∈ T
74 70 73 eqeltri ⊢ X ∖ C ∈ 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 ∈ T
79 39 74 78 kur14lem1 ⊢ N = C → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
80 difss ⊢ X ∖ K ⁡ X ∖ A ⊆ X
81 69 80 eqsstri ⊢ I ⁡ A ⊆ 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 ∈ T
86 fvex ⊢ K ⁡ I ⁡ A ∈ V
87 86 tpid3 ⊢ K ⁡ I ⁡ A ∈ K ⁡ B D K ⁡ I ⁡ A
88 63 87 sselii ⊢ K ⁡ I ⁡ A ∈ T
89 81 85 88 kur14lem1 ⊢ N = I ⁡ A → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
90 67 79 89 3jaoi ⊢ N = B ∨ N = C ∨ N = I ⁡ A → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
91 57 90 syl ⊢ N ∈ B C I ⁡ A → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
92 56 91 jaoi ⊢ N ∈ A X ∖ A K ⁡ A ∨ N ∈ B C I ⁡ A → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
93 12 92 sylbi ⊢ N ∈ A X ∖ A K ⁡ A ∪ B C I ⁡ A → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
94 eltpi ⊢ N ∈ K ⁡ B D K ⁡ I ⁡ A → N = K ⁡ B ∨ N = D ∨ N = K ⁡ I ⁡ A
95 1 2 3 4 47 kur14lem3 ⊢ K ⁡ B ⊆ 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 ⊆ X
102 100 101 eqsstri ⊢ D ⊆ X
103 22 102 ssexi ⊢ D ∈ V
104 103 tpid2 ⊢ D ∈ K ⁡ B D K ⁡ I ⁡ A
105 63 104 sselii ⊢ D ∈ T
106 99 105 eqeltrri ⊢ X ∖ K ⁡ B ∈ T
107 1 2 3 4 47 kur14lem5 ⊢ K ⁡ K ⁡ B = K ⁡ B
108 107 66 eqeltri ⊢ K ⁡ K ⁡ B ∈ T
109 95 106 108 kur14lem1 ⊢ N = K ⁡ B → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ 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 ∈ T
114 ssun1 ⊢ I ⁡ C K ⁡ D I ⁡ K ⁡ B ⊆ I ⁡ C K ⁡ D I ⁡ K ⁡ B ∪ K ⁡ I ⁡ C I ⁡ K ⁡ I ⁡ A
115 ssun2 ⊢ I ⁡ C K ⁡ D I ⁡ K ⁡ B ∪ K ⁡ I ⁡ C I ⁡ K ⁡ I ⁡ A ⊆ A X ∖ A K ⁡ A ∪ B C I ⁡ A ∪ K ⁡ B D K ⁡ I ⁡ A ∪ I ⁡ C K ⁡ D I ⁡ K ⁡ B ∪ K ⁡ I ⁡ C I ⁡ K ⁡ I ⁡ A
116 115 9 sseqtrri ⊢ I ⁡ C K ⁡ D I ⁡ K ⁡ B ∪ K ⁡ I ⁡ C I ⁡ K ⁡ I ⁡ A ⊆ T
117 114 116 sstri ⊢ I ⁡ C K ⁡ D I ⁡ K ⁡ B ⊆ T
118 fvex ⊢ K ⁡ D ∈ V
119 118 tpid2 ⊢ K ⁡ D ∈ I ⁡ C K ⁡ D I ⁡ K ⁡ B
120 117 119 sselii ⊢ K ⁡ D ∈ T
121 102 113 120 kur14lem1 ⊢ N = D → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
122 1 2 3 4 81 kur14lem3 ⊢ K ⁡ I ⁡ A ⊆ 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 ∈ V
128 127 tpid1 ⊢ I ⁡ C ∈ I ⁡ C K ⁡ D I ⁡ K ⁡ B
129 117 128 sselii ⊢ I ⁡ C ∈ T
130 126 129 eqeltrri ⊢ X ∖ K ⁡ I ⁡ A ∈ T
131 1 2 3 4 81 kur14lem5 ⊢ K ⁡ K ⁡ I ⁡ A = K ⁡ I ⁡ A
132 131 88 eqeltri ⊢ K ⁡ K ⁡ I ⁡ A ∈ T
133 122 130 132 kur14lem1 ⊢ N = K ⁡ I ⁡ A → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
134 109 121 133 3jaoi ⊢ N = K ⁡ B ∨ N = D ∨ N = K ⁡ I ⁡ A → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
135 94 134 syl ⊢ N ∈ K ⁡ B D K ⁡ I ⁡ A → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
136 93 135 jaoi ⊢ N ∈ A X ∖ A K ⁡ A ∪ B C I ⁡ A ∨ N ∈ K ⁡ B D K ⁡ I ⁡ A → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
137 11 136 sylbi ⊢ N ∈ A X ∖ A K ⁡ A ∪ B C I ⁡ A ∪ K ⁡ B D K ⁡ I ⁡ A → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
138 elun ⊢ N ∈ I ⁡ C K ⁡ D I ⁡ K ⁡ B ∪ K ⁡ I ⁡ C I ⁡ K ⁡ I ⁡ A ↔ N ∈ I ⁡ C K ⁡ D I ⁡ K ⁡ B ∨ N ∈ K ⁡ I ⁡ C I ⁡ K ⁡ I ⁡ A
139 eltpi ⊢ N ∈ I ⁡ C K ⁡ D I ⁡ K ⁡ B → N = I ⁡ C ∨ N = K ⁡ D ∨ N = I ⁡ K ⁡ B
140 difss ⊢ X ∖ K ⁡ X ∖ C ⊆ X
141 123 140 eqsstri ⊢ I ⁡ 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 ∈ T
146 ssun2 ⊢ K ⁡ I ⁡ C I ⁡ K ⁡ I ⁡ A ⊆ I ⁡ C K ⁡ D I ⁡ K ⁡ B ∪ K ⁡ I ⁡ C I ⁡ K ⁡ I ⁡ A
147 146 116 sstri ⊢ K ⁡ I ⁡ C I ⁡ K ⁡ I ⁡ A ⊆ T
148 fvex ⊢ K ⁡ I ⁡ C ∈ V
149 148 prid1 ⊢ K ⁡ I ⁡ C ∈ K ⁡ I ⁡ C I ⁡ K ⁡ I ⁡ A
150 147 149 sselii ⊢ K ⁡ I ⁡ C ∈ T
151 141 145 150 kur14lem1 ⊢ N = I ⁡ C → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
152 1 2 3 4 102 kur14lem3 ⊢ K ⁡ D ⊆ 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 ∈ V
158 157 tpid3 ⊢ I ⁡ K ⁡ B ∈ I ⁡ C K ⁡ D I ⁡ K ⁡ B
159 117 158 sselii ⊢ I ⁡ K ⁡ B ∈ T
160 156 159 eqeltri ⊢ X ∖ K ⁡ D ∈ T
161 1 2 3 4 102 kur14lem5 ⊢ K ⁡ K ⁡ D = K ⁡ D
162 161 120 eqeltri ⊢ K ⁡ K ⁡ D ∈ T
163 152 160 162 kur14lem1 ⊢ N = K ⁡ D → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
164 difss ⊢ X ∖ K ⁡ X ∖ K ⁡ B ⊆ X
165 155 164 eqsstri ⊢ I ⁡ K ⁡ B ⊆ 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 ∈ T
170 1 2 3 4 5 6 kur14lem6 ⊢ K ⁡ I ⁡ K ⁡ B = K ⁡ B
171 170 66 eqeltri ⊢ K ⁡ I ⁡ K ⁡ B ∈ T
172 165 169 171 kur14lem1 ⊢ N = I ⁡ K ⁡ B → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
173 151 163 172 3jaoi ⊢ N = I ⁡ C ∨ N = K ⁡ D ∨ N = I ⁡ K ⁡ B → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
174 139 173 syl ⊢ N ∈ I ⁡ C K ⁡ D I ⁡ K ⁡ B → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
175 elpri ⊢ N ∈ 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 ⊆ 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 ∈ V
182 181 prid2 ⊢ I ⁡ K ⁡ I ⁡ A ∈ K ⁡ I ⁡ C I ⁡ K ⁡ I ⁡ A
183 147 182 sselii ⊢ I ⁡ K ⁡ I ⁡ A ∈ T
184 180 183 eqeltri ⊢ X ∖ K ⁡ I ⁡ C ∈ T
185 1 2 3 4 141 kur14lem5 ⊢ K ⁡ K ⁡ I ⁡ C = K ⁡ I ⁡ C
186 185 150 eqeltri ⊢ K ⁡ K ⁡ I ⁡ C ∈ T
187 176 184 186 kur14lem1 ⊢ N = K ⁡ I ⁡ C → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
188 difss ⊢ X ∖ K ⁡ X ∖ K ⁡ I ⁡ A ⊆ X
189 179 188 eqsstri ⊢ I ⁡ K ⁡ I ⁡ A ⊆ 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 ∈ 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 ∈ T
196 189 193 195 kur14lem1 ⊢ N = I ⁡ K ⁡ I ⁡ A → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
197 187 196 jaoi ⊢ N = K ⁡ I ⁡ C ∨ N = I ⁡ K ⁡ I ⁡ A → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
198 175 197 syl ⊢ N ∈ K ⁡ I ⁡ C I ⁡ K ⁡ I ⁡ A → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
199 174 198 jaoi ⊢ N ∈ I ⁡ C K ⁡ D I ⁡ K ⁡ B ∨ N ∈ K ⁡ I ⁡ C I ⁡ K ⁡ I ⁡ A → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
200 138 199 sylbi ⊢ N ∈ I ⁡ C K ⁡ D I ⁡ K ⁡ B ∪ K ⁡ I ⁡ C I ⁡ K ⁡ I ⁡ A → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
201 137 200 jaoi ⊢ N ∈ A X ∖ A K ⁡ A ∪ B C I ⁡ A ∪ K ⁡ B D K ⁡ I ⁡ A ∨ N ∈ I ⁡ C K ⁡ D I ⁡ K ⁡ B ∪ K ⁡ I ⁡ C I ⁡ K ⁡ I ⁡ A → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
202 10 201 sylbi ⊢ N ∈ A X ∖ A K ⁡ A ∪ B C I ⁡ A ∪ K ⁡ B D K ⁡ I ⁡ A ∪ I ⁡ C K ⁡ D I ⁡ K ⁡ B ∪ K ⁡ I ⁡ C I ⁡ K ⁡ I ⁡ A → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T
203 202 9 eleq2s ⊢ N ∈ T → N ⊆ X ∧ X ∖ N K ⁡ N ⊆ T