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	syl5bb	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐴 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) } ↔ ( 𝐴 ⊆ 𝑋 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝐴 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) ) )
13	2 12	bitrd	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝐴 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) ) )