Metamath Proof Explorer

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 
|- ( ( 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 syl5eq 
 |-  ( ( 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 =/= (/) )