This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )