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 = J
Assertion iskgen3 J ran 𝑘Gen J Top x 𝒫 X k 𝒫 X J 𝑡 k Comp x k J 𝑡 k x J

Proof

Step Hyp Ref Expression
1 iskgen3.1 X = J
2 iskgen2 J ran 𝑘Gen J Top 𝑘Gen J J
3 1 toptopon J Top J TopOn X
4 elkgen J TopOn X x 𝑘Gen J x X k 𝒫 X J 𝑡 k Comp x k J 𝑡 k
5 3 4 sylbi J Top x 𝑘Gen J x X k 𝒫 X J 𝑡 k Comp x k J 𝑡 k
6 vex x V
7 6 elpw x 𝒫 X x X
8 7 anbi1i x 𝒫 X k 𝒫 X J 𝑡 k Comp x k J 𝑡 k x X k 𝒫 X J 𝑡 k Comp x k J 𝑡 k
9 5 8 bitr4di J Top x 𝑘Gen J x 𝒫 X k 𝒫 X J 𝑡 k Comp x k J 𝑡 k
10 9 imbi1d J Top x 𝑘Gen J x J x 𝒫 X k 𝒫 X J 𝑡 k Comp x k J 𝑡 k x J
11 impexp x 𝒫 X k 𝒫 X J 𝑡 k Comp x k J 𝑡 k x J x 𝒫 X k 𝒫 X J 𝑡 k Comp x k J 𝑡 k x J
12 10 11 bitrdi J Top x 𝑘Gen J x J x 𝒫 X k 𝒫 X J 𝑡 k Comp x k J 𝑡 k x J
13 12 albidv J Top x x 𝑘Gen J x J x x 𝒫 X k 𝒫 X J 𝑡 k Comp x k J 𝑡 k x J
14 dfss2 𝑘Gen J J x x 𝑘Gen J x J
15 df-ral x 𝒫 X k 𝒫 X J 𝑡 k Comp x k J 𝑡 k x J x x 𝒫 X k 𝒫 X J 𝑡 k Comp x k J 𝑡 k x J
16 13 14 15 3bitr4g J Top 𝑘Gen J J x 𝒫 X k 𝒫 X J 𝑡 k Comp x k J 𝑡 k x J
17 16 pm5.32i J Top 𝑘Gen J J J Top x 𝒫 X k 𝒫 X J 𝑡 k Comp x k J 𝑡 k x J
18 2 17 bitri J ran 𝑘Gen J Top x 𝒫 X k 𝒫 X J 𝑡 k Comp x k J 𝑡 k x J