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

Metamath Proof Explorer

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 𝑘 ) ) → 𝑥 ∈ 𝐽 ) ) )