Theorem kur14lem9

Description: Lemma for kur14 . Since the set T is closed under closure and complement, it contains the minimal set S as a subset, so S also has at most 1 4 elements. (Indeed S = T , and it's not hard to prove this, but we don't need it for this proof.) (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)$$
	kur14lem.s	$$⊢S=\bigcap \left\{x\in 𝒫𝒫X|\left(A\in x\wedge \forall y\in x\left\{X\setminus y,K\left(y\right)\right\}\subseteq x\right)\right\}$$
Assertion	kur14lem9	$$⊢\left(S\in \mathrm{Fin}\wedge \left|S\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		kur14lem.s	$$⊢S=\bigcap \left\{x\in 𝒫𝒫X|\left(A\in x\wedge \forall y\in x\left\{X\setminus y,K\left(y\right)\right\}\subseteq x\right)\right\}$$
11		vex	$$⊢s\in \mathrm{V}$$
12	11	elintrab	$$⊢s\in \bigcap \left\{x\in 𝒫𝒫X|\left(A\in x\wedge \forall y\in x\left\{X\setminus y,K\left(y\right)\right\}\subseteq x\right)\right\}\leftrightarrow \forall x\in 𝒫𝒫X\left(\left(A\in x\wedge \forall y\in x\left\{X\setminus y,K\left(y\right)\right\}\subseteq x\right)\to s\in x\right)$$
13		ssun1	$$⊢\left\{A,X\setminus A,K\left(A\right)\right\}\subseteq \left\{A,X\setminus A,K\left(A\right)\right\}\cup \left\{B,C,I\left(A\right)\right\}$$
14		ssun1	$$⊢\left\{A,X\setminus A,K\left(A\right)\right\}\cup \left\{B,C,I\left(A\right)\right\}\subseteq \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\}$$
15		ssun1	$$⊢\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\}\subseteq \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)$$
16	15 9	sseqtrri	$$⊢\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\}\subseteq T$$
17	14 16	sstri	$$⊢\left\{A,X\setminus A,K\left(A\right)\right\}\cup \left\{B,C,I\left(A\right)\right\}\subseteq T$$
18	13 17	sstri	$$⊢\left\{A,X\setminus A,K\left(A\right)\right\}\subseteq T$$
19	2	topopn	$$⊢J\in \mathrm{Top}\to X\in J$$
20	1 19	ax-mp	$$⊢X\in J$$
21	20	elexi	$$⊢X\in \mathrm{V}$$
22	21 5	ssexi	$$⊢A\in \mathrm{V}$$
23	22	tpid1	$$⊢A\in \left\{A,X\setminus A,K\left(A\right)\right\}$$
24	18 23	sselii	$$⊢A\in T$$
25	1 2 3 4 5 6 7 8 9	kur14lem7	$$⊢y\in T\to \left(y\subseteq X\wedge \left\{X\setminus y,K\left(y\right)\right\}\subseteq T\right)$$
26	25	simprd	$$⊢y\in T\to \left\{X\setminus y,K\left(y\right)\right\}\subseteq T$$
27	26	rgen	$$⊢\forall y\in T\left\{X\setminus y,K\left(y\right)\right\}\subseteq T$$
28	25	simpld	$$⊢y\in T\to y\subseteq X$$
29	21	elpw2	$$⊢y\in 𝒫X\leftrightarrow y\subseteq X$$
30	28 29	sylibr	$$⊢y\in T\to y\in 𝒫X$$
31	30	ssriv	$$⊢T\subseteq 𝒫X$$
32	21	pwex	$$⊢𝒫X\in \mathrm{V}$$
33	32	elpw2	$$⊢T\in 𝒫𝒫X\leftrightarrow T\subseteq 𝒫X$$
34	31 33	mpbir	$$⊢T\in 𝒫𝒫X$$
35		eleq2	$$⊢x=T\to \left(A\in x\leftrightarrow A\in T\right)$$
36		sseq2	$$⊢x=T\to \left(\left\{X\setminus y,K\left(y\right)\right\}\subseteq x\leftrightarrow \left\{X\setminus y,K\left(y\right)\right\}\subseteq T\right)$$
37	36	raleqbi1dv	$$⊢x=T\to \left(\forall y\in x\left\{X\setminus y,K\left(y\right)\right\}\subseteq x\leftrightarrow \forall y\in T\left\{X\setminus y,K\left(y\right)\right\}\subseteq T\right)$$
38	35 37	anbi12d	$$⊢x=T\to \left(\left(A\in x\wedge \forall y\in x\left\{X\setminus y,K\left(y\right)\right\}\subseteq x\right)\leftrightarrow \left(A\in T\wedge \forall y\in T\left\{X\setminus y,K\left(y\right)\right\}\subseteq T\right)\right)$$
39		eleq2	$$⊢x=T\to \left(s\in x\leftrightarrow s\in T\right)$$
40	38 39	imbi12d	$$⊢x=T\to \left(\left(\left(A\in x\wedge \forall y\in x\left\{X\setminus y,K\left(y\right)\right\}\subseteq x\right)\to s\in x\right)\leftrightarrow \left(\left(A\in T\wedge \forall y\in T\left\{X\setminus y,K\left(y\right)\right\}\subseteq T\right)\to s\in T\right)\right)$$
41	40	rspccv	$$⊢\forall x\in 𝒫𝒫X\left(\left(A\in x\wedge \forall y\in x\left\{X\setminus y,K\left(y\right)\right\}\subseteq x\right)\to s\in x\right)\to \left(T\in 𝒫𝒫X\to \left(\left(A\in T\wedge \forall y\in T\left\{X\setminus y,K\left(y\right)\right\}\subseteq T\right)\to s\in T\right)\right)$$
42	34 41	mpi	$$⊢\forall x\in 𝒫𝒫X\left(\left(A\in x\wedge \forall y\in x\left\{X\setminus y,K\left(y\right)\right\}\subseteq x\right)\to s\in x\right)\to \left(\left(A\in T\wedge \forall y\in T\left\{X\setminus y,K\left(y\right)\right\}\subseteq T\right)\to s\in T\right)$$
43	24 27 42	mp2ani	$$⊢\forall x\in 𝒫𝒫X\left(\left(A\in x\wedge \forall y\in x\left\{X\setminus y,K\left(y\right)\right\}\subseteq x\right)\to s\in x\right)\to s\in T$$
44	12 43	sylbi	$$⊢s\in \bigcap \left\{x\in 𝒫𝒫X|\left(A\in x\wedge \forall y\in x\left\{X\setminus y,K\left(y\right)\right\}\subseteq x\right)\right\}\to s\in T$$
45	44	ssriv	$$⊢\bigcap \left\{x\in 𝒫𝒫X|\left(A\in x\wedge \forall y\in x\left\{X\setminus y,K\left(y\right)\right\}\subseteq x\right)\right\}\subseteq T$$
46	10 45	eqsstri	$$⊢S\subseteq T$$
47	1 2 3 4 5 6 7 8 9	kur14lem8	$$⊢\left(T\in \mathrm{Fin}\wedge \left|T\right|\le 14\right)$$
48		1nn0	$$⊢1\in {\mathbb{N}}_0$$
49		4nn0	$$⊢4\in {\mathbb{N}}_0$$
50	48 49	deccl	$$⊢14\in {\mathbb{N}}_0$$
51	46 47 50	hashsslei	$$⊢\left(S\in \mathrm{Fin}\wedge \left|S\right|\le 14\right)$$