Theorem kur14lem10

Description: Lemma for kur14 . Discharge the set T . (Contributed by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Hypotheses	kur14lem10.j	$$⊢J\in \mathrm{Top}$$
	kur14lem10.x	$$⊢X=\bigcup J$$
	kur14lem10.k	$$⊢K=\mathrm{cls}\left(J\right)$$
	kur14lem10.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\}$$
	kur14lem10.a	$$⊢A\subseteq X$$
Assertion	kur14lem10	$$⊢\left(S\in \mathrm{Fin}\wedge \left|S\right|\le 14\right)$$

Proof

Step	Hyp	Ref	Expression
1		kur14lem10.j	$$⊢J\in \mathrm{Top}$$
2		kur14lem10.x	$$⊢X=\bigcup J$$
3		kur14lem10.k	$$⊢K=\mathrm{cls}\left(J\right)$$
4		kur14lem10.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\}$$
5		kur14lem10.a	$$⊢A\subseteq X$$
6		eqid	$$⊢\mathrm{int}\left(J\right)=\mathrm{int}\left(J\right)$$
7		eqid	$$⊢X\setminus K\left(A\right)=X\setminus K\left(A\right)$$
8		eqid	$$⊢K\left(X\setminus A\right)=K\left(X\setminus A\right)$$
9		eqid	$$⊢\mathrm{int}\left(J\right)\left(K\left(A\right)\right)=\mathrm{int}\left(J\right)\left(K\left(A\right)\right)$$
10		eqid	$$⊢\left(\left(\left\{A,X\setminus A,K\left(A\right)\right\}\cup \left\{X\setminus K\left(A\right),K\left(X\setminus A\right),\mathrm{int}\left(J\right)\left(A\right)\right\}\right)\cup \left\{K\left(X\setminus K\left(A\right)\right),\mathrm{int}\left(J\right)\left(K\left(A\right)\right),K\left(\mathrm{int}\left(J\right)\left(A\right)\right)\right\}\right)\cup \left(\left\{\mathrm{int}\left(J\right)\left(K\left(X\setminus A\right)\right),K\left(\mathrm{int}\left(J\right)\left(K\left(A\right)\right)\right),\mathrm{int}\left(J\right)\left(K\left(X\setminus K\left(A\right)\right)\right)\right\}\cup \left\{K\left(\mathrm{int}\left(J\right)\left(K\left(X\setminus A\right)\right)\right),\mathrm{int}\left(J\right)\left(K\left(\mathrm{int}\left(J\right)\left(A\right)\right)\right)\right\}\right)=\left(\left(\left\{A,X\setminus A,K\left(A\right)\right\}\cup \left\{X\setminus K\left(A\right),K\left(X\setminus A\right),\mathrm{int}\left(J\right)\left(A\right)\right\}\right)\cup \left\{K\left(X\setminus K\left(A\right)\right),\mathrm{int}\left(J\right)\left(K\left(A\right)\right),K\left(\mathrm{int}\left(J\right)\left(A\right)\right)\right\}\right)\cup \left(\left\{\mathrm{int}\left(J\right)\left(K\left(X\setminus A\right)\right),K\left(\mathrm{int}\left(J\right)\left(K\left(A\right)\right)\right),\mathrm{int}\left(J\right)\left(K\left(X\setminus K\left(A\right)\right)\right)\right\}\cup \left\{K\left(\mathrm{int}\left(J\right)\left(K\left(X\setminus A\right)\right)\right),\mathrm{int}\left(J\right)\left(K\left(\mathrm{int}\left(J\right)\left(A\right)\right)\right)\right\}\right)$$
11	1 2 3 6 5 7 8 9 10 4	kur14lem9	$$⊢\left(S\in \mathrm{Fin}\wedge \left|S\right|\le 14\right)$$