Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  kur14lem7 Structured version   Visualization version   GIF version

Theorem kur14lem7 31320
 Description: Lemma for kur14 31324: main proof. The set 𝑇 here contains all the distinct combinations of 𝑘 and 𝑐 that can arise, and we prove here that applying 𝑘 or 𝑐 to any element of 𝑇 yields another elemnt of 𝑇. In operator shorthand, we have 𝑇 = {𝐴, 𝑐𝐴, 𝑘𝐴 , 𝑐𝑘𝐴, 𝑘𝑐𝐴, 𝑐𝑘𝑐𝐴, 𝑘𝑐𝑘𝐴, 𝑐𝑘𝑐𝑘𝐴, 𝑘𝑐𝑘𝑐𝐴, 𝑐𝑘𝑐𝑘𝑐𝐴, 𝑘𝑐𝑘𝑐𝑘𝐴, 𝑐𝑘𝑐𝑘𝑐𝑘𝐴, 𝑘𝑐𝑘𝑐𝑘𝑐𝐴, 𝑐𝑘𝑐𝑘𝑐𝑘𝑐𝐴}. From the identities 𝑐𝑐𝐴 = 𝐴 and 𝑘𝑘𝐴 = 𝑘𝐴, 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 𝑘𝑐𝑘𝐴 = 𝑘𝑐𝑘𝑐𝑘𝑐𝑘𝐴, proved in kur14lem6 31319. (Contributed by Mario Carneiro, 11-Feb-2015.)
Hypotheses
Ref Expression
kur14lem.j 𝐽 ∈ Top
kur14lem.x 𝑋 = 𝐽
kur14lem.k 𝐾 = (cls‘𝐽)
kur14lem.i 𝐼 = (int‘𝐽)
kur14lem.a 𝐴𝑋
kur14lem.b 𝐵 = (𝑋 ∖ (𝐾𝐴))
kur14lem.c 𝐶 = (𝐾‘(𝑋𝐴))
kur14lem.d 𝐷 = (𝐼‘(𝐾𝐴))
kur14lem.t 𝑇 = ((({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}) ∪ ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))}))
Assertion
Ref Expression
kur14lem7 (𝑁𝑇 → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))

Proof of Theorem kur14lem7
StepHypRef Expression
1 elun 3786 . . 3 (𝑁 ∈ ((({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}) ∪ ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))})) ↔ (𝑁 ∈ (({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}) ∨ 𝑁 ∈ ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))})))
2 elun 3786 . . . . 5 (𝑁 ∈ (({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}) ↔ (𝑁 ∈ ({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∨ 𝑁 ∈ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}))
3 elun 3786 . . . . . . 7 (𝑁 ∈ ({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ↔ (𝑁 ∈ {𝐴, (𝑋𝐴), (𝐾𝐴)} ∨ 𝑁 ∈ {𝐵, 𝐶, (𝐼𝐴)}))
4 eltpi 4261 . . . . . . . . 9 (𝑁 ∈ {𝐴, (𝑋𝐴), (𝐾𝐴)} → (𝑁 = 𝐴𝑁 = (𝑋𝐴) ∨ 𝑁 = (𝐾𝐴)))
5 kur14lem.a . . . . . . . . . . 11 𝐴𝑋
6 ssun1 3809 . . . . . . . . . . . . 13 {𝐴, (𝑋𝐴), (𝐾𝐴)} ⊆ ({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)})
7 ssun1 3809 . . . . . . . . . . . . . 14 ({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ⊆ (({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))})
8 ssun1 3809 . . . . . . . . . . . . . . 15 (({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}) ⊆ ((({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}) ∪ ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))}))
9 kur14lem.t . . . . . . . . . . . . . . 15 𝑇 = ((({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}) ∪ ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))}))
108, 9sseqtr4i 3671 . . . . . . . . . . . . . 14 (({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}) ⊆ 𝑇
117, 10sstri 3645 . . . . . . . . . . . . 13 ({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ⊆ 𝑇
126, 11sstri 3645 . . . . . . . . . . . 12 {𝐴, (𝑋𝐴), (𝐾𝐴)} ⊆ 𝑇
13 kur14lem.j . . . . . . . . . . . . . . . 16 𝐽 ∈ Top
14 kur14lem.x . . . . . . . . . . . . . . . . 17 𝑋 = 𝐽
1514topopn 20759 . . . . . . . . . . . . . . . 16 (𝐽 ∈ Top → 𝑋𝐽)
1613, 15ax-mp 5 . . . . . . . . . . . . . . 15 𝑋𝐽
1716elexi 3244 . . . . . . . . . . . . . 14 𝑋 ∈ V
18 difss 3770 . . . . . . . . . . . . . 14 (𝑋𝐴) ⊆ 𝑋
1917, 18ssexi 4836 . . . . . . . . . . . . 13 (𝑋𝐴) ∈ V
2019tpid2 4336 . . . . . . . . . . . 12 (𝑋𝐴) ∈ {𝐴, (𝑋𝐴), (𝐾𝐴)}
2112, 20sselii 3633 . . . . . . . . . . 11 (𝑋𝐴) ∈ 𝑇
22 fvex 6239 . . . . . . . . . . . . 13 (𝐾𝐴) ∈ V
2322tpid3 4338 . . . . . . . . . . . 12 (𝐾𝐴) ∈ {𝐴, (𝑋𝐴), (𝐾𝐴)}
2412, 23sselii 3633 . . . . . . . . . . 11 (𝐾𝐴) ∈ 𝑇
255, 21, 24kur14lem1 31314 . . . . . . . . . 10 (𝑁 = 𝐴 → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
26 kur14lem.k . . . . . . . . . . . . 13 𝐾 = (cls‘𝐽)
27 kur14lem.i . . . . . . . . . . . . 13 𝐼 = (int‘𝐽)
2813, 14, 26, 27, 5kur14lem4 31317 . . . . . . . . . . . 12 (𝑋 ∖ (𝑋𝐴)) = 𝐴
2917, 5ssexi 4836 . . . . . . . . . . . . . 14 𝐴 ∈ V
3029tpid1 4335 . . . . . . . . . . . . 13 𝐴 ∈ {𝐴, (𝑋𝐴), (𝐾𝐴)}
3112, 30sselii 3633 . . . . . . . . . . . 12 𝐴𝑇
3228, 31eqeltri 2726 . . . . . . . . . . 11 (𝑋 ∖ (𝑋𝐴)) ∈ 𝑇
33 kur14lem.c . . . . . . . . . . . 12 𝐶 = (𝐾‘(𝑋𝐴))
34 ssun2 3810 . . . . . . . . . . . . . 14 {𝐵, 𝐶, (𝐼𝐴)} ⊆ ({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)})
3534, 11sstri 3645 . . . . . . . . . . . . 13 {𝐵, 𝐶, (𝐼𝐴)} ⊆ 𝑇
3613, 14, 26, 27, 18kur14lem3 31316 . . . . . . . . . . . . . . . 16 (𝐾‘(𝑋𝐴)) ⊆ 𝑋
3733, 36eqsstri 3668 . . . . . . . . . . . . . . 15 𝐶𝑋
3817, 37ssexi 4836 . . . . . . . . . . . . . 14 𝐶 ∈ V
3938tpid2 4336 . . . . . . . . . . . . 13 𝐶 ∈ {𝐵, 𝐶, (𝐼𝐴)}
4035, 39sselii 3633 . . . . . . . . . . . 12 𝐶𝑇
4133, 40eqeltrri 2727 . . . . . . . . . . 11 (𝐾‘(𝑋𝐴)) ∈ 𝑇
4218, 32, 41kur14lem1 31314 . . . . . . . . . 10 (𝑁 = (𝑋𝐴) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
4313, 14, 26, 27, 5kur14lem3 31316 . . . . . . . . . . 11 (𝐾𝐴) ⊆ 𝑋
44 kur14lem.b . . . . . . . . . . . 12 𝐵 = (𝑋 ∖ (𝐾𝐴))
45 difss 3770 . . . . . . . . . . . . . . . 16 (𝑋 ∖ (𝐾𝐴)) ⊆ 𝑋
4644, 45eqsstri 3668 . . . . . . . . . . . . . . 15 𝐵𝑋
4717, 46ssexi 4836 . . . . . . . . . . . . . 14 𝐵 ∈ V
4847tpid1 4335 . . . . . . . . . . . . 13 𝐵 ∈ {𝐵, 𝐶, (𝐼𝐴)}
4935, 48sselii 3633 . . . . . . . . . . . 12 𝐵𝑇
5044, 49eqeltrri 2727 . . . . . . . . . . 11 (𝑋 ∖ (𝐾𝐴)) ∈ 𝑇
5113, 14, 26, 27, 5kur14lem5 31318 . . . . . . . . . . . 12 (𝐾‘(𝐾𝐴)) = (𝐾𝐴)
5251, 24eqeltri 2726 . . . . . . . . . . 11 (𝐾‘(𝐾𝐴)) ∈ 𝑇
5343, 50, 52kur14lem1 31314 . . . . . . . . . 10 (𝑁 = (𝐾𝐴) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
5425, 42, 533jaoi 1431 . . . . . . . . 9 ((𝑁 = 𝐴𝑁 = (𝑋𝐴) ∨ 𝑁 = (𝐾𝐴)) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
554, 54syl 17 . . . . . . . 8 (𝑁 ∈ {𝐴, (𝑋𝐴), (𝐾𝐴)} → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
56 eltpi 4261 . . . . . . . . 9 (𝑁 ∈ {𝐵, 𝐶, (𝐼𝐴)} → (𝑁 = 𝐵𝑁 = 𝐶𝑁 = (𝐼𝐴)))
5744difeq2i 3758 . . . . . . . . . . . . 13 (𝑋𝐵) = (𝑋 ∖ (𝑋 ∖ (𝐾𝐴)))
5813, 14, 26, 27, 43kur14lem4 31317 . . . . . . . . . . . . 13 (𝑋 ∖ (𝑋 ∖ (𝐾𝐴))) = (𝐾𝐴)
5957, 58eqtri 2673 . . . . . . . . . . . 12 (𝑋𝐵) = (𝐾𝐴)
6059, 24eqeltri 2726 . . . . . . . . . . 11 (𝑋𝐵) ∈ 𝑇
61 ssun2 3810 . . . . . . . . . . . . 13 {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))} ⊆ (({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))})
6261, 10sstri 3645 . . . . . . . . . . . 12 {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))} ⊆ 𝑇
63 fvex 6239 . . . . . . . . . . . . 13 (𝐾𝐵) ∈ V
6463tpid1 4335 . . . . . . . . . . . 12 (𝐾𝐵) ∈ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}
6562, 64sselii 3633 . . . . . . . . . . 11 (𝐾𝐵) ∈ 𝑇
6646, 60, 65kur14lem1 31314 . . . . . . . . . 10 (𝑁 = 𝐵 → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
6733difeq2i 3758 . . . . . . . . . . . . 13 (𝑋𝐶) = (𝑋 ∖ (𝐾‘(𝑋𝐴)))
6813, 14, 26, 27, 5kur14lem2 31315 . . . . . . . . . . . . 13 (𝐼𝐴) = (𝑋 ∖ (𝐾‘(𝑋𝐴)))
6967, 68eqtr4i 2676 . . . . . . . . . . . 12 (𝑋𝐶) = (𝐼𝐴)
70 fvex 6239 . . . . . . . . . . . . . 14 (𝐼𝐴) ∈ V
7170tpid3 4338 . . . . . . . . . . . . 13 (𝐼𝐴) ∈ {𝐵, 𝐶, (𝐼𝐴)}
7235, 71sselii 3633 . . . . . . . . . . . 12 (𝐼𝐴) ∈ 𝑇
7369, 72eqeltri 2726 . . . . . . . . . . 11 (𝑋𝐶) ∈ 𝑇
7413, 14, 26, 27, 18kur14lem5 31318 . . . . . . . . . . . . 13 (𝐾‘(𝐾‘(𝑋𝐴))) = (𝐾‘(𝑋𝐴))
7533fveq2i 6232 . . . . . . . . . . . . 13 (𝐾𝐶) = (𝐾‘(𝐾‘(𝑋𝐴)))
7674, 75, 333eqtr4i 2683 . . . . . . . . . . . 12 (𝐾𝐶) = 𝐶
7776, 40eqeltri 2726 . . . . . . . . . . 11 (𝐾𝐶) ∈ 𝑇
7837, 73, 77kur14lem1 31314 . . . . . . . . . 10 (𝑁 = 𝐶 → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
79 difss 3770 . . . . . . . . . . . 12 (𝑋 ∖ (𝐾‘(𝑋𝐴))) ⊆ 𝑋
8068, 79eqsstri 3668 . . . . . . . . . . 11 (𝐼𝐴) ⊆ 𝑋
8169difeq2i 3758 . . . . . . . . . . . . 13 (𝑋 ∖ (𝑋𝐶)) = (𝑋 ∖ (𝐼𝐴))
8213, 14, 26, 27, 37kur14lem4 31317 . . . . . . . . . . . . 13 (𝑋 ∖ (𝑋𝐶)) = 𝐶
8381, 82eqtr3i 2675 . . . . . . . . . . . 12 (𝑋 ∖ (𝐼𝐴)) = 𝐶
8483, 40eqeltri 2726 . . . . . . . . . . 11 (𝑋 ∖ (𝐼𝐴)) ∈ 𝑇
85 fvex 6239 . . . . . . . . . . . . 13 (𝐾‘(𝐼𝐴)) ∈ V
8685tpid3 4338 . . . . . . . . . . . 12 (𝐾‘(𝐼𝐴)) ∈ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}
8762, 86sselii 3633 . . . . . . . . . . 11 (𝐾‘(𝐼𝐴)) ∈ 𝑇
8880, 84, 87kur14lem1 31314 . . . . . . . . . 10 (𝑁 = (𝐼𝐴) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
8966, 78, 883jaoi 1431 . . . . . . . . 9 ((𝑁 = 𝐵𝑁 = 𝐶𝑁 = (𝐼𝐴)) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
9056, 89syl 17 . . . . . . . 8 (𝑁 ∈ {𝐵, 𝐶, (𝐼𝐴)} → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
9155, 90jaoi 393 . . . . . . 7 ((𝑁 ∈ {𝐴, (𝑋𝐴), (𝐾𝐴)} ∨ 𝑁 ∈ {𝐵, 𝐶, (𝐼𝐴)}) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
923, 91sylbi 207 . . . . . 6 (𝑁 ∈ ({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
93 eltpi 4261 . . . . . . 7 (𝑁 ∈ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))} → (𝑁 = (𝐾𝐵) ∨ 𝑁 = 𝐷𝑁 = (𝐾‘(𝐼𝐴))))
9413, 14, 26, 27, 46kur14lem3 31316 . . . . . . . . 9 (𝐾𝐵) ⊆ 𝑋
9513, 14, 26, 27, 43kur14lem2 31315 . . . . . . . . . . 11 (𝐼‘(𝐾𝐴)) = (𝑋 ∖ (𝐾‘(𝑋 ∖ (𝐾𝐴))))
96 kur14lem.d . . . . . . . . . . 11 𝐷 = (𝐼‘(𝐾𝐴))
9744fveq2i 6232 . . . . . . . . . . . 12 (𝐾𝐵) = (𝐾‘(𝑋 ∖ (𝐾𝐴)))
9897difeq2i 3758 . . . . . . . . . . 11 (𝑋 ∖ (𝐾𝐵)) = (𝑋 ∖ (𝐾‘(𝑋 ∖ (𝐾𝐴))))
9995, 96, 983eqtr4i 2683 . . . . . . . . . 10 𝐷 = (𝑋 ∖ (𝐾𝐵))
10096, 95eqtri 2673 . . . . . . . . . . . . . 14 𝐷 = (𝑋 ∖ (𝐾‘(𝑋 ∖ (𝐾𝐴))))
101 difss 3770 . . . . . . . . . . . . . 14 (𝑋 ∖ (𝐾‘(𝑋 ∖ (𝐾𝐴)))) ⊆ 𝑋
102100, 101eqsstri 3668 . . . . . . . . . . . . 13 𝐷𝑋
10317, 102ssexi 4836 . . . . . . . . . . . 12 𝐷 ∈ V
104103tpid2 4336 . . . . . . . . . . 11 𝐷 ∈ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}
10562, 104sselii 3633 . . . . . . . . . 10 𝐷𝑇
10699, 105eqeltrri 2727 . . . . . . . . 9 (𝑋 ∖ (𝐾𝐵)) ∈ 𝑇
10713, 14, 26, 27, 46kur14lem5 31318 . . . . . . . . . 10 (𝐾‘(𝐾𝐵)) = (𝐾𝐵)
108107, 65eqeltri 2726 . . . . . . . . 9 (𝐾‘(𝐾𝐵)) ∈ 𝑇
10994, 106, 108kur14lem1 31314 . . . . . . . 8 (𝑁 = (𝐾𝐵) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
11099difeq2i 3758 . . . . . . . . . . 11 (𝑋𝐷) = (𝑋 ∖ (𝑋 ∖ (𝐾𝐵)))
11113, 14, 26, 27, 94kur14lem4 31317 . . . . . . . . . . 11 (𝑋 ∖ (𝑋 ∖ (𝐾𝐵))) = (𝐾𝐵)
112110, 111eqtri 2673 . . . . . . . . . 10 (𝑋𝐷) = (𝐾𝐵)
113112, 65eqeltri 2726 . . . . . . . . 9 (𝑋𝐷) ∈ 𝑇
114 ssun1 3809 . . . . . . . . . . 11 {(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ⊆ ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))})
115 ssun2 3810 . . . . . . . . . . . 12 ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))}) ⊆ ((({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}) ∪ ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))}))
116115, 9sseqtr4i 3671 . . . . . . . . . . 11 ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))}) ⊆ 𝑇
117114, 116sstri 3645 . . . . . . . . . 10 {(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ⊆ 𝑇
118 fvex 6239 . . . . . . . . . . 11 (𝐾𝐷) ∈ V
119118tpid2 4336 . . . . . . . . . 10 (𝐾𝐷) ∈ {(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))}
120117, 119sselii 3633 . . . . . . . . 9 (𝐾𝐷) ∈ 𝑇
121102, 113, 120kur14lem1 31314 . . . . . . . 8 (𝑁 = 𝐷 → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
12213, 14, 26, 27, 80kur14lem3 31316 . . . . . . . . 9 (𝐾‘(𝐼𝐴)) ⊆ 𝑋
12313, 14, 26, 27, 37kur14lem2 31315 . . . . . . . . . . 11 (𝐼𝐶) = (𝑋 ∖ (𝐾‘(𝑋𝐶)))
12469fveq2i 6232 . . . . . . . . . . . 12 (𝐾‘(𝑋𝐶)) = (𝐾‘(𝐼𝐴))
125124difeq2i 3758 . . . . . . . . . . 11 (𝑋 ∖ (𝐾‘(𝑋𝐶))) = (𝑋 ∖ (𝐾‘(𝐼𝐴)))
126123, 125eqtri 2673 . . . . . . . . . 10 (𝐼𝐶) = (𝑋 ∖ (𝐾‘(𝐼𝐴)))
127 fvex 6239 . . . . . . . . . . . 12 (𝐼𝐶) ∈ V
128127tpid1 4335 . . . . . . . . . . 11 (𝐼𝐶) ∈ {(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))}
129117, 128sselii 3633 . . . . . . . . . 10 (𝐼𝐶) ∈ 𝑇
130126, 129eqeltrri 2727 . . . . . . . . 9 (𝑋 ∖ (𝐾‘(𝐼𝐴))) ∈ 𝑇
13113, 14, 26, 27, 80kur14lem5 31318 . . . . . . . . . 10 (𝐾‘(𝐾‘(𝐼𝐴))) = (𝐾‘(𝐼𝐴))
132131, 87eqeltri 2726 . . . . . . . . 9 (𝐾‘(𝐾‘(𝐼𝐴))) ∈ 𝑇
133122, 130, 132kur14lem1 31314 . . . . . . . 8 (𝑁 = (𝐾‘(𝐼𝐴)) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
134109, 121, 1333jaoi 1431 . . . . . . 7 ((𝑁 = (𝐾𝐵) ∨ 𝑁 = 𝐷𝑁 = (𝐾‘(𝐼𝐴))) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
13593, 134syl 17 . . . . . 6 (𝑁 ∈ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))} → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
13692, 135jaoi 393 . . . . 5 ((𝑁 ∈ ({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∨ 𝑁 ∈ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
1372, 136sylbi 207 . . . 4 (𝑁 ∈ (({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
138 elun 3786 . . . . 5 (𝑁 ∈ ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))}) ↔ (𝑁 ∈ {(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∨ 𝑁 ∈ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))}))
139 eltpi 4261 . . . . . . 7 (𝑁 ∈ {(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} → (𝑁 = (𝐼𝐶) ∨ 𝑁 = (𝐾𝐷) ∨ 𝑁 = (𝐼‘(𝐾𝐵))))
140 difss 3770 . . . . . . . . . 10 (𝑋 ∖ (𝐾‘(𝑋𝐶))) ⊆ 𝑋
141123, 140eqsstri 3668 . . . . . . . . 9 (𝐼𝐶) ⊆ 𝑋
142126difeq2i 3758 . . . . . . . . . . 11 (𝑋 ∖ (𝐼𝐶)) = (𝑋 ∖ (𝑋 ∖ (𝐾‘(𝐼𝐴))))
14313, 14, 26, 27, 122kur14lem4 31317 . . . . . . . . . . 11 (𝑋 ∖ (𝑋 ∖ (𝐾‘(𝐼𝐴)))) = (𝐾‘(𝐼𝐴))
144142, 143eqtri 2673 . . . . . . . . . 10 (𝑋 ∖ (𝐼𝐶)) = (𝐾‘(𝐼𝐴))
145144, 87eqeltri 2726 . . . . . . . . 9 (𝑋 ∖ (𝐼𝐶)) ∈ 𝑇
146 ssun2 3810 . . . . . . . . . . 11 {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))} ⊆ ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))})
147146, 116sstri 3645 . . . . . . . . . 10 {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))} ⊆ 𝑇
148 fvex 6239 . . . . . . . . . . 11 (𝐾‘(𝐼𝐶)) ∈ V
149148prid1 4329 . . . . . . . . . 10 (𝐾‘(𝐼𝐶)) ∈ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))}
150147, 149sselii 3633 . . . . . . . . 9 (𝐾‘(𝐼𝐶)) ∈ 𝑇
151141, 145, 150kur14lem1 31314 . . . . . . . 8 (𝑁 = (𝐼𝐶) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
15213, 14, 26, 27, 102kur14lem3 31316 . . . . . . . . 9 (𝐾𝐷) ⊆ 𝑋
15399fveq2i 6232 . . . . . . . . . . . 12 (𝐾𝐷) = (𝐾‘(𝑋 ∖ (𝐾𝐵)))
154153difeq2i 3758 . . . . . . . . . . 11 (𝑋 ∖ (𝐾𝐷)) = (𝑋 ∖ (𝐾‘(𝑋 ∖ (𝐾𝐵))))
15513, 14, 26, 27, 94kur14lem2 31315 . . . . . . . . . . 11 (𝐼‘(𝐾𝐵)) = (𝑋 ∖ (𝐾‘(𝑋 ∖ (𝐾𝐵))))
156154, 155eqtr4i 2676 . . . . . . . . . 10 (𝑋 ∖ (𝐾𝐷)) = (𝐼‘(𝐾𝐵))
157 fvex 6239 . . . . . . . . . . . 12 (𝐼‘(𝐾𝐵)) ∈ V
158157tpid3 4338 . . . . . . . . . . 11 (𝐼‘(𝐾𝐵)) ∈ {(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))}
159117, 158sselii 3633 . . . . . . . . . 10 (𝐼‘(𝐾𝐵)) ∈ 𝑇
160156, 159eqeltri 2726 . . . . . . . . 9 (𝑋 ∖ (𝐾𝐷)) ∈ 𝑇
16113, 14, 26, 27, 102kur14lem5 31318 . . . . . . . . . 10 (𝐾‘(𝐾𝐷)) = (𝐾𝐷)
162161, 120eqeltri 2726 . . . . . . . . 9 (𝐾‘(𝐾𝐷)) ∈ 𝑇
163152, 160, 162kur14lem1 31314 . . . . . . . 8 (𝑁 = (𝐾𝐷) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
164 difss 3770 . . . . . . . . . 10 (𝑋 ∖ (𝐾‘(𝑋 ∖ (𝐾𝐵)))) ⊆ 𝑋
165155, 164eqsstri 3668 . . . . . . . . 9 (𝐼‘(𝐾𝐵)) ⊆ 𝑋
166156difeq2i 3758 . . . . . . . . . . 11 (𝑋 ∖ (𝑋 ∖ (𝐾𝐷))) = (𝑋 ∖ (𝐼‘(𝐾𝐵)))
16713, 14, 26, 27, 152kur14lem4 31317 . . . . . . . . . . 11 (𝑋 ∖ (𝑋 ∖ (𝐾𝐷))) = (𝐾𝐷)
168166, 167eqtr3i 2675 . . . . . . . . . 10 (𝑋 ∖ (𝐼‘(𝐾𝐵))) = (𝐾𝐷)
169168, 120eqeltri 2726 . . . . . . . . 9 (𝑋 ∖ (𝐼‘(𝐾𝐵))) ∈ 𝑇
17013, 14, 26, 27, 5, 44kur14lem6 31319 . . . . . . . . . 10 (𝐾‘(𝐼‘(𝐾𝐵))) = (𝐾𝐵)
171170, 65eqeltri 2726 . . . . . . . . 9 (𝐾‘(𝐼‘(𝐾𝐵))) ∈ 𝑇
172165, 169, 171kur14lem1 31314 . . . . . . . 8 (𝑁 = (𝐼‘(𝐾𝐵)) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
173151, 163, 1723jaoi 1431 . . . . . . 7 ((𝑁 = (𝐼𝐶) ∨ 𝑁 = (𝐾𝐷) ∨ 𝑁 = (𝐼‘(𝐾𝐵))) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
174139, 173syl 17 . . . . . 6 (𝑁 ∈ {(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
175 elpri 4230 . . . . . . 7 (𝑁 ∈ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))} → (𝑁 = (𝐾‘(𝐼𝐶)) ∨ 𝑁 = (𝐼‘(𝐾‘(𝐼𝐴)))))
17613, 14, 26, 27, 141kur14lem3 31316 . . . . . . . . 9 (𝐾‘(𝐼𝐶)) ⊆ 𝑋
177126fveq2i 6232 . . . . . . . . . . . 12 (𝐾‘(𝐼𝐶)) = (𝐾‘(𝑋 ∖ (𝐾‘(𝐼𝐴))))
178177difeq2i 3758 . . . . . . . . . . 11 (𝑋 ∖ (𝐾‘(𝐼𝐶))) = (𝑋 ∖ (𝐾‘(𝑋 ∖ (𝐾‘(𝐼𝐴)))))
17913, 14, 26, 27, 122kur14lem2 31315 . . . . . . . . . . 11 (𝐼‘(𝐾‘(𝐼𝐴))) = (𝑋 ∖ (𝐾‘(𝑋 ∖ (𝐾‘(𝐼𝐴)))))
180178, 179eqtr4i 2676 . . . . . . . . . 10 (𝑋 ∖ (𝐾‘(𝐼𝐶))) = (𝐼‘(𝐾‘(𝐼𝐴)))
181 fvex 6239 . . . . . . . . . . . 12 (𝐼‘(𝐾‘(𝐼𝐴))) ∈ V
182181prid2 4330 . . . . . . . . . . 11 (𝐼‘(𝐾‘(𝐼𝐴))) ∈ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))}
183147, 182sselii 3633 . . . . . . . . . 10 (𝐼‘(𝐾‘(𝐼𝐴))) ∈ 𝑇
184180, 183eqeltri 2726 . . . . . . . . 9 (𝑋 ∖ (𝐾‘(𝐼𝐶))) ∈ 𝑇
18513, 14, 26, 27, 141kur14lem5 31318 . . . . . . . . . 10 (𝐾‘(𝐾‘(𝐼𝐶))) = (𝐾‘(𝐼𝐶))
186185, 150eqeltri 2726 . . . . . . . . 9 (𝐾‘(𝐾‘(𝐼𝐶))) ∈ 𝑇
187176, 184, 186kur14lem1 31314 . . . . . . . 8 (𝑁 = (𝐾‘(𝐼𝐶)) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
188 difss 3770 . . . . . . . . . 10 (𝑋 ∖ (𝐾‘(𝑋 ∖ (𝐾‘(𝐼𝐴))))) ⊆ 𝑋
189179, 188eqsstri 3668 . . . . . . . . 9 (𝐼‘(𝐾‘(𝐼𝐴))) ⊆ 𝑋
190180difeq2i 3758 . . . . . . . . . . 11 (𝑋 ∖ (𝑋 ∖ (𝐾‘(𝐼𝐶)))) = (𝑋 ∖ (𝐼‘(𝐾‘(𝐼𝐴))))
19113, 14, 26, 27, 176kur14lem4 31317 . . . . . . . . . . 11 (𝑋 ∖ (𝑋 ∖ (𝐾‘(𝐼𝐶)))) = (𝐾‘(𝐼𝐶))
192190, 191eqtr3i 2675 . . . . . . . . . 10 (𝑋 ∖ (𝐼‘(𝐾‘(𝐼𝐴)))) = (𝐾‘(𝐼𝐶))
193192, 150eqeltri 2726 . . . . . . . . 9 (𝑋 ∖ (𝐼‘(𝐾‘(𝐼𝐴)))) ∈ 𝑇
19413, 14, 26, 27, 18, 68kur14lem6 31319 . . . . . . . . . 10 (𝐾‘(𝐼‘(𝐾‘(𝐼𝐴)))) = (𝐾‘(𝐼𝐴))
195194, 87eqeltri 2726 . . . . . . . . 9 (𝐾‘(𝐼‘(𝐾‘(𝐼𝐴)))) ∈ 𝑇
196189, 193, 195kur14lem1 31314 . . . . . . . 8 (𝑁 = (𝐼‘(𝐾‘(𝐼𝐴))) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
197187, 196jaoi 393 . . . . . . 7 ((𝑁 = (𝐾‘(𝐼𝐶)) ∨ 𝑁 = (𝐼‘(𝐾‘(𝐼𝐴)))) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
198175, 197syl 17 . . . . . 6 (𝑁 ∈ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))} → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
199174, 198jaoi 393 . . . . 5 ((𝑁 ∈ {(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∨ 𝑁 ∈ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))}) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
200138, 199sylbi 207 . . . 4 (𝑁 ∈ ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))}) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
201137, 200jaoi 393 . . 3 ((𝑁 ∈ (({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}) ∨ 𝑁 ∈ ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))})) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
2021, 201sylbi 207 . 2 (𝑁 ∈ ((({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}) ∪ ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))})) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
203202, 9eleq2s 2748 1 (𝑁𝑇 → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 382   ∧ wa 383   ∨ w3o 1053   = wceq 1523   ∈ wcel 2030   ∖ cdif 3604   ∪ cun 3605   ⊆ wss 3607  {cpr 4212  {ctp 4214  ∪ cuni 4468  ‘cfv 5926  Topctop 20746  intcnt 20869  clsccl 20870 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-top 20747  df-cld 20871  df-ntr 20872  df-cls 20873 This theorem is referenced by:  kur14lem9  31322
 Copyright terms: Public domain W3C validator