Metamath Proof Explorer

Theorem kur14lem8

Description: Lemma for kur14 . Show that the set T contains at most 1 4 elements. (It could be less if some of the operators take the same value for a given set, but Kuratowski showed that this upper bound of 1 4 is tight in the sense that there exist topological spaces and subsets of these spaces for which all 1 4 generated sets are distinct, and indeed the real numbers form such a topological space.) (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=AX∖AK⁡A∪BCI⁡A∪K⁡BDK⁡I⁡A∪I⁡CK⁡DI⁡K⁡B∪K⁡I⁡CI⁡K⁡I⁡A
Assertion kur14lem8 ⊢T∈Fin∧T≤14

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=AX∖AK⁡A∪BCI⁡A∪K⁡BDK⁡I⁡A∪I⁡CK⁡DI⁡K⁡B∪K⁡I⁡CI⁡K⁡I⁡A
10 eqid ⊢AX∖AK⁡A∪BCI⁡A∪K⁡BDK⁡I⁡A=AX∖AK⁡A∪BCI⁡A∪K⁡BDK⁡I⁡A
11 eqid ⊢AX∖AK⁡A∪BCI⁡A=AX∖AK⁡A∪BCI⁡A
12 hashtplei ⊢AX∖AK⁡A∈Fin∧AX∖AK⁡A≤3
13 hashtplei ⊢BCI⁡A∈Fin∧BCI⁡A≤3
14 3nn0 ⊢3∈ℕ0
15 3p3e6 ⊢3+3=6
16 11 12 13 14 14 15 hashunlei ⊢AX∖AK⁡A∪BCI⁡A∈Fin∧AX∖AK⁡A∪BCI⁡A≤6
17 hashtplei ⊢K⁡BDK⁡I⁡A∈Fin∧K⁡BDK⁡I⁡A≤3
18 6nn0 ⊢6∈ℕ0
19 6p3e9 ⊢6+3=9
20 10 16 17 18 14 19 hashunlei ⊢AX∖AK⁡A∪BCI⁡A∪K⁡BDK⁡I⁡A∈Fin∧AX∖AK⁡A∪BCI⁡A∪K⁡BDK⁡I⁡A≤9
21 eqid ⊢I⁡CK⁡DI⁡K⁡B∪K⁡I⁡CI⁡K⁡I⁡A=I⁡CK⁡DI⁡K⁡B∪K⁡I⁡CI⁡K⁡I⁡A
22 hashtplei ⊢I⁡CK⁡DI⁡K⁡B∈Fin∧I⁡CK⁡DI⁡K⁡B≤3
23 hashprlei ⊢K⁡I⁡CI⁡K⁡I⁡A∈Fin∧K⁡I⁡CI⁡K⁡I⁡A≤2
24 2nn0 ⊢2∈ℕ0
25 3p2e5 ⊢3+2=5
26 21 22 23 14 24 25 hashunlei ⊢I⁡CK⁡DI⁡K⁡B∪K⁡I⁡CI⁡K⁡I⁡A∈Fin∧I⁡CK⁡DI⁡K⁡B∪K⁡I⁡CI⁡K⁡I⁡A≤5
27 9nn0 ⊢9∈ℕ0
28 5nn0 ⊢5∈ℕ0
29 9p5e14 ⊢9+5=14
30 9 20 26 27 28 29 hashunlei ⊢T∈Fin∧T≤14