Theorem iskgen3

Description: Derive the usual definition of "compactly generated". A topology is compactly generated if every subset of X that is open in every compact subset is open. (Contributed by Mario Carneiro, 20-Mar-2015)

	Ref	Expression
Hypothesis	iskgen3.1	⊢ 𝑋 = ∪ 𝐽
Assertion	iskgen3	⊢ ( 𝐽 ∈ ran 𝑘Gen ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) → 𝑥 ∈ 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		iskgen3.1	⊢ 𝑋 = ∪ 𝐽
2		iskgen2	⊢ ( 𝐽 ∈ ran 𝑘Gen ↔ ( 𝐽 ∈ Top ∧ ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 ) )
3	1	toptopon	⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4		elkgen	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) ) )
5	3 4	sylbi	⊢ ( 𝐽 ∈ Top → ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) ) )
6		vex	⊢ 𝑥 ∈ V
7	6	elpw	⊢ ( 𝑥 ∈ 𝒫 𝑋 ↔ 𝑥 ⊆ 𝑋 )
8	7	anbi1i	⊢ ( ( 𝑥 ∈ 𝒫 𝑋 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) )
9	5 8	bitr4di	⊢ ( 𝐽 ∈ Top → ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ↔ ( 𝑥 ∈ 𝒫 𝑋 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) ) )
10	9	imbi1d	⊢ ( 𝐽 ∈ Top → ( ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) → 𝑥 ∈ 𝐽 ) ↔ ( ( 𝑥 ∈ 𝒫 𝑋 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) → 𝑥 ∈ 𝐽 ) ) )
11		impexp	⊢ ( ( ( 𝑥 ∈ 𝒫 𝑋 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) → 𝑥 ∈ 𝐽 ) ↔ ( 𝑥 ∈ 𝒫 𝑋 → ( ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) → 𝑥 ∈ 𝐽 ) ) )
12	10 11	bitrdi	⊢ ( 𝐽 ∈ Top → ( ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) → 𝑥 ∈ 𝐽 ) ↔ ( 𝑥 ∈ 𝒫 𝑋 → ( ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) → 𝑥 ∈ 𝐽 ) ) ) )
13	12	albidv	⊢ ( 𝐽 ∈ Top → ( ∀ 𝑥 ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) → 𝑥 ∈ 𝐽 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝒫 𝑋 → ( ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) → 𝑥 ∈ 𝐽 ) ) ) )
14		df-ss	⊢ ( ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 ↔ ∀ 𝑥 ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) → 𝑥 ∈ 𝐽 ) )
15		df-ral	⊢ ( ∀ 𝑥 ∈ 𝒫 𝑋 ( ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) → 𝑥 ∈ 𝐽 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝒫 𝑋 → ( ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) → 𝑥 ∈ 𝐽 ) ) )
16	13 14 15	3bitr4g	⊢ ( 𝐽 ∈ Top → ( ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 ↔ ∀ 𝑥 ∈ 𝒫 𝑋 ( ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) → 𝑥 ∈ 𝐽 ) ) )
17	16	pm5.32i	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 ) ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) → 𝑥 ∈ 𝐽 ) ) )
18	2 17	bitri	⊢ ( 𝐽 ∈ ran 𝑘Gen ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) → 𝑥 ∈ 𝐽 ) ) )