Metamath Proof Explorer

Theorem elkgen

Description: Value of the compact generator. (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Assertion elkgen ⊢ J ∈ TopOn ⁡ X → A ∈ 𝑘Gen ⁡ J ↔ A ⊆ X ∧ ∀ k ∈ 𝒫 X J ↾ 𝑡 k ∈ Comp → A ∩ k ∈ J ↾ 𝑡 k

Proof

Step Hyp Ref Expression
1 kgenval ⊢ J ∈ TopOn ⁡ X → 𝑘Gen ⁡ J = x ∈ 𝒫 X | ∀ k ∈ 𝒫 X J ↾ 𝑡 k ∈ Comp → x ∩ k ∈ J ↾ 𝑡 k
2 1 eleq2d ⊢ J ∈ TopOn ⁡ X → A ∈ 𝑘Gen ⁡ J ↔ A ∈ x ∈ 𝒫 X | ∀ k ∈ 𝒫 X J ↾ 𝑡 k ∈ Comp → x ∩ k ∈ J ↾ 𝑡 k
3 ineq1 ⊢ x = A → x ∩ k = A ∩ k
4 3 eleq1d ⊢ x = A → x ∩ k ∈ J ↾ 𝑡 k ↔ A ∩ k ∈ J ↾ 𝑡 k
5 4 imbi2d ⊢ x = A → J ↾ 𝑡 k ∈ Comp → x ∩ k ∈ J ↾ 𝑡 k ↔ J ↾ 𝑡 k ∈ Comp → A ∩ k ∈ J ↾ 𝑡 k
6 5 ralbidv ⊢ x = A → ∀ k ∈ 𝒫 X J ↾ 𝑡 k ∈ Comp → x ∩ k ∈ J ↾ 𝑡 k ↔ ∀ k ∈ 𝒫 X J ↾ 𝑡 k ∈ Comp → A ∩ k ∈ J ↾ 𝑡 k
7 6 elrab ⊢ A ∈ x ∈ 𝒫 X | ∀ k ∈ 𝒫 X J ↾ 𝑡 k ∈ Comp → x ∩ k ∈ J ↾ 𝑡 k ↔ A ∈ 𝒫 X ∧ ∀ k ∈ 𝒫 X J ↾ 𝑡 k ∈ Comp → A ∩ k ∈ J ↾ 𝑡 k
8 toponmax ⊢ J ∈ TopOn ⁡ X → X ∈ J
9 elpw2g ⊢ X ∈ J → A ∈ 𝒫 X ↔ A ⊆ X
10 8 9 syl ⊢ J ∈ TopOn ⁡ X → A ∈ 𝒫 X ↔ A ⊆ X
11 10 anbi1d ⊢ J ∈ TopOn ⁡ X → A ∈ 𝒫 X ∧ ∀ k ∈ 𝒫 X J ↾ 𝑡 k ∈ Comp → A ∩ k ∈ J ↾ 𝑡 k ↔ A ⊆ X ∧ ∀ k ∈ 𝒫 X J ↾ 𝑡 k ∈ Comp → A ∩ k ∈ J ↾ 𝑡 k
12 7 11 syl5bb ⊢ J ∈ TopOn ⁡ X → A ∈ x ∈ 𝒫 X | ∀ k ∈ 𝒫 X J ↾ 𝑡 k ∈ Comp → x ∩ k ∈ J ↾ 𝑡 k ↔ A ⊆ X ∧ ∀ k ∈ 𝒫 X J ↾ 𝑡 k ∈ Comp → A ∩ k ∈ J ↾ 𝑡 k
13 2 12 bitrd ⊢ J ∈ TopOn ⁡ X → A ∈ 𝑘Gen ⁡ J ↔ A ⊆ X ∧ ∀ k ∈ 𝒫 X J ↾ 𝑡 k ∈ Comp → A ∩ k ∈ J ↾ 𝑡 k