Metamath Proof Explorer


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 e. V -> ( topGen ` { S , { ~P U. S } } ) e. Comp )

Proof

Step Hyp Ref Expression
1 prex
 |-  { S , { ~P U. S } } e. _V
2 vex
 |-  x e. _V
3 2 elpr
 |-  ( x e. { S , { ~P U. S } } <-> ( x = S \/ x = { ~P U. S } ) )
4 vex
 |-  y e. _V
5 4 elpr
 |-  ( y e. { S , { ~P U. S } } <-> ( y = S \/ y = { ~P U. S } ) )
6 eqtr3
 |-  ( ( x = S /\ y = S ) -> x = y )
7 6 orcd
 |-  ( ( x = S /\ y = S ) -> ( x = y \/ ( x i^i y ) = (/) ) )
8 ineq12
 |-  ( ( x = { ~P U. S } /\ y = S ) -> ( x i^i y ) = ( { ~P U. S } i^i S ) )
9 incom
 |-  ( { ~P U. S } i^i S ) = ( S i^i { ~P U. S } )
10 pwuninel
 |-  -. ~P U. S e. S
11 disjsn
 |-  ( ( S i^i { ~P U. S } ) = (/) <-> -. ~P U. S e. S )
12 10 11 mpbir
 |-  ( S i^i { ~P U. S } ) = (/)
13 9 12 eqtri
 |-  ( { ~P U. S } i^i S ) = (/)
14 8 13 eqtrdi
 |-  ( ( x = { ~P U. S } /\ y = S ) -> ( x i^i y ) = (/) )
15 14 olcd
 |-  ( ( x = { ~P U. S } /\ y = S ) -> ( x = y \/ ( x i^i y ) = (/) ) )
16 ineq12
 |-  ( ( x = S /\ y = { ~P U. S } ) -> ( x i^i y ) = ( S i^i { ~P U. S } ) )
17 16 12 eqtrdi
 |-  ( ( x = S /\ y = { ~P U. S } ) -> ( x i^i y ) = (/) )
18 17 olcd
 |-  ( ( x = S /\ y = { ~P U. S } ) -> ( x = y \/ ( x i^i y ) = (/) ) )
19 eqtr3
 |-  ( ( x = { ~P U. S } /\ y = { ~P U. S } ) -> x = y )
20 19 orcd
 |-  ( ( x = { ~P U. S } /\ y = { ~P U. S } ) -> ( x = y \/ ( x i^i y ) = (/) ) )
21 7 15 18 20 ccase
 |-  ( ( ( x = S \/ x = { ~P U. S } ) /\ ( y = S \/ y = { ~P U. S } ) ) -> ( x = y \/ ( x i^i y ) = (/) ) )
22 3 5 21 syl2anb
 |-  ( ( x e. { S , { ~P U. S } } /\ y e. { S , { ~P U. S } } ) -> ( x = y \/ ( x i^i y ) = (/) ) )
23 22 rgen2
 |-  A. x e. { S , { ~P U. S } } A. y e. { S , { ~P U. S } } ( x = y \/ ( x i^i y ) = (/) )
24 baspartn
 |-  ( ( { S , { ~P U. S } } e. _V /\ A. x e. { S , { ~P U. S } } A. y e. { S , { ~P U. S } } ( x = y \/ ( x i^i y ) = (/) ) ) -> { S , { ~P U. S } } e. TopBases )
25 1 23 24 mp2an
 |-  { S , { ~P U. S } } e. TopBases
26 tgcl
 |-  ( { S , { ~P U. S } } e. TopBases -> ( topGen ` { S , { ~P U. S } } ) e. Top )
27 25 26 mp1i
 |-  ( S e. V -> ( topGen ` { S , { ~P U. S } } ) e. Top )
28 prfi
 |-  { S , { ~P U. S } } e. Fin
29 pwfi
 |-  ( { S , { ~P U. S } } e. Fin <-> ~P { S , { ~P U. S } } e. Fin )
30 28 29 mpbi
 |-  ~P { S , { ~P U. S } } e. Fin
31 tgdom
 |-  ( { S , { ~P U. S } } e. _V -> ( topGen ` { S , { ~P U. S } } ) ~<_ ~P { S , { ~P U. S } } )
32 1 31 ax-mp
 |-  ( topGen ` { S , { ~P U. S } } ) ~<_ ~P { S , { ~P U. S } }
33 domfi
 |-  ( ( ~P { S , { ~P U. S } } e. Fin /\ ( topGen ` { S , { ~P U. S } } ) ~<_ ~P { S , { ~P U. S } } ) -> ( topGen ` { S , { ~P U. S } } ) e. Fin )
34 30 32 33 mp2an
 |-  ( topGen ` { S , { ~P U. S } } ) e. Fin
35 34 a1i
 |-  ( S e. V -> ( topGen ` { S , { ~P U. S } } ) e. Fin )
36 27 35 elind
 |-  ( S e. V -> ( topGen ` { S , { ~P U. S } } ) e. ( Top i^i Fin ) )
37 fincmp
 |-  ( ( topGen ` { S , { ~P U. S } } ) e. ( Top i^i Fin ) -> ( topGen ` { S , { ~P U. S } } ) e. Comp )
38 36 37 syl
 |-  ( S e. V -> ( topGen ` { S , { ~P U. S } } ) e. Comp )