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

Metamath Proof Explorer

Theorem elkgen

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

Ref Expression
Assertion elkgen ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝐴 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 kgenval ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝑘Gen ‘ 𝐽 ) = { 𝑥 ∈ 𝒫 𝑋 ∣ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) } )
2 1 eleq2d ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ↔ 𝐴 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) } ) )
3 ineq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∩ 𝑘 ) = ( 𝐴 ∩ 𝑘 ) )
4 3 eleq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ↔ ( 𝐴 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) )
5 4 imbi2d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ↔ ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝐴 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) )
6 5 ralbidv ⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ↔ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝐴 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) )
7 6 elrab ⊢ ( 𝐴 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) } ↔ ( 𝐴 ∈ 𝒫 𝑋 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝐴 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) )
8 toponmax ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
9 elpw2g ⊢ ( 𝑋 ∈ 𝐽 → ( 𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋 ) )
10 8 9 syl ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋 ) )
11 10 anbi1d ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ( 𝐴 ∈ 𝒫 𝑋 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝐴 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝐴 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) ) )
12 7 11 bitrid ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐴 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) } ↔ ( 𝐴 ⊆ 𝑋 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝐴 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) ) )
13 2 12 bitrd ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝐴 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) ) )