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 β€˜ 𝐾 ) )