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

Theorem kur14lem7 31514
Description: Lemma for kur14 31518: 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 31513. (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 3949 . . 3 (𝑁 ∈ ((({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}) ∪ ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))})) ↔ (𝑁 ∈ (({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}) ∨ 𝑁 ∈ ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))})))
2 elun 3949 . . . . 5 (𝑁 ∈ (({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}) ↔ (𝑁 ∈ ({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∨ 𝑁 ∈ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}))
3 elun 3949 . . . . . . 7 (𝑁 ∈ ({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ↔ (𝑁 ∈ {𝐴, (𝑋𝐴), (𝐾𝐴)} ∨ 𝑁 ∈ {𝐵, 𝐶, (𝐼𝐴)}))
4 eltpi 4418 . . . . . . . . 9 (𝑁 ∈ {𝐴, (𝑋𝐴), (𝐾𝐴)} → (𝑁 = 𝐴𝑁 = (𝑋𝐴) ∨ 𝑁 = (𝐾𝐴)))
5 kur14lem.a . . . . . . . . . . 11 𝐴𝑋
6 ssun1 3972 . . . . . . . . . . . . 13 {𝐴, (𝑋𝐴), (𝐾𝐴)} ⊆ ({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)})
7 ssun1 3972 . . . . . . . . . . . . . 14 ({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ⊆ (({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))})
8 ssun1 3972 . . . . . . . . . . . . . . 15 (({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}) ⊆ ((({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}) ∪ ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))}))
9 kur14lem.t . . . . . . . . . . . . . . 15 𝑇 = ((({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}) ∪ ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))}))
108, 9sseqtr4i 3832 . . . . . . . . . . . . . 14 (({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}) ⊆ 𝑇
117, 10sstri 3804 . . . . . . . . . . . . 13 ({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ⊆ 𝑇
126, 11sstri 3804 . . . . . . . . . . . 12 {𝐴, (𝑋𝐴), (𝐾𝐴)} ⊆ 𝑇
13 kur14lem.j . . . . . . . . . . . . . . . 16 𝐽 ∈ Top
14 kur14lem.x . . . . . . . . . . . . . . . . 17 𝑋 = 𝐽
1514topopn 20920 . . . . . . . . . . . . . . . 16 (𝐽 ∈ Top → 𝑋𝐽)
1613, 15ax-mp 5 . . . . . . . . . . . . . . 15 𝑋𝐽
1716elexi 3406 . . . . . . . . . . . . . 14 𝑋 ∈ V
18 difss 3933 . . . . . . . . . . . . . 14 (𝑋𝐴) ⊆ 𝑋
1917, 18ssexi 4995 . . . . . . . . . . . . 13 (𝑋𝐴) ∈ V
2019tpid2 4492 . . . . . . . . . . . 12 (𝑋𝐴) ∈ {𝐴, (𝑋𝐴), (𝐾𝐴)}
2112, 20sselii 3792 . . . . . . . . . . 11 (𝑋𝐴) ∈ 𝑇
22 fvex 6418 . . . . . . . . . . . . 13 (𝐾𝐴) ∈ V
2322tpid3 4494 . . . . . . . . . . . 12 (𝐾𝐴) ∈ {𝐴, (𝑋𝐴), (𝐾𝐴)}
2412, 23sselii 3792 . . . . . . . . . . 11 (𝐾𝐴) ∈ 𝑇
255, 21, 24kur14lem1 31508 . . . . . . . . . 10 (𝑁 = 𝐴 → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
26 kur14lem.k . . . . . . . . . . . . 13 𝐾 = (cls‘𝐽)
27 kur14lem.i . . . . . . . . . . . . 13 𝐼 = (int‘𝐽)
2813, 14, 26, 27, 5kur14lem4 31511 . . . . . . . . . . . 12 (𝑋 ∖ (𝑋𝐴)) = 𝐴
2917, 5ssexi 4995 . . . . . . . . . . . . . 14 𝐴 ∈ V
3029tpid1 4491 . . . . . . . . . . . . 13 𝐴 ∈ {𝐴, (𝑋𝐴), (𝐾𝐴)}
3112, 30sselii 3792 . . . . . . . . . . . 12 𝐴𝑇
3228, 31eqeltri 2880 . . . . . . . . . . 11 (𝑋 ∖ (𝑋𝐴)) ∈ 𝑇
33 kur14lem.c . . . . . . . . . . . 12 𝐶 = (𝐾‘(𝑋𝐴))
34 ssun2 3973 . . . . . . . . . . . . . 14 {𝐵, 𝐶, (𝐼𝐴)} ⊆ ({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)})
3534, 11sstri 3804 . . . . . . . . . . . . 13 {𝐵, 𝐶, (𝐼𝐴)} ⊆ 𝑇
3613, 14, 26, 27, 18kur14lem3 31510 . . . . . . . . . . . . . . . 16 (𝐾‘(𝑋𝐴)) ⊆ 𝑋
3733, 36eqsstri 3829 . . . . . . . . . . . . . . 15 𝐶𝑋
3817, 37ssexi 4995 . . . . . . . . . . . . . 14 𝐶 ∈ V
3938tpid2 4492 . . . . . . . . . . . . 13 𝐶 ∈ {𝐵, 𝐶, (𝐼𝐴)}
4035, 39sselii 3792 . . . . . . . . . . . 12 𝐶𝑇
4133, 40eqeltrri 2881 . . . . . . . . . . 11 (𝐾‘(𝑋𝐴)) ∈ 𝑇
4218, 32, 41kur14lem1 31508 . . . . . . . . . 10 (𝑁 = (𝑋𝐴) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
4313, 14, 26, 27, 5kur14lem3 31510 . . . . . . . . . . 11 (𝐾𝐴) ⊆ 𝑋
44 kur14lem.b . . . . . . . . . . . 12 𝐵 = (𝑋 ∖ (𝐾𝐴))
45 difss 3933 . . . . . . . . . . . . . . . 16 (𝑋 ∖ (𝐾𝐴)) ⊆ 𝑋
4644, 45eqsstri 3829 . . . . . . . . . . . . . . 15 𝐵𝑋
4717, 46ssexi 4995 . . . . . . . . . . . . . 14 𝐵 ∈ V
4847tpid1 4491 . . . . . . . . . . . . 13 𝐵 ∈ {𝐵, 𝐶, (𝐼𝐴)}
4935, 48sselii 3792 . . . . . . . . . . . 12 𝐵𝑇
5044, 49eqeltrri 2881 . . . . . . . . . . 11 (𝑋 ∖ (𝐾𝐴)) ∈ 𝑇
5113, 14, 26, 27, 5kur14lem5 31512 . . . . . . . . . . . 12 (𝐾‘(𝐾𝐴)) = (𝐾𝐴)
5251, 24eqeltri 2880 . . . . . . . . . . 11 (𝐾‘(𝐾𝐴)) ∈ 𝑇
5343, 50, 52kur14lem1 31508 . . . . . . . . . 10 (𝑁 = (𝐾𝐴) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
5425, 42, 533jaoi 1545 . . . . . . . . 9 ((𝑁 = 𝐴𝑁 = (𝑋𝐴) ∨ 𝑁 = (𝐾𝐴)) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
554, 54syl 17 . . . . . . . 8 (𝑁 ∈ {𝐴, (𝑋𝐴), (𝐾𝐴)} → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
56 eltpi 4418 . . . . . . . . 9 (𝑁 ∈ {𝐵, 𝐶, (𝐼𝐴)} → (𝑁 = 𝐵𝑁 = 𝐶𝑁 = (𝐼𝐴)))
5744difeq2i 3921 . . . . . . . . . . . . 13 (𝑋𝐵) = (𝑋 ∖ (𝑋 ∖ (𝐾𝐴)))
5813, 14, 26, 27, 43kur14lem4 31511 . . . . . . . . . . . . 13 (𝑋 ∖ (𝑋 ∖ (𝐾𝐴))) = (𝐾𝐴)
5957, 58eqtri 2827 . . . . . . . . . . . 12 (𝑋𝐵) = (𝐾𝐴)
6059, 24eqeltri 2880 . . . . . . . . . . 11 (𝑋𝐵) ∈ 𝑇
61 ssun2 3973 . . . . . . . . . . . . 13 {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))} ⊆ (({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))})
6261, 10sstri 3804 . . . . . . . . . . . 12 {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))} ⊆ 𝑇
63 fvex 6418 . . . . . . . . . . . . 13 (𝐾𝐵) ∈ V
6463tpid1 4491 . . . . . . . . . . . 12 (𝐾𝐵) ∈ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}
6562, 64sselii 3792 . . . . . . . . . . 11 (𝐾𝐵) ∈ 𝑇
6646, 60, 65kur14lem1 31508 . . . . . . . . . 10 (𝑁 = 𝐵 → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
6733difeq2i 3921 . . . . . . . . . . . . 13 (𝑋𝐶) = (𝑋 ∖ (𝐾‘(𝑋𝐴)))
6813, 14, 26, 27, 5kur14lem2 31509 . . . . . . . . . . . . 13 (𝐼𝐴) = (𝑋 ∖ (𝐾‘(𝑋𝐴)))
6967, 68eqtr4i 2830 . . . . . . . . . . . 12 (𝑋𝐶) = (𝐼𝐴)
70 fvex 6418 . . . . . . . . . . . . . 14 (𝐼𝐴) ∈ V
7170tpid3 4494 . . . . . . . . . . . . 13 (𝐼𝐴) ∈ {𝐵, 𝐶, (𝐼𝐴)}
7235, 71sselii 3792 . . . . . . . . . . . 12 (𝐼𝐴) ∈ 𝑇
7369, 72eqeltri 2880 . . . . . . . . . . 11 (𝑋𝐶) ∈ 𝑇
7413, 14, 26, 27, 18kur14lem5 31512 . . . . . . . . . . . . 13 (𝐾‘(𝐾‘(𝑋𝐴))) = (𝐾‘(𝑋𝐴))
7533fveq2i 6408 . . . . . . . . . . . . 13 (𝐾𝐶) = (𝐾‘(𝐾‘(𝑋𝐴)))
7674, 75, 333eqtr4i 2837 . . . . . . . . . . . 12 (𝐾𝐶) = 𝐶
7776, 40eqeltri 2880 . . . . . . . . . . 11 (𝐾𝐶) ∈ 𝑇
7837, 73, 77kur14lem1 31508 . . . . . . . . . 10 (𝑁 = 𝐶 → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
79 difss 3933 . . . . . . . . . . . 12 (𝑋 ∖ (𝐾‘(𝑋𝐴))) ⊆ 𝑋
8068, 79eqsstri 3829 . . . . . . . . . . 11 (𝐼𝐴) ⊆ 𝑋
8169difeq2i 3921 . . . . . . . . . . . . 13 (𝑋 ∖ (𝑋𝐶)) = (𝑋 ∖ (𝐼𝐴))
8213, 14, 26, 27, 37kur14lem4 31511 . . . . . . . . . . . . 13 (𝑋 ∖ (𝑋𝐶)) = 𝐶
8381, 82eqtr3i 2829 . . . . . . . . . . . 12 (𝑋 ∖ (𝐼𝐴)) = 𝐶
8483, 40eqeltri 2880 . . . . . . . . . . 11 (𝑋 ∖ (𝐼𝐴)) ∈ 𝑇
85 fvex 6418 . . . . . . . . . . . . 13 (𝐾‘(𝐼𝐴)) ∈ V
8685tpid3 4494 . . . . . . . . . . . 12 (𝐾‘(𝐼𝐴)) ∈ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}
8762, 86sselii 3792 . . . . . . . . . . 11 (𝐾‘(𝐼𝐴)) ∈ 𝑇
8880, 84, 87kur14lem1 31508 . . . . . . . . . 10 (𝑁 = (𝐼𝐴) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
8966, 78, 883jaoi 1545 . . . . . . . . 9 ((𝑁 = 𝐵𝑁 = 𝐶𝑁 = (𝐼𝐴)) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
9056, 89syl 17 . . . . . . . 8 (𝑁 ∈ {𝐵, 𝐶, (𝐼𝐴)} → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
9155, 90jaoi 875 . . . . . . 7 ((𝑁 ∈ {𝐴, (𝑋𝐴), (𝐾𝐴)} ∨ 𝑁 ∈ {𝐵, 𝐶, (𝐼𝐴)}) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
923, 91sylbi 208 . . . . . 6 (𝑁 ∈ ({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
93 eltpi 4418 . . . . . . 7 (𝑁 ∈ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))} → (𝑁 = (𝐾𝐵) ∨ 𝑁 = 𝐷𝑁 = (𝐾‘(𝐼𝐴))))
9413, 14, 26, 27, 46kur14lem3 31510 . . . . . . . . 9 (𝐾𝐵) ⊆ 𝑋
9513, 14, 26, 27, 43kur14lem2 31509 . . . . . . . . . . 11 (𝐼‘(𝐾𝐴)) = (𝑋 ∖ (𝐾‘(𝑋 ∖ (𝐾𝐴))))
96 kur14lem.d . . . . . . . . . . 11 𝐷 = (𝐼‘(𝐾𝐴))
9744fveq2i 6408 . . . . . . . . . . . 12 (𝐾𝐵) = (𝐾‘(𝑋 ∖ (𝐾𝐴)))
9897difeq2i 3921 . . . . . . . . . . 11 (𝑋 ∖ (𝐾𝐵)) = (𝑋 ∖ (𝐾‘(𝑋 ∖ (𝐾𝐴))))
9995, 96, 983eqtr4i 2837 . . . . . . . . . 10 𝐷 = (𝑋 ∖ (𝐾𝐵))
10096, 95eqtri 2827 . . . . . . . . . . . . . 14 𝐷 = (𝑋 ∖ (𝐾‘(𝑋 ∖ (𝐾𝐴))))
101 difss 3933 . . . . . . . . . . . . . 14 (𝑋 ∖ (𝐾‘(𝑋 ∖ (𝐾𝐴)))) ⊆ 𝑋
102100, 101eqsstri 3829 . . . . . . . . . . . . 13 𝐷𝑋
10317, 102ssexi 4995 . . . . . . . . . . . 12 𝐷 ∈ V
104103tpid2 4492 . . . . . . . . . . 11 𝐷 ∈ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}
10562, 104sselii 3792 . . . . . . . . . 10 𝐷𝑇
10699, 105eqeltrri 2881 . . . . . . . . 9 (𝑋 ∖ (𝐾𝐵)) ∈ 𝑇
10713, 14, 26, 27, 46kur14lem5 31512 . . . . . . . . . 10 (𝐾‘(𝐾𝐵)) = (𝐾𝐵)
108107, 65eqeltri 2880 . . . . . . . . 9 (𝐾‘(𝐾𝐵)) ∈ 𝑇
10994, 106, 108kur14lem1 31508 . . . . . . . 8 (𝑁 = (𝐾𝐵) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
11099difeq2i 3921 . . . . . . . . . . 11 (𝑋𝐷) = (𝑋 ∖ (𝑋 ∖ (𝐾𝐵)))
11113, 14, 26, 27, 94kur14lem4 31511 . . . . . . . . . . 11 (𝑋 ∖ (𝑋 ∖ (𝐾𝐵))) = (𝐾𝐵)
112110, 111eqtri 2827 . . . . . . . . . 10 (𝑋𝐷) = (𝐾𝐵)
113112, 65eqeltri 2880 . . . . . . . . 9 (𝑋𝐷) ∈ 𝑇
114 ssun1 3972 . . . . . . . . . . 11 {(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ⊆ ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))})
115 ssun2 3973 . . . . . . . . . . . 12 ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))}) ⊆ ((({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}) ∪ ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))}))
116115, 9sseqtr4i 3832 . . . . . . . . . . 11 ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))}) ⊆ 𝑇
117114, 116sstri 3804 . . . . . . . . . 10 {(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ⊆ 𝑇
118 fvex 6418 . . . . . . . . . . 11 (𝐾𝐷) ∈ V
119118tpid2 4492 . . . . . . . . . 10 (𝐾𝐷) ∈ {(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))}
120117, 119sselii 3792 . . . . . . . . 9 (𝐾𝐷) ∈ 𝑇
121102, 113, 120kur14lem1 31508 . . . . . . . 8 (𝑁 = 𝐷 → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
12213, 14, 26, 27, 80kur14lem3 31510 . . . . . . . . 9 (𝐾‘(𝐼𝐴)) ⊆ 𝑋
12313, 14, 26, 27, 37kur14lem2 31509 . . . . . . . . . . 11 (𝐼𝐶) = (𝑋 ∖ (𝐾‘(𝑋𝐶)))
12469fveq2i 6408 . . . . . . . . . . . 12 (𝐾‘(𝑋𝐶)) = (𝐾‘(𝐼𝐴))
125124difeq2i 3921 . . . . . . . . . . 11 (𝑋 ∖ (𝐾‘(𝑋𝐶))) = (𝑋 ∖ (𝐾‘(𝐼𝐴)))
126123, 125eqtri 2827 . . . . . . . . . 10 (𝐼𝐶) = (𝑋 ∖ (𝐾‘(𝐼𝐴)))
127 fvex 6418 . . . . . . . . . . . 12 (𝐼𝐶) ∈ V
128127tpid1 4491 . . . . . . . . . . 11 (𝐼𝐶) ∈ {(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))}
129117, 128sselii 3792 . . . . . . . . . 10 (𝐼𝐶) ∈ 𝑇
130126, 129eqeltrri 2881 . . . . . . . . 9 (𝑋 ∖ (𝐾‘(𝐼𝐴))) ∈ 𝑇
13113, 14, 26, 27, 80kur14lem5 31512 . . . . . . . . . 10 (𝐾‘(𝐾‘(𝐼𝐴))) = (𝐾‘(𝐼𝐴))
132131, 87eqeltri 2880 . . . . . . . . 9 (𝐾‘(𝐾‘(𝐼𝐴))) ∈ 𝑇
133122, 130, 132kur14lem1 31508 . . . . . . . 8 (𝑁 = (𝐾‘(𝐼𝐴)) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
134109, 121, 1333jaoi 1545 . . . . . . 7 ((𝑁 = (𝐾𝐵) ∨ 𝑁 = 𝐷𝑁 = (𝐾‘(𝐼𝐴))) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
13593, 134syl 17 . . . . . 6 (𝑁 ∈ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))} → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
13692, 135jaoi 875 . . . . 5 ((𝑁 ∈ ({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∨ 𝑁 ∈ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
1372, 136sylbi 208 . . . 4 (𝑁 ∈ (({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
138 elun 3949 . . . . 5 (𝑁 ∈ ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))}) ↔ (𝑁 ∈ {(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∨ 𝑁 ∈ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))}))
139 eltpi 4418 . . . . . . 7 (𝑁 ∈ {(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} → (𝑁 = (𝐼𝐶) ∨ 𝑁 = (𝐾𝐷) ∨ 𝑁 = (𝐼‘(𝐾𝐵))))
140 difss 3933 . . . . . . . . . 10 (𝑋 ∖ (𝐾‘(𝑋𝐶))) ⊆ 𝑋
141123, 140eqsstri 3829 . . . . . . . . 9 (𝐼𝐶) ⊆ 𝑋
142126difeq2i 3921 . . . . . . . . . . 11 (𝑋 ∖ (𝐼𝐶)) = (𝑋 ∖ (𝑋 ∖ (𝐾‘(𝐼𝐴))))
14313, 14, 26, 27, 122kur14lem4 31511 . . . . . . . . . . 11 (𝑋 ∖ (𝑋 ∖ (𝐾‘(𝐼𝐴)))) = (𝐾‘(𝐼𝐴))
144142, 143eqtri 2827 . . . . . . . . . 10 (𝑋 ∖ (𝐼𝐶)) = (𝐾‘(𝐼𝐴))
145144, 87eqeltri 2880 . . . . . . . . 9 (𝑋 ∖ (𝐼𝐶)) ∈ 𝑇
146 ssun2 3973 . . . . . . . . . . 11 {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))} ⊆ ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))})
147146, 116sstri 3804 . . . . . . . . . 10 {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))} ⊆ 𝑇
148 fvex 6418 . . . . . . . . . . 11 (𝐾‘(𝐼𝐶)) ∈ V
149148prid1 4485 . . . . . . . . . 10 (𝐾‘(𝐼𝐶)) ∈ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))}
150147, 149sselii 3792 . . . . . . . . 9 (𝐾‘(𝐼𝐶)) ∈ 𝑇
151141, 145, 150kur14lem1 31508 . . . . . . . 8 (𝑁 = (𝐼𝐶) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
15213, 14, 26, 27, 102kur14lem3 31510 . . . . . . . . 9 (𝐾𝐷) ⊆ 𝑋
15399fveq2i 6408 . . . . . . . . . . . 12 (𝐾𝐷) = (𝐾‘(𝑋 ∖ (𝐾𝐵)))
154153difeq2i 3921 . . . . . . . . . . 11 (𝑋 ∖ (𝐾𝐷)) = (𝑋 ∖ (𝐾‘(𝑋 ∖ (𝐾𝐵))))
15513, 14, 26, 27, 94kur14lem2 31509 . . . . . . . . . . 11 (𝐼‘(𝐾𝐵)) = (𝑋 ∖ (𝐾‘(𝑋 ∖ (𝐾𝐵))))
156154, 155eqtr4i 2830 . . . . . . . . . 10 (𝑋 ∖ (𝐾𝐷)) = (𝐼‘(𝐾𝐵))
157 fvex 6418 . . . . . . . . . . . 12 (𝐼‘(𝐾𝐵)) ∈ V
158157tpid3 4494 . . . . . . . . . . 11 (𝐼‘(𝐾𝐵)) ∈ {(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))}
159117, 158sselii 3792 . . . . . . . . . 10 (𝐼‘(𝐾𝐵)) ∈ 𝑇
160156, 159eqeltri 2880 . . . . . . . . 9 (𝑋 ∖ (𝐾𝐷)) ∈ 𝑇
16113, 14, 26, 27, 102kur14lem5 31512 . . . . . . . . . 10 (𝐾‘(𝐾𝐷)) = (𝐾𝐷)
162161, 120eqeltri 2880 . . . . . . . . 9 (𝐾‘(𝐾𝐷)) ∈ 𝑇
163152, 160, 162kur14lem1 31508 . . . . . . . 8 (𝑁 = (𝐾𝐷) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
164 difss 3933 . . . . . . . . . 10 (𝑋 ∖ (𝐾‘(𝑋 ∖ (𝐾𝐵)))) ⊆ 𝑋
165155, 164eqsstri 3829 . . . . . . . . 9 (𝐼‘(𝐾𝐵)) ⊆ 𝑋
166156difeq2i 3921 . . . . . . . . . . 11 (𝑋 ∖ (𝑋 ∖ (𝐾𝐷))) = (𝑋 ∖ (𝐼‘(𝐾𝐵)))
16713, 14, 26, 27, 152kur14lem4 31511 . . . . . . . . . . 11 (𝑋 ∖ (𝑋 ∖ (𝐾𝐷))) = (𝐾𝐷)
168166, 167eqtr3i 2829 . . . . . . . . . 10 (𝑋 ∖ (𝐼‘(𝐾𝐵))) = (𝐾𝐷)
169168, 120eqeltri 2880 . . . . . . . . 9 (𝑋 ∖ (𝐼‘(𝐾𝐵))) ∈ 𝑇
17013, 14, 26, 27, 5, 44kur14lem6 31513 . . . . . . . . . 10 (𝐾‘(𝐼‘(𝐾𝐵))) = (𝐾𝐵)
171170, 65eqeltri 2880 . . . . . . . . 9 (𝐾‘(𝐼‘(𝐾𝐵))) ∈ 𝑇
172165, 169, 171kur14lem1 31508 . . . . . . . 8 (𝑁 = (𝐼‘(𝐾𝐵)) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
173151, 163, 1723jaoi 1545 . . . . . . 7 ((𝑁 = (𝐼𝐶) ∨ 𝑁 = (𝐾𝐷) ∨ 𝑁 = (𝐼‘(𝐾𝐵))) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
174139, 173syl 17 . . . . . 6 (𝑁 ∈ {(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
175 elpri 4389 . . . . . . 7 (𝑁 ∈ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))} → (𝑁 = (𝐾‘(𝐼𝐶)) ∨ 𝑁 = (𝐼‘(𝐾‘(𝐼𝐴)))))
17613, 14, 26, 27, 141kur14lem3 31510 . . . . . . . . 9 (𝐾‘(𝐼𝐶)) ⊆ 𝑋
177126fveq2i 6408 . . . . . . . . . . . 12 (𝐾‘(𝐼𝐶)) = (𝐾‘(𝑋 ∖ (𝐾‘(𝐼𝐴))))
178177difeq2i 3921 . . . . . . . . . . 11 (𝑋 ∖ (𝐾‘(𝐼𝐶))) = (𝑋 ∖ (𝐾‘(𝑋 ∖ (𝐾‘(𝐼𝐴)))))
17913, 14, 26, 27, 122kur14lem2 31509 . . . . . . . . . . 11 (𝐼‘(𝐾‘(𝐼𝐴))) = (𝑋 ∖ (𝐾‘(𝑋 ∖ (𝐾‘(𝐼𝐴)))))
180178, 179eqtr4i 2830 . . . . . . . . . 10 (𝑋 ∖ (𝐾‘(𝐼𝐶))) = (𝐼‘(𝐾‘(𝐼𝐴)))
181 fvex 6418 . . . . . . . . . . . 12 (𝐼‘(𝐾‘(𝐼𝐴))) ∈ V
182181prid2 4486 . . . . . . . . . . 11 (𝐼‘(𝐾‘(𝐼𝐴))) ∈ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))}
183147, 182sselii 3792 . . . . . . . . . 10 (𝐼‘(𝐾‘(𝐼𝐴))) ∈ 𝑇
184180, 183eqeltri 2880 . . . . . . . . 9 (𝑋 ∖ (𝐾‘(𝐼𝐶))) ∈ 𝑇
18513, 14, 26, 27, 141kur14lem5 31512 . . . . . . . . . 10 (𝐾‘(𝐾‘(𝐼𝐶))) = (𝐾‘(𝐼𝐶))
186185, 150eqeltri 2880 . . . . . . . . 9 (𝐾‘(𝐾‘(𝐼𝐶))) ∈ 𝑇
187176, 184, 186kur14lem1 31508 . . . . . . . 8 (𝑁 = (𝐾‘(𝐼𝐶)) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
188 difss 3933 . . . . . . . . . 10 (𝑋 ∖ (𝐾‘(𝑋 ∖ (𝐾‘(𝐼𝐴))))) ⊆ 𝑋
189179, 188eqsstri 3829 . . . . . . . . 9 (𝐼‘(𝐾‘(𝐼𝐴))) ⊆ 𝑋
190180difeq2i 3921 . . . . . . . . . . 11 (𝑋 ∖ (𝑋 ∖ (𝐾‘(𝐼𝐶)))) = (𝑋 ∖ (𝐼‘(𝐾‘(𝐼𝐴))))
19113, 14, 26, 27, 176kur14lem4 31511 . . . . . . . . . . 11 (𝑋 ∖ (𝑋 ∖ (𝐾‘(𝐼𝐶)))) = (𝐾‘(𝐼𝐶))
192190, 191eqtr3i 2829 . . . . . . . . . 10 (𝑋 ∖ (𝐼‘(𝐾‘(𝐼𝐴)))) = (𝐾‘(𝐼𝐶))
193192, 150eqeltri 2880 . . . . . . . . 9 (𝑋 ∖ (𝐼‘(𝐾‘(𝐼𝐴)))) ∈ 𝑇
19413, 14, 26, 27, 18, 68kur14lem6 31513 . . . . . . . . . 10 (𝐾‘(𝐼‘(𝐾‘(𝐼𝐴)))) = (𝐾‘(𝐼𝐴))
195194, 87eqeltri 2880 . . . . . . . . 9 (𝐾‘(𝐼‘(𝐾‘(𝐼𝐴)))) ∈ 𝑇
196189, 193, 195kur14lem1 31508 . . . . . . . 8 (𝑁 = (𝐼‘(𝐾‘(𝐼𝐴))) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
197187, 196jaoi 875 . . . . . . 7 ((𝑁 = (𝐾‘(𝐼𝐶)) ∨ 𝑁 = (𝐼‘(𝐾‘(𝐼𝐴)))) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
198175, 197syl 17 . . . . . 6 (𝑁 ∈ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))} → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
199174, 198jaoi 875 . . . . 5 ((𝑁 ∈ {(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∨ 𝑁 ∈ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))}) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
200138, 199sylbi 208 . . . 4 (𝑁 ∈ ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))}) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
201137, 200jaoi 875 . . 3 ((𝑁 ∈ (({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}) ∨ 𝑁 ∈ ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))})) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
2021, 201sylbi 208 . 2 (𝑁 ∈ ((({𝐴, (𝑋𝐴), (𝐾𝐴)} ∪ {𝐵, 𝐶, (𝐼𝐴)}) ∪ {(𝐾𝐵), 𝐷, (𝐾‘(𝐼𝐴))}) ∪ ({(𝐼𝐶), (𝐾𝐷), (𝐼‘(𝐾𝐵))} ∪ {(𝐾‘(𝐼𝐶)), (𝐼‘(𝐾‘(𝐼𝐴)))})) → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
203202, 9eleq2s 2902 1 (𝑁𝑇 → (𝑁𝑋 ∧ {(𝑋𝑁), (𝐾𝑁)} ⊆ 𝑇))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wo 865  w3o 1099   = wceq 1637  wcel 2158  cdif 3763  cun 3764  wss 3766  {cpr 4369  {ctp 4371   cuni 4626  cfv 6098  Topctop 20907  intcnt 21031  clsccl 21032
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-8 2160  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-rep 4960  ax-sep 4971  ax-nul 4980  ax-pow 5032  ax-pr 5093  ax-un 7176
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-mo 2637  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ne 2978  df-ral 3100  df-rex 3101  df-reu 3102  df-rab 3104  df-v 3392  df-sbc 3631  df-csb 3726  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-nul 4114  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-uni 4627  df-int 4666  df-iun 4710  df-iin 4711  df-br 4841  df-opab 4903  df-mpt 4920  df-id 5216  df-xp 5314  df-rel 5315  df-cnv 5316  df-co 5317  df-dm 5318  df-rn 5319  df-res 5320  df-ima 5321  df-iota 6061  df-fun 6100  df-fn 6101  df-f 6102  df-f1 6103  df-fo 6104  df-f1o 6105  df-fv 6106  df-top 20908  df-cld 21033  df-ntr 21034  df-cls 21035
This theorem is referenced by:  kur14lem9  31516
  Copyright terms: Public domain W3C validator