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