Theorem kelac2

Description: Kelley's choice, most common form: compactness of a product of knob topologies recovers choice. (Contributed by Stefan O'Rear, 22-Feb-2015)

	Ref	Expression
Hypotheses	kelac2.s	$$⊢\left(\phi \wedge x\in I\right)\to S\in V$$
	kelac2.z	$$⊢\left(\phi \wedge x\in I\right)\to S\ne \varnothing$$
	kelac2.k	$$⊢\phi \to {\prod }_{𝑡}\left(\left(x\in I⟼\mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\right)\right)\in \mathrm{Comp}$$
Assertion	kelac2	$$⊢\phi \to \underset{x\in I}{⨉}S\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		kelac2.s	$$⊢\left(\phi \wedge x\in I\right)\to S\in V$$
2		kelac2.z	$$⊢\left(\phi \wedge x\in I\right)\to S\ne \varnothing$$
3		kelac2.k	$$⊢\phi \to {\prod }_{𝑡}\left(\left(x\in I⟼\mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\right)\right)\in \mathrm{Comp}$$
4		kelac2lem	$$⊢S\in V\to \mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\in \mathrm{Comp}$$
5		cmptop	$$⊢\mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\in \mathrm{Comp}\to \mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\in \mathrm{Top}$$
6	1 4 5	3syl	$$⊢\left(\phi \wedge x\in I\right)\to \mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\in \mathrm{Top}$$
7		uncom	$$⊢S\cup \left\{𝒫\bigcup S\right\}=\left\{𝒫\bigcup S\right\}\cup S$$
8	7	difeq1i	$$⊢\left(S\cup \left\{𝒫\bigcup S\right\}\right)\setminus S=\left(\left\{𝒫\bigcup S\right\}\cup S\right)\setminus S$$
9		difun2	$$⊢\left(\left\{𝒫\bigcup S\right\}\cup S\right)\setminus S=\left\{𝒫\bigcup S\right\}\setminus S$$
10	8 9	eqtri	$$⊢\left(S\cup \left\{𝒫\bigcup S\right\}\right)\setminus S=\left\{𝒫\bigcup S\right\}\setminus S$$
11		snex	$$⊢\left\{𝒫\bigcup S\right\}\in \mathrm{V}$$
12		uniprg	$$⊢\left(S\in V\wedge \left\{𝒫\bigcup S\right\}\in \mathrm{V}\right)\to \bigcup \left\{S,\left\{𝒫\bigcup S\right\}\right\}=S\cup \left\{𝒫\bigcup S\right\}$$
13	1 11 12	sylancl	$$⊢\left(\phi \wedge x\in I\right)\to \bigcup \left\{S,\left\{𝒫\bigcup S\right\}\right\}=S\cup \left\{𝒫\bigcup S\right\}$$
14	13	difeq1d	$$⊢\left(\phi \wedge x\in I\right)\to \bigcup \left\{S,\left\{𝒫\bigcup S\right\}\right\}\setminus S=\left(S\cup \left\{𝒫\bigcup S\right\}\right)\setminus S$$
15		incom	$$⊢\left\{𝒫\bigcup S\right\}\cap S=S\cap \left\{𝒫\bigcup S\right\}$$
16		pwuninel	$$⊢\neg 𝒫\bigcup S\in S$$
17	16	a1i	$$⊢\left(\phi \wedge x\in I\right)\to \neg 𝒫\bigcup S\in S$$
18		disjsn	$$⊢S\cap \left\{𝒫\bigcup S\right\}=\varnothing \leftrightarrow \neg 𝒫\bigcup S\in S$$
19	17 18	sylibr	$$⊢\left(\phi \wedge x\in I\right)\to S\cap \left\{𝒫\bigcup S\right\}=\varnothing$$
20	15 19	syl5eq	$$⊢\left(\phi \wedge x\in I\right)\to \left\{𝒫\bigcup S\right\}\cap S=\varnothing$$
21		disj3	$$⊢\left\{𝒫\bigcup S\right\}\cap S=\varnothing \leftrightarrow \left\{𝒫\bigcup S\right\}=\left\{𝒫\bigcup S\right\}\setminus S$$
22	20 21	sylib	$$⊢\left(\phi \wedge x\in I\right)\to \left\{𝒫\bigcup S\right\}=\left\{𝒫\bigcup S\right\}\setminus S$$
23	10 14 22	3eqtr4a	$$⊢\left(\phi \wedge x\in I\right)\to \bigcup \left\{S,\left\{𝒫\bigcup S\right\}\right\}\setminus S=\left\{𝒫\bigcup S\right\}$$
24		prex	$$⊢\left\{S,\left\{𝒫\bigcup S\right\}\right\}\in \mathrm{V}$$
25		bastg	$$⊢\left\{S,\left\{𝒫\bigcup S\right\}\right\}\in \mathrm{V}\to \left\{S,\left\{𝒫\bigcup S\right\}\right\}\subseteq \mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)$$
26	24 25	mp1i	$$⊢\left(\phi \wedge x\in I\right)\to \left\{S,\left\{𝒫\bigcup S\right\}\right\}\subseteq \mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)$$
27	11	prid2	$$⊢\left\{𝒫\bigcup S\right\}\in \left\{S,\left\{𝒫\bigcup S\right\}\right\}$$
28	27	a1i	$$⊢\left(\phi \wedge x\in I\right)\to \left\{𝒫\bigcup S\right\}\in \left\{S,\left\{𝒫\bigcup S\right\}\right\}$$
29	26 28	sseldd	$$⊢\left(\phi \wedge x\in I\right)\to \left\{𝒫\bigcup S\right\}\in \mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)$$
30	23 29	eqeltrd	$$⊢\left(\phi \wedge x\in I\right)\to \bigcup \left\{S,\left\{𝒫\bigcup S\right\}\right\}\setminus S\in \mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)$$
31		prid1g	$$⊢S\in V\to S\in \left\{S,\left\{𝒫\bigcup S\right\}\right\}$$
32		elssuni	$$⊢S\in \left\{S,\left\{𝒫\bigcup S\right\}\right\}\to S\subseteq \bigcup \left\{S,\left\{𝒫\bigcup S\right\}\right\}$$
33	1 31 32	3syl	$$⊢\left(\phi \wedge x\in I\right)\to S\subseteq \bigcup \left\{S,\left\{𝒫\bigcup S\right\}\right\}$$
34		unitg	$$⊢\left\{S,\left\{𝒫\bigcup S\right\}\right\}\in \mathrm{V}\to \bigcup \mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)=\bigcup \left\{S,\left\{𝒫\bigcup S\right\}\right\}$$
35	24 34	ax-mp	$$⊢\bigcup \mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)=\bigcup \left\{S,\left\{𝒫\bigcup S\right\}\right\}$$
36	35	eqcomi	$$⊢\bigcup \left\{S,\left\{𝒫\bigcup S\right\}\right\}=\bigcup \mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)$$
37	36	iscld2	$$⊢\left(\mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\in \mathrm{Top}\wedge S\subseteq \bigcup \left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\to \left(S\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\right)\leftrightarrow \bigcup \left\{S,\left\{𝒫\bigcup S\right\}\right\}\setminus S\in \mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\right)$$
38	6 33 37	syl2anc	$$⊢\left(\phi \wedge x\in I\right)\to \left(S\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\right)\leftrightarrow \bigcup \left\{S,\left\{𝒫\bigcup S\right\}\right\}\setminus S\in \mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\right)$$
39	30 38	mpbird	$$⊢\left(\phi \wedge x\in I\right)\to S\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)\right)$$
40		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_S\right):S\underset{1-1\; onto}{⟶}S$$
41	40	a1i	$$⊢\left(\phi \wedge x\in I\right)\to \left({\mathrm{I}\upharpoonright }_S\right):S\underset{1-1\; onto}{⟶}S$$
42		elssuni	$$⊢\left\{𝒫\bigcup S\right\}\in \left\{S,\left\{𝒫\bigcup S\right\}\right\}\to \left\{𝒫\bigcup S\right\}\subseteq \bigcup \left\{S,\left\{𝒫\bigcup S\right\}\right\}$$
43	27 42	mp1i	$$⊢\left(\phi \wedge x\in I\right)\to \left\{𝒫\bigcup S\right\}\subseteq \bigcup \left\{S,\left\{𝒫\bigcup S\right\}\right\}$$
44		uniexg	$$⊢S\in V\to \bigcup S\in \mathrm{V}$$
45		pwexg	$$⊢\bigcup S\in \mathrm{V}\to 𝒫\bigcup S\in \mathrm{V}$$
46		snidg	$$⊢𝒫\bigcup S\in \mathrm{V}\to 𝒫\bigcup S\in \left\{𝒫\bigcup S\right\}$$
47	1 44 45 46	4syl	$$⊢\left(\phi \wedge x\in I\right)\to 𝒫\bigcup S\in \left\{𝒫\bigcup S\right\}$$
48	43 47	sseldd	$$⊢\left(\phi \wedge x\in I\right)\to 𝒫\bigcup S\in \bigcup \left\{S,\left\{𝒫\bigcup S\right\}\right\}$$
49	48 35	eleqtrrdi	$$⊢\left(\phi \wedge x\in I\right)\to 𝒫\bigcup S\in \bigcup \mathrm{topGen}\left(\left\{S,\left\{𝒫\bigcup S\right\}\right\}\right)$$
50	2 6 39 41 49 3	kelac1	$$⊢\phi \to \underset{x\in I}{⨉}S\ne \varnothing$$