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 𝑘 ) ) } )