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 5 birani ⊢ ( ( 𝑗 ∈ Top ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) ) → 𝑗 ∈ ( TopOn ‘ ∪ 𝑗 ) )
24 elkgen ⊢ ( 𝑗 ∈ ( TopOn ‘ ∪ 𝑗 ) → ( 𝑥 ∈ ( 𝑘Gen ‘ 𝑗 ) ↔ ( 𝑥 ⊆ ∪ 𝑗 ∧ ∀ 𝑘 ∈ 𝒫 ∪ 𝑗 ( ( 𝑗 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝑗 ↾t 𝑘 ) ) ) ) )
25 23 24 syl ⊢ ( ( 𝑗 ∈ Top ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) ) → ( 𝑥 ∈ ( 𝑘Gen ‘ 𝑗 ) ↔ ( 𝑥 ⊆ ∪ 𝑗 ∧ ∀ 𝑘 ∈ 𝒫 ∪ 𝑗 ( ( 𝑗 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝑗 ↾t 𝑘 ) ) ) ) )
26 11 22 25 mpbir2and ⊢ ( ( 𝑗 ∈ Top ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) ) → 𝑥 ∈ ( 𝑘Gen ‘ 𝑗 ) )
27 26 ex ⊢ ( 𝑗 ∈ Top → ( 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) → 𝑥 ∈ ( 𝑘Gen ‘ 𝑗 ) ) )
28 27 ssrdv ⊢ ( 𝑗 ∈ Top → ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) ⊆ ( 𝑘Gen ‘ 𝑗 ) )
29 fveq2 ⊢ ( ( 𝑘Gen ‘ 𝑗 ) = 𝐽 → ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) = ( 𝑘Gen ‘ 𝐽 ) )
30 id ⊢ ( ( 𝑘Gen ‘ 𝑗 ) = 𝐽 → ( 𝑘Gen ‘ 𝑗 ) = 𝐽 )
31 29 30 sseq12d ⊢ ( ( 𝑘Gen ‘ 𝑗 ) = 𝐽 → ( ( 𝑘Gen ‘ ( 𝑘Gen ‘ 𝑗 ) ) ⊆ ( 𝑘Gen ‘ 𝑗 ) ↔ ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 ) )
32 28 31 syl5ibcom ⊢ ( 𝑗 ∈ Top → ( ( 𝑘Gen ‘ 𝑗 ) = 𝐽 → ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 ) )
33 32 rexlimiv ⊢ ( ∃ 𝑗 ∈ Top ( 𝑘Gen ‘ 𝑗 ) = 𝐽 → ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 )
34 4 33 sylbi ⊢ ( 𝐽 ∈ ran 𝑘Gen → ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 )
35 kgentop ⊢ ( 𝐽 ∈ ran 𝑘Gen → 𝐽 ∈ Top )
36 kgenss ⊢ ( 𝐽 ∈ Top → 𝐽 ⊆ ( 𝑘Gen ‘ 𝐽 ) )
37 35 36 syl ⊢ ( 𝐽 ∈ ran 𝑘Gen → 𝐽 ⊆ ( 𝑘Gen ‘ 𝐽 ) )
38 34 37 eqssd ⊢ ( 𝐽 ∈ ran 𝑘Gen → ( 𝑘Gen ‘ 𝐽 ) = 𝐽 )