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

Metamath Proof Explorer

Theorem kgenval

Description: Value of the compact generator. (The "k" in kGen comes from the name "k-space" for these spaces, after the German word kompakt.) (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Assertion kgenval ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝑘Gen ‘ 𝐽 ) = { 𝑥 ∈ 𝒫 𝑋 ∣ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) } )

Proof

Step Hyp Ref Expression
1 df-kgen ⊢ 𝑘Gen = ( 𝑗 ∈ Top ↦ { 𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ∀ 𝑘 ∈ 𝒫 ∪ 𝑗 ( ( 𝑗 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝑗 ↾t 𝑘 ) ) } )
2 unieq ⊢ ( 𝑗 = 𝐽 → ∪ 𝑗 = ∪ 𝐽 )
3 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
4 3 eqcomd ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ∪ 𝐽 = 𝑋 )
5 2 4 sylan9eqr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑗 = 𝐽 ) → ∪ 𝑗 = 𝑋 )
6 5 pweqd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑗 = 𝐽 ) → 𝒫 ∪ 𝑗 = 𝒫 𝑋 )
7 oveq1 ⊢ ( 𝑗 = 𝐽 → ( 𝑗 ↾t 𝑘 ) = ( 𝐽 ↾t 𝑘 ) )
8 7 eleq1d ⊢ ( 𝑗 = 𝐽 → ( ( 𝑗 ↾t 𝑘 ) ∈ Comp ↔ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) )
9 7 eleq2d ⊢ ( 𝑗 = 𝐽 → ( ( 𝑥 ∩ 𝑘 ) ∈ ( 𝑗 ↾t 𝑘 ) ↔ ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) )
10 8 9 imbi12d ⊢ ( 𝑗 = 𝐽 → ( ( ( 𝑗 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝑗 ↾t 𝑘 ) ) ↔ ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) )
11 10 adantl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑗 = 𝐽 ) → ( ( ( 𝑗 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝑗 ↾t 𝑘 ) ) ↔ ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) )
12 6 11 raleqbidv ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑗 = 𝐽 ) → ( ∀ 𝑘 ∈ 𝒫 ∪ 𝑗 ( ( 𝑗 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝑗 ↾t 𝑘 ) ) ↔ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) )
13 6 12 rabeqbidv ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑗 = 𝐽 ) → { 𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ∀ 𝑘 ∈ 𝒫 ∪ 𝑗 ( ( 𝑗 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝑗 ↾t 𝑘 ) ) } = { 𝑥 ∈ 𝒫 𝑋 ∣ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) } )
14 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
15 toponmax ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
16 pwexg ⊢ ( 𝑋 ∈ 𝐽 → 𝒫 𝑋 ∈ V )
17 rabexg ⊢ ( 𝒫 𝑋 ∈ V → { 𝑥 ∈ 𝒫 𝑋 ∣ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) } ∈ V )
18 15 16 17 3syl ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → { 𝑥 ∈ 𝒫 𝑋 ∣ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) } ∈ V )
19 1 13 14 18 fvmptd2 ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝑘Gen ‘ 𝐽 ) = { 𝑥 ∈ 𝒫 𝑋 ∣ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) } )