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

Metamath Proof Explorer

Theorem kgenidm

Description: The compact generator is idempotent on compactly generated spaces. (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Assertion kgenidm ( 𝐽 ∈ ran 𝑘Gen → ( 𝑘Gen ‘ 𝐽 ) = 𝐽 )

Proof

Step Hyp Ref Expression
1 kgenf ⊢ 𝑘Gen : Top ⟶ Top
2 ffn ⊢ ( 𝑘Gen : Top ⟶ Top → 𝑘Gen Fn Top )
3 fvelrnb ⊢ ( 𝑘Gen Fn Top → ( 𝐽 ∈ ran 𝑘Gen ↔ ∃ 𝑗 ∈ Top ( 𝑘Gen ‘ 𝑗 ) = 𝐽 ) )
4 1 2 3 mp2b ⊢ ( 𝐽 ∈ ran 𝑘Gen ↔ ∃ 𝑗 ∈ Top ( 𝑘Gen ‘ 𝑗 ) = 𝐽 )
5 toptopon2 ⊢ ( 𝑗 ∈ Top ↔ 𝑗 ∈ ( TopOn ‘ ∪ 𝑗 ) )
6 kgentopon ⊢ ( 𝑗 ∈ ( TopOn ‘ ∪ 𝑗 ) → ( 𝑘Gen ‘ 𝑗 ) ∈ ( TopOn ‘ ∪ 𝑗 ) )
7 5 6 sylbi ⊢ ( 𝑗 ∈ Top → ( 𝑘Gen ‘ 𝑗 ) ∈ ( TopOn ‘ ∪ 𝑗 ) )
8 kgentopon ⊢ ( ( 𝑘Gen ‘ 𝑗 ) ∈ ( TopOn ‘ ∪ 𝑗 ) → ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) ∈ ( TopOn ‘ ∪ 𝑗 ) )
9 7 8 syl ⊢ ( 𝑗 ∈ Top → ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) ∈ ( TopOn ‘ ∪ 𝑗 ) )
10 toponss ⊢ ( ( ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) ∈ ( TopOn ‘ ∪ 𝑗 ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) ) → 𝑥 ⊆ ∪ 𝑗 )
11 9 10 sylan ⊢ ( ( 𝑗 ∈ Top ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) ) → 𝑥 ⊆ ∪ 𝑗 )
12 simplr ⊢ ( ( ( 𝑗 ∈ Top ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑗 ∧ ( 𝑗 ↾t 𝑘 ) ∈ Comp ) ) → 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) )
13 kgencmp2 ⊢ ( 𝑗 ∈ Top → ( ( 𝑗 ↾t 𝑘 ) ∈ Comp ↔ ( ( 𝑘Gen ‘ 𝑗 ) ↾t 𝑘 ) ∈ Comp ) )
14 13 biimpa ⊢ ( ( 𝑗 ∈ Top ∧ ( 𝑗 ↾t 𝑘 ) ∈ Comp ) → ( ( 𝑘Gen ‘ 𝑗 ) ↾t 𝑘 ) ∈ Comp )
15 14 ad2ant2rl ⊢ ( ( ( 𝑗 ∈ Top ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑗 ∧ ( 𝑗 ↾t 𝑘 ) ∈ Comp ) ) → ( ( 𝑘Gen ‘ 𝑗 ) ↾t 𝑘 ) ∈ Comp )
16 kgeni ⊢ ( ( 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) ∧ ( ( 𝑘Gen ‘ 𝑗 ) ↾t 𝑘 ) ∈ Comp ) → ( 𝑥 ∩ 𝑘 ) ∈ ( ( 𝑘Gen ‘ 𝑗 ) ↾t 𝑘 ) )
17 12 15 16 syl2anc ⊢ ( ( ( 𝑗 ∈ Top ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑗 ∧ ( 𝑗 ↾t 𝑘 ) ∈ Comp ) ) → ( 𝑥 ∩ 𝑘 ) ∈ ( ( 𝑘Gen ‘ 𝑗 ) ↾t 𝑘 ) )
18 kgencmp ⊢ ( ( 𝑗 ∈ Top ∧ ( 𝑗 ↾t 𝑘 ) ∈ Comp ) → ( 𝑗 ↾t 𝑘 ) = ( ( 𝑘Gen ‘ 𝑗 ) ↾t 𝑘 ) )
19 18 ad2ant2rl ⊢ ( ( ( 𝑗 ∈ Top ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑗 ∧ ( 𝑗 ↾t 𝑘 ) ∈ Comp ) ) → ( 𝑗 ↾t 𝑘 ) = ( ( 𝑘Gen ‘ 𝑗 ) ↾t 𝑘 ) )
20 17 19 eleqtrrd ⊢ ( ( ( 𝑗 ∈ Top ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑗 ∧ ( 𝑗 ↾t 𝑘 ) ∈ Comp ) ) → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝑗 ↾t 𝑘 ) )
21 20 expr ⊢ ( ( ( 𝑗 ∈ Top ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ 𝒫 ∪ 𝑗 ) → ( ( 𝑗 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝑗 ↾t 𝑘 ) ) )
22 21 ralrimiva ⊢ ( ( 𝑗 ∈ Top ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) ) → ∀ 𝑘 ∈ 𝒫 ∪ 𝑗 ( ( 𝑗 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝑗 ↾t 𝑘 ) ) )
23 simpl ⊢ ( ( 𝑗 ∈ Top ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) ) → 𝑗 ∈ Top )
24 23 5 sylib ⊢ ( ( 𝑗 ∈ Top ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) ) → 𝑗 ∈ ( TopOn ‘ ∪ 𝑗 ) )
25 elkgen ⊢ ( 𝑗 ∈ ( TopOn ‘ ∪ 𝑗 ) → ( 𝑥 ∈ ( 𝑘Gen ‘ 𝑗 ) ↔ ( 𝑥 ⊆ ∪ 𝑗 ∧ ∀ 𝑘 ∈ 𝒫 ∪ 𝑗 ( ( 𝑗 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝑗 ↾t 𝑘 ) ) ) ) )
26 24 25 syl ⊢ ( ( 𝑗 ∈ Top ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) ) → ( 𝑥 ∈ ( 𝑘Gen ‘ 𝑗 ) ↔ ( 𝑥 ⊆ ∪ 𝑗 ∧ ∀ 𝑘 ∈ 𝒫 ∪ 𝑗 ( ( 𝑗 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝑗 ↾t 𝑘 ) ) ) ) )
27 11 22 26 mpbir2and ⊢ ( ( 𝑗 ∈ Top ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) ) → 𝑥 ∈ ( 𝑘Gen ‘ 𝑗 ) )
28 27 ex ⊢ ( 𝑗 ∈ Top → ( 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) → 𝑥 ∈ ( 𝑘Gen ‘ 𝑗 ) ) )
29 28 ssrdv ⊢ ( 𝑗 ∈ Top → ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) ⊆ ( 𝑘Gen ‘ 𝑗 ) )
30 fveq2 ⊢ ( ( 𝑘Gen ‘ 𝑗 ) = 𝐽 → ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) = ( 𝑘Gen ‘ 𝐽 ) )
31 id ⊢ ( ( 𝑘Gen ‘ 𝑗 ) = 𝐽 → ( 𝑘Gen ‘ 𝑗 ) = 𝐽 )
32 30 31 sseq12d ⊢ ( ( 𝑘Gen ‘ 𝑗 ) = 𝐽 → ( ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) ⊆ ( 𝑘Gen ‘ 𝑗 ) ↔ ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 ) )
33 29 32 syl5ibcom ⊢ ( 𝑗 ∈ Top → ( ( 𝑘Gen ‘ 𝑗 ) = 𝐽 → ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 ) )
34 33 rexlimiv ⊢ ( ∃ 𝑗 ∈ Top ( 𝑘Gen ‘ 𝑗 ) = 𝐽 → ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 )
35 4 34 sylbi ⊢ ( 𝐽 ∈ ran 𝑘Gen → ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 )
36 kgentop ⊢ ( 𝐽 ∈ ran 𝑘Gen → 𝐽 ∈ Top )
37 kgenss ⊢ ( 𝐽 ∈ Top → 𝐽 ⊆ ( 𝑘Gen ‘ 𝐽 ) )
38 36 37 syl ⊢ ( 𝐽 ∈ ran 𝑘Gen → 𝐽 ⊆ ( 𝑘Gen ‘ 𝐽 ) )
39 35 38 eqssd ⊢ ( 𝐽 ∈ ran 𝑘Gen → ( 𝑘Gen ‘ 𝐽 ) = 𝐽 )