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\in \mathrm{Top}$$
	kur14lem.x	$$⊢X=\bigcup J$$
	kur14lem.k	$$⊢K=\mathrm{cls}\left(J\right)$$
	kur14lem.i	$$⊢I=\mathrm{int}\left(J\right)$$
	kur14lem.a	$$⊢A\subseteq X$$
	kur14lem.b	$$⊢B=X\setminus K\left(A\right)$$
	kur14lem.c	$$⊢C=K\left(X\setminus A\right)$$
	kur14lem.d	$$⊢D=I\left(K\left(A\right)\right)$$
	kur14lem.t	$$⊢T=\left(\left(\left\{A,X\setminus A,K\left(A\right)\right\}\cup \left\{B,C,I\left(A\right)\right\}\right)\cup \left\{K\left(B\right),D,K\left(I\left(A\right)\right)\right\}\right)\cup \left(\left\{I\left(C\right),K\left(D\right),I\left(K\left(B\right)\right)\right\}\cup \left\{K\left(I\left(C\right)\right),I\left(K\left(I\left(A\right)\right)\right)\right\}\right)$$
Assertion	kur14lem8	$$⊢\left(T\in \mathrm{Fin}\wedge \left|T\right|\le 14\right)$$

Proof

Step	Hyp	Ref	Expression
1		kur14lem.j	$$⊢J\in \mathrm{Top}$$
2		kur14lem.x	$$⊢X=\bigcup J$$
3		kur14lem.k	$$⊢K=\mathrm{cls}\left(J\right)$$
4		kur14lem.i	$$⊢I=\mathrm{int}\left(J\right)$$
5		kur14lem.a	$$⊢A\subseteq X$$
6		kur14lem.b	$$⊢B=X\setminus K\left(A\right)$$
7		kur14lem.c	$$⊢C=K\left(X\setminus A\right)$$
8		kur14lem.d	$$⊢D=I\left(K\left(A\right)\right)$$
9		kur14lem.t	$$⊢T=\left(\left(\left\{A,X\setminus A,K\left(A\right)\right\}\cup \left\{B,C,I\left(A\right)\right\}\right)\cup \left\{K\left(B\right),D,K\left(I\left(A\right)\right)\right\}\right)\cup \left(\left\{I\left(C\right),K\left(D\right),I\left(K\left(B\right)\right)\right\}\cup \left\{K\left(I\left(C\right)\right),I\left(K\left(I\left(A\right)\right)\right)\right\}\right)$$
10		eqid	$$⊢\left(\left\{A,X\setminus A,K\left(A\right)\right\}\cup \left\{B,C,I\left(A\right)\right\}\right)\cup \left\{K\left(B\right),D,K\left(I\left(A\right)\right)\right\}=\left(\left\{A,X\setminus A,K\left(A\right)\right\}\cup \left\{B,C,I\left(A\right)\right\}\right)\cup \left\{K\left(B\right),D,K\left(I\left(A\right)\right)\right\}$$
11		eqid	$$⊢\left\{A,X\setminus A,K\left(A\right)\right\}\cup \left\{B,C,I\left(A\right)\right\}=\left\{A,X\setminus A,K\left(A\right)\right\}\cup \left\{B,C,I\left(A\right)\right\}$$
12		hashtplei	$$⊢\left(\left\{A,X\setminus A,K\left(A\right)\right\}\in \mathrm{Fin}\wedge \left|\left\{A,X\setminus A,K\left(A\right)\right\}\right|\le 3\right)$$
13		hashtplei	$$⊢\left(\left\{B,C,I\left(A\right)\right\}\in \mathrm{Fin}\wedge \left|\left\{B,C,I\left(A\right)\right\}\right|\le 3\right)$$
14		3nn0	$$⊢3\in {\mathbb{N}}_0$$
15		3p3e6	$$⊢3+3=6$$
16	11 12 13 14 14 15	hashunlei	$$⊢\left(\left\{A,X\setminus A,K\left(A\right)\right\}\cup \left\{B,C,I\left(A\right)\right\}\in \mathrm{Fin}\wedge \left|\left\{A,X\setminus A,K\left(A\right)\right\}\cup \left\{B,C,I\left(A\right)\right\}\right|\le 6\right)$$
17		hashtplei	$$⊢\left(\left\{K\left(B\right),D,K\left(I\left(A\right)\right)\right\}\in \mathrm{Fin}\wedge \left|\left\{K\left(B\right),D,K\left(I\left(A\right)\right)\right\}\right|\le 3\right)$$
18		6nn0	$$⊢6\in {\mathbb{N}}_0$$
19		6p3e9	$$⊢6+3=9$$
20	10 16 17 18 14 19	hashunlei	$$⊢\left(\left(\left\{A,X\setminus A,K\left(A\right)\right\}\cup \left\{B,C,I\left(A\right)\right\}\right)\cup \left\{K\left(B\right),D,K\left(I\left(A\right)\right)\right\}\in \mathrm{Fin}\wedge \left|\left(\left\{A,X\setminus A,K\left(A\right)\right\}\cup \left\{B,C,I\left(A\right)\right\}\right)\cup \left\{K\left(B\right),D,K\left(I\left(A\right)\right)\right\}\right|\le 9\right)$$
21		eqid	$$⊢\left\{I\left(C\right),K\left(D\right),I\left(K\left(B\right)\right)\right\}\cup \left\{K\left(I\left(C\right)\right),I\left(K\left(I\left(A\right)\right)\right)\right\}=\left\{I\left(C\right),K\left(D\right),I\left(K\left(B\right)\right)\right\}\cup \left\{K\left(I\left(C\right)\right),I\left(K\left(I\left(A\right)\right)\right)\right\}$$
22		hashtplei	$$⊢\left(\left\{I\left(C\right),K\left(D\right),I\left(K\left(B\right)\right)\right\}\in \mathrm{Fin}\wedge \left|\left\{I\left(C\right),K\left(D\right),I\left(K\left(B\right)\right)\right\}\right|\le 3\right)$$
23		hashprlei	$$⊢\left(\left\{K\left(I\left(C\right)\right),I\left(K\left(I\left(A\right)\right)\right)\right\}\in \mathrm{Fin}\wedge \left|\left\{K\left(I\left(C\right)\right),I\left(K\left(I\left(A\right)\right)\right)\right\}\right|\le 2\right)$$
24		2nn0	$$⊢2\in {\mathbb{N}}_0$$
25		3p2e5	$$⊢3+2=5$$
26	21 22 23 14 24 25	hashunlei	$$⊢\left(\left\{I\left(C\right),K\left(D\right),I\left(K\left(B\right)\right)\right\}\cup \left\{K\left(I\left(C\right)\right),I\left(K\left(I\left(A\right)\right)\right)\right\}\in \mathrm{Fin}\wedge \left|\left\{I\left(C\right),K\left(D\right),I\left(K\left(B\right)\right)\right\}\cup \left\{K\left(I\left(C\right)\right),I\left(K\left(I\left(A\right)\right)\right)\right\}\right|\le 5\right)$$
27		9nn0	$$⊢9\in {\mathbb{N}}_0$$
28		5nn0	$$⊢5\in {\mathbb{N}}_0$$
29		9p5e14	$$⊢9+5=14$$
30	9 20 26 27 28 29	hashunlei	$$⊢\left(T\in \mathrm{Fin}\wedge \left|T\right|\le 14\right)$$