Metamath Proof Explorer

Theorem iskgen3

Description: Derive the usual definition of "compactly generated". A topology is compactly generated if every subset of X that is open in every compact subset is open. (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Hypothesis iskgen3.1 
|- X = U. J
Assertion iskgen3 
|- ( J e. ran kGen <-> ( J e. Top /\ A. x e. ~P X ( A. k e. ~P X ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) -> x e. J ) ) )

Proof

Step Hyp Ref Expression
1 iskgen3.1 
 |-  X = U. J
2 iskgen2 
 |-  ( J e. ran kGen <-> ( J e. Top /\ ( kGen ` J ) C_ J ) )
3 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
4 elkgen 
 |-  ( J e. ( TopOn ` X ) -> ( x e. ( kGen ` J ) <-> ( x C_ X /\ A. k e. ~P X ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) ) ) )
5 3 4 sylbi 
 |-  ( J e. Top -> ( x e. ( kGen ` J ) <-> ( x C_ X /\ A. k e. ~P X ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) ) ) )
6 vex 
 |-  x e. _V
7 6 elpw 
 |-  ( x e. ~P X <-> x C_ X )
8 7 anbi1i 
 |-  ( ( x e. ~P X /\ A. k e. ~P X ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) ) <-> ( x C_ X /\ A. k e. ~P X ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) ) )
9 5 8 bitr4di 
 |-  ( J e. Top -> ( x e. ( kGen ` J ) <-> ( x e. ~P X /\ A. k e. ~P X ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) ) ) )
10 9 imbi1d 
 |-  ( J e. Top -> ( ( x e. ( kGen ` J ) -> x e. J ) <-> ( ( x e. ~P X /\ A. k e. ~P X ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) ) -> x e. J ) ) )
11 impexp 
 |-  ( ( ( x e. ~P X /\ A. k e. ~P X ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) ) -> x e. J ) <-> ( x e. ~P X -> ( A. k e. ~P X ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) -> x e. J ) ) )
12 10 11 bitrdi 
 |-  ( J e. Top -> ( ( x e. ( kGen ` J ) -> x e. J ) <-> ( x e. ~P X -> ( A. k e. ~P X ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) -> x e. J ) ) ) )
13 12 albidv 
 |-  ( J e. Top -> ( A. x ( x e. ( kGen ` J ) -> x e. J ) <-> A. x ( x e. ~P X -> ( A. k e. ~P X ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) -> x e. J ) ) ) )
14 dfss2 
 |-  ( ( kGen ` J ) C_ J <-> A. x ( x e. ( kGen ` J ) -> x e. J ) )
15 df-ral 
 |-  ( A. x e. ~P X ( A. k e. ~P X ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) -> x e. J ) <-> A. x ( x e. ~P X -> ( A. k e. ~P X ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) -> x e. J ) ) )
16 13 14 15 3bitr4g 
 |-  ( J e. Top -> ( ( kGen ` J ) C_ J <-> A. x e. ~P X ( A. k e. ~P X ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) -> x e. J ) ) )
17 16 pm5.32i 
 |-  ( ( J e. Top /\ ( kGen ` J ) C_ J ) <-> ( J e. Top /\ A. x e. ~P X ( A. k e. ~P X ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) -> x e. J ) ) )
18 2 17 bitri 
 |-  ( J e. ran kGen <-> ( J e. Top /\ A. x e. ~P X ( A. k e. ~P X ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) -> x e. J ) ) )