Metamath Proof Explorer

Theorem kgen2ss

Description: The compact generator preserves the subset (fineness) relationship on topologies. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion kgen2ss ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → ( 𝑘Gen ‘ 𝐽 ) ⊆ ( 𝑘Gen ‘ 𝐾 ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 elpwi ⊢ ( 𝑘 ∈ 𝒫 𝑋 → 𝑘 ⊆ 𝑋 )
3 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑘 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝑘 ) ∈ ( TopOn ‘ 𝑘 ) )
4 1 2 3 syl2an ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → ( 𝐽 ↾t 𝑘 ) ∈ ( TopOn ‘ 𝑘 ) )
5 simp2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
6 resttopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑘 ⊆ 𝑋 ) → ( 𝐾 ↾t 𝑘 ) ∈ ( TopOn ‘ 𝑘 ) )
7 5 2 6 syl2an ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → ( 𝐾 ↾t 𝑘 ) ∈ ( TopOn ‘ 𝑘 ) )
8 toponuni ⊢ ( ( 𝐾 ↾t 𝑘 ) ∈ ( TopOn ‘ 𝑘 ) → 𝑘 = ∪ ( 𝐾 ↾t 𝑘 ) )
9 7 8 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → 𝑘 = ∪ ( 𝐾 ↾t 𝑘 ) )
10 9 fveq2d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → ( TopOn ‘ 𝑘 ) = ( TopOn ‘ ∪ ( 𝐾 ↾t 𝑘 ) ) )
11 4 10 eleqtrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → ( 𝐽 ↾t 𝑘 ) ∈ ( TopOn ‘ ∪ ( 𝐾 ↾t 𝑘 ) ) )
12 simpl2 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
13 topontop ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) → 𝐾 ∈ Top )
14 12 13 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → 𝐾 ∈ Top )
15 simpl3 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → 𝐽 ⊆ 𝐾 )
16 ssrest ⊢ ( ( 𝐾 ∈ Top ∧ 𝐽 ⊆ 𝐾 ) → ( 𝐽 ↾t 𝑘 ) ⊆ ( 𝐾 ↾t 𝑘 ) )
17 14 15 16 syl2anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → ( 𝐽 ↾t 𝑘 ) ⊆ ( 𝐾 ↾t 𝑘 ) )
18 eqid ⊢ ∪ ( 𝐾 ↾t 𝑘 ) = ∪ ( 𝐾 ↾t 𝑘 )
19 18 sscmp ⊢ ( ( ( 𝐽 ↾t 𝑘 ) ∈ ( TopOn ‘ ∪ ( 𝐾 ↾t 𝑘 ) ) ∧ ( 𝐾 ↾t 𝑘 ) ∈ Comp ∧ ( 𝐽 ↾t 𝑘 ) ⊆ ( 𝐾 ↾t 𝑘 ) ) → ( 𝐽 ↾t 𝑘 ) ∈ Comp )
20 19 3com23 ⊢ ( ( ( 𝐽 ↾t 𝑘 ) ∈ ( TopOn ‘ ∪ ( 𝐾 ↾t 𝑘 ) ) ∧ ( 𝐽 ↾t 𝑘 ) ⊆ ( 𝐾 ↾t 𝑘 ) ∧ ( 𝐾 ↾t 𝑘 ) ∈ Comp ) → ( 𝐽 ↾t 𝑘 ) ∈ Comp )
21 20 3expia ⊢ ( ( ( 𝐽 ↾t 𝑘 ) ∈ ( TopOn ‘ ∪ ( 𝐾 ↾t 𝑘 ) ) ∧ ( 𝐽 ↾t 𝑘 ) ⊆ ( 𝐾 ↾t 𝑘 ) ) → ( ( 𝐾 ↾t 𝑘 ) ∈ Comp → ( 𝐽 ↾t 𝑘 ) ∈ Comp ) )
22 11 17 21 syl2anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → ( ( 𝐾 ↾t 𝑘 ) ∈ Comp → ( 𝐽 ↾t 𝑘 ) ∈ Comp ) )
23 17 sseld ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → ( ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐾 ↾t 𝑘 ) ) )
24 22 23 imim12d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → ( ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) → ( ( 𝐾 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐾 ↾t 𝑘 ) ) ) )
25 24 ralimdva ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → ( ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) → ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐾 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐾 ↾t 𝑘 ) ) ) )
26 25 anim2d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → ( ( 𝑥 ⊆ 𝑋 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) → ( 𝑥 ⊆ 𝑋 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐾 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐾 ↾t 𝑘 ) ) ) ) )
27 elkgen ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) ) )
28 27 3ad2ant1 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) ) )
29 elkgen ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) → ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐾 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐾 ↾t 𝑘 ) ) ) ) )
30 29 3ad2ant2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐾 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐾 ↾t 𝑘 ) ) ) ) )
31 26 28 30 3imtr4d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) → 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) )
32 31 ssrdv ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → ( 𝑘Gen ‘ 𝐽 ) ⊆ ( 𝑘Gen ‘ 𝐾 ) )