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	\|- ( ( ph /\ x e. I ) -> S e. V )
	kelac2.z	\|- ( ( ph /\ x e. I ) -> S =/= (/) )
	kelac2.k	\|- ( ph -> ( Xt_ ` ( x e. I \|-> ( topGen ` { S , { ~P U. S } } ) ) ) e. Comp )
Assertion	kelac2	\|- ( ph -> X_ x e. I S =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		kelac2.s	\|- ( ( ph /\ x e. I ) -> S e. V )
2		kelac2.z	\|- ( ( ph /\ x e. I ) -> S =/= (/) )
3		kelac2.k	\|- ( ph -> ( Xt_ ` ( x e. I \|-> ( topGen ` { S , { ~P U. S } } ) ) ) e. Comp )
4		kelac2lem	\|- ( S e. V -> ( topGen ` { S , { ~P U. S } } ) e. Comp )
5		cmptop	\|- ( ( topGen ` { S , { ~P U. S } } ) e. Comp -> ( topGen ` { S , { ~P U. S } } ) e. Top )
6	1 4 5	3syl	\|- ( ( ph /\ x e. I ) -> ( topGen ` { S , { ~P U. S } } ) e. Top )
7		uncom	\|- ( S u. { ~P U. S } ) = ( { ~P U. S } u. S )
8	7	difeq1i	\|- ( ( S u. { ~P U. S } ) \ S ) = ( ( { ~P U. S } u. S ) \ S )
9		difun2	\|- ( ( { ~P U. S } u. S ) \ S ) = ( { ~P U. S } \ S )
10	8 9	eqtri	\|- ( ( S u. { ~P U. S } ) \ S ) = ( { ~P U. S } \ S )
11		snex	\|- { ~P U. S } e. _V
12		uniprg	\|- ( ( S e. V /\ { ~P U. S } e. _V ) -> U. { S , { ~P U. S } } = ( S u. { ~P U. S } ) )
13	1 11 12	sylancl	\|- ( ( ph /\ x e. I ) -> U. { S , { ~P U. S } } = ( S u. { ~P U. S } ) )
14	13	difeq1d	\|- ( ( ph /\ x e. I ) -> ( U. { S , { ~P U. S } } \ S ) = ( ( S u. { ~P U. S } ) \ S ) )
15		incom	\|- ( { ~P U. S } i^i S ) = ( S i^i { ~P U. S } )
16		pwuninel	\|- -. ~P U. S e. S
17	16	a1i	\|- ( ( ph /\ x e. I ) -> -. ~P U. S e. S )
18		disjsn	\|- ( ( S i^i { ~P U. S } ) = (/) <-> -. ~P U. S e. S )
19	17 18	sylibr	\|- ( ( ph /\ x e. I ) -> ( S i^i { ~P U. S } ) = (/) )
20	15 19	eqtrid	\|- ( ( ph /\ x e. I ) -> ( { ~P U. S } i^i S ) = (/) )
21		disj3	\|- ( ( { ~P U. S } i^i S ) = (/) <-> { ~P U. S } = ( { ~P U. S } \ S ) )
22	20 21	sylib	\|- ( ( ph /\ x e. I ) -> { ~P U. S } = ( { ~P U. S } \ S ) )
23	10 14 22	3eqtr4a	\|- ( ( ph /\ x e. I ) -> ( U. { S , { ~P U. S } } \ S ) = { ~P U. S } )
24		prex	\|- { S , { ~P U. S } } e. _V
25		bastg	\|- ( { S , { ~P U. S } } e. _V -> { S , { ~P U. S } } C_ ( topGen ` { S , { ~P U. S } } ) )
26	24 25	mp1i	\|- ( ( ph /\ x e. I ) -> { S , { ~P U. S } } C_ ( topGen ` { S , { ~P U. S } } ) )
27	11	prid2	\|- { ~P U. S } e. { S , { ~P U. S } }
28	27	a1i	\|- ( ( ph /\ x e. I ) -> { ~P U. S } e. { S , { ~P U. S } } )
29	26 28	sseldd	\|- ( ( ph /\ x e. I ) -> { ~P U. S } e. ( topGen ` { S , { ~P U. S } } ) )
30	23 29	eqeltrd	\|- ( ( ph /\ x e. I ) -> ( U. { S , { ~P U. S } } \ S ) e. ( topGen ` { S , { ~P U. S } } ) )
31		prid1g	\|- ( S e. V -> S e. { S , { ~P U. S } } )
32		elssuni	\|- ( S e. { S , { ~P U. S } } -> S C_ U. { S , { ~P U. S } } )
33	1 31 32	3syl	\|- ( ( ph /\ x e. I ) -> S C_ U. { S , { ~P U. S } } )
34		unitg	\|- ( { S , { ~P U. S } } e. _V -> U. ( topGen ` { S , { ~P U. S } } ) = U. { S , { ~P U. S } } )
35	24 34	ax-mp	\|- U. ( topGen ` { S , { ~P U. S } } ) = U. { S , { ~P U. S } }
36	35	eqcomi	\|- U. { S , { ~P U. S } } = U. ( topGen ` { S , { ~P U. S } } )
37	36	iscld2	\|- ( ( ( topGen ` { S , { ~P U. S } } ) e. Top /\ S C_ U. { S , { ~P U. S } } ) -> ( S e. ( Clsd ` ( topGen ` { S , { ~P U. S } } ) ) <-> ( U. { S , { ~P U. S } } \ S ) e. ( topGen ` { S , { ~P U. S } } ) ) )
38	6 33 37	syl2anc	\|- ( ( ph /\ x e. I ) -> ( S e. ( Clsd ` ( topGen ` { S , { ~P U. S } } ) ) <-> ( U. { S , { ~P U. S } } \ S ) e. ( topGen ` { S , { ~P U. S } } ) ) )
39	30 38	mpbird	\|- ( ( ph /\ x e. I ) -> S e. ( Clsd ` ( topGen ` { S , { ~P U. S } } ) ) )
40		f1oi	\|- ( _I \|` S ) : S -1-1-onto-> S
41	40	a1i	\|- ( ( ph /\ x e. I ) -> ( _I \|` S ) : S -1-1-onto-> S )
42		elssuni	\|- ( { ~P U. S } e. { S , { ~P U. S } } -> { ~P U. S } C_ U. { S , { ~P U. S } } )
43	27 42	mp1i	\|- ( ( ph /\ x e. I ) -> { ~P U. S } C_ U. { S , { ~P U. S } } )
44		uniexg	\|- ( S e. V -> U. S e. _V )
45		pwexg	\|- ( U. S e. _V -> ~P U. S e. _V )
46		snidg	\|- ( ~P U. S e. _V -> ~P U. S e. { ~P U. S } )
47	1 44 45 46	4syl	\|- ( ( ph /\ x e. I ) -> ~P U. S e. { ~P U. S } )
48	43 47	sseldd	\|- ( ( ph /\ x e. I ) -> ~P U. S e. U. { S , { ~P U. S } } )
49	48 35	eleqtrrdi	\|- ( ( ph /\ x e. I ) -> ~P U. S e. U. ( topGen ` { S , { ~P U. S } } ) )
50	2 6 39 41 49 3	kelac1	\|- ( ph -> X_ x e. I S =/= (/) )

Metamath Proof Explorer

Theorem kelac2

Proof