Theorem kelac2lem

Description: Lemma for kelac2 and dfac21 : knob topologies are compact. (Contributed by Stefan O'Rear, 22-Feb-2015)

	Ref	Expression
Assertion	kelac2lem	$$⊢S\in V\to \mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\in \mathrm{Comp}$$

Proof

Step	Hyp	Ref	Expression
1		prex	$$⊢\left\{S,\left\{𝒫\bigcup S\right\}\right\}\in \mathrm{V}$$
2		vex	$$⊢x\in \mathrm{V}$$
3	2	elpr	$$⊢x\in \left\{S,\left\{𝒫\bigcup S\right\}\right\}\leftrightarrow \left(x=S\vee x=\left\{𝒫\bigcup S\right\}\right)$$
4		vex	$$⊢y\in \mathrm{V}$$
5	4	elpr	$$⊢y\in \left\{S,\left\{𝒫\bigcup S\right\}\right\}\leftrightarrow \left(y=S\vee y=\left\{𝒫\bigcup S\right\}\right)$$
6		eqtr3	$$⊢\left(x=S\wedge y=S\right)\to x=y$$
7	6	orcd	$$⊢\left(x=S\wedge y=S\right)\to \left(x=y\vee x\cap y=\varnothing \right)$$
8		ineq12	$$⊢\left(x=\left\{𝒫\bigcup S\right\}\wedge y=S\right)\to x\cap y=\left\{𝒫\bigcup S\right\}\cap S$$
9		incom	$$⊢\left\{𝒫\bigcup S\right\}\cap S=S\cap \left\{𝒫\bigcup S\right\}$$
10		pwuninel	$$⊢\neg 𝒫\bigcup S\in S$$
11		disjsn	$$⊢S\cap \left\{𝒫\bigcup S\right\}=\varnothing \leftrightarrow \neg 𝒫\bigcup S\in S$$
12	10 11	mpbir	$$⊢S\cap \left\{𝒫\bigcup S\right\}=\varnothing$$
13	9 12	eqtri	$$⊢\left\{𝒫\bigcup S\right\}\cap S=\varnothing$$
14	8 13	eqtrdi	$$⊢\left(x=\left\{𝒫\bigcup S\right\}\wedge y=S\right)\to x\cap y=\varnothing$$
15	14	olcd	$$⊢\left(x=\left\{𝒫\bigcup S\right\}\wedge y=S\right)\to \left(x=y\vee x\cap y=\varnothing \right)$$
16		ineq12	$$⊢\left(x=S\wedge y=\left\{𝒫\bigcup S\right\}\right)\to x\cap y=S\cap \left\{𝒫\bigcup S\right\}$$
17	16 12	eqtrdi	$$⊢\left(x=S\wedge y=\left\{𝒫\bigcup S\right\}\right)\to x\cap y=\varnothing$$
18	17	olcd	$$⊢\left(x=S\wedge y=\left\{𝒫\bigcup S\right\}\right)\to \left(x=y\vee x\cap y=\varnothing \right)$$
19		eqtr3	$$⊢\left(x=\left\{𝒫\bigcup S\right\}\wedge y=\left\{𝒫\bigcup S\right\}\right)\to x=y$$
20	19	orcd	$$⊢\left(x=\left\{𝒫\bigcup S\right\}\wedge y=\left\{𝒫\bigcup S\right\}\right)\to \left(x=y\vee x\cap y=\varnothing \right)$$
21	7 15 18 20	ccase	$$⊢\left(\left(x=S\vee x=\left\{𝒫\bigcup S\right\}\right)\wedge \left(y=S\vee y=\left\{𝒫\bigcup S\right\}\right)\right)\to \left(x=y\vee x\cap y=\varnothing \right)$$
22	3 5 21	syl2anb	$$⊢\left(x\in \left\{S,\left\{𝒫\bigcup S\right\}\right\}\wedge y\in \left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\to \left(x=y\vee x\cap y=\varnothing \right)$$
23	22	rgen2	$$⊢\forall x\in \left\{S,\left\{𝒫\bigcup S\right\}\right\}\forall y\in \left\{S,\left\{𝒫\bigcup S\right\}\right\}\left(x=y\vee x\cap y=\varnothing \right)$$
24		baspartn	$$⊢\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\in \mathrm{V}\wedge \forall x\in \left\{S,\left\{𝒫\bigcup S\right\}\right\}\forall y\in \left\{S,\left\{𝒫\bigcup S\right\}\right\}\left(x=y\vee x\cap y=\varnothing \right)\right)\to \left\{S,\left\{𝒫\bigcup S\right\}\right\}\in \mathrm{TopBases}$$
25	1 23 24	mp2an	$$⊢\left\{S,\left\{𝒫\bigcup S\right\}\right\}\in \mathrm{TopBases}$$
26		tgcl	$$⊢\left\{S,\left\{𝒫\bigcup S\right\}\right\}\in \mathrm{TopBases}\to \mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\in \mathrm{Top}$$
27	25 26	mp1i	$$⊢S\in V\to \mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\in \mathrm{Top}$$
28		prfi	$$⊢\left\{S,\left\{𝒫\bigcup S\right\}\right\}\in \mathrm{Fin}$$
29		pwfi	$$⊢\left\{S,\left\{𝒫\bigcup S\right\}\right\}\in \mathrm{Fin}\leftrightarrow 𝒫\left\{S,\left\{𝒫\bigcup S\right\}\right\}\in \mathrm{Fin}$$
30	28 29	mpbi	$$⊢𝒫\left\{S,\left\{𝒫\bigcup S\right\}\right\}\in \mathrm{Fin}$$
31		tgdom	$$⊢\left\{S,\left\{𝒫\bigcup S\right\}\right\}\in \mathrm{V}\to \mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\preccurlyeq 𝒫\left\{S,\left\{𝒫\bigcup S\right\}\right\}$$
32	1 31	ax-mp	$$⊢\mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\preccurlyeq 𝒫\left\{S,\left\{𝒫\bigcup S\right\}\right\}$$
33		domfi	$$⊢\left(𝒫\left\{S,\left\{𝒫\bigcup S\right\}\right\}\in \mathrm{Fin}\wedge \mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\preccurlyeq 𝒫\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\to \mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\in \mathrm{Fin}$$
34	30 32 33	mp2an	$$⊢\mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\in \mathrm{Fin}$$
35	34	a1i	$$⊢S\in V\to \mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\in \mathrm{Fin}$$
36	27 35	elind	$$⊢S\in V\to \mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\in \left(\mathrm{Top}\cap \mathrm{Fin}\right)$$
37		fincmp	$$⊢\mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\in \left(\mathrm{Top}\cap \mathrm{Fin}\right)\to \mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\in \mathrm{Comp}$$
38	36 37	syl	$$⊢S\in V\to \mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\in \mathrm{Comp}$$