Metamath Proof Explorer

Theorem kgencmp2

Description: The compact generator topology has the same compact sets as the original topology. (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Assertion kgencmp2 ( 𝐽 ∈ Top β†’ ( ( 𝐽 β†Ύt 𝐾 ) ∈ Comp ↔ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ∈ Comp ) )

Proof

Step Hyp Ref Expression
1 kgencmp ⊒ ( ( 𝐽 ∈ Top ∧ ( 𝐽 β†Ύt 𝐾 ) ∈ Comp ) β†’ ( 𝐽 β†Ύt 𝐾 ) = ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) )
2 simpr ⊒ ( ( 𝐽 ∈ Top ∧ ( 𝐽 β†Ύt 𝐾 ) ∈ Comp ) β†’ ( 𝐽 β†Ύt 𝐾 ) ∈ Comp )
3 1 2 eqeltrrd ⊒ ( ( 𝐽 ∈ Top ∧ ( 𝐽 β†Ύt 𝐾 ) ∈ Comp ) β†’ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ∈ Comp )
4 cmptop ⊒ ( ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ∈ Comp β†’ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ∈ Top )
5 restrcl ⊒ ( ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ∈ Top β†’ ( ( π‘˜Gen β€˜ 𝐽 ) ∈ V ∧ 𝐾 ∈ V ) )
6 5 simprd ⊒ ( ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ∈ Top β†’ 𝐾 ∈ V )
7 4 6 syl ⊒ ( ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ∈ Comp β†’ 𝐾 ∈ V )
8 resttop ⊒ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ V ) β†’ ( 𝐽 β†Ύt 𝐾 ) ∈ Top )
9 7 8 sylan2 ⊒ ( ( 𝐽 ∈ Top ∧ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ∈ Comp ) β†’ ( 𝐽 β†Ύt 𝐾 ) ∈ Top )
10 toptopon2 ⊒ ( ( 𝐽 β†Ύt 𝐾 ) ∈ Top ↔ ( 𝐽 β†Ύt 𝐾 ) ∈ ( TopOn β€˜ βˆͺ ( 𝐽 β†Ύt 𝐾 ) ) )
11 9 10 sylib ⊒ ( ( 𝐽 ∈ Top ∧ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ∈ Comp ) β†’ ( 𝐽 β†Ύt 𝐾 ) ∈ ( TopOn β€˜ βˆͺ ( 𝐽 β†Ύt 𝐾 ) ) )
12 eqid ⊒ βˆͺ 𝐽 = βˆͺ 𝐽
13 12 kgenuni ⊒ ( 𝐽 ∈ Top β†’ βˆͺ 𝐽 = βˆͺ ( π‘˜Gen β€˜ 𝐽 ) )
14 13 adantr ⊒ ( ( 𝐽 ∈ Top ∧ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ∈ Comp ) β†’ βˆͺ 𝐽 = βˆͺ ( π‘˜Gen β€˜ 𝐽 ) )
15 14 ineq2d ⊒ ( ( 𝐽 ∈ Top ∧ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ∈ Comp ) β†’ ( 𝐾 ∩ βˆͺ 𝐽 ) = ( 𝐾 ∩ βˆͺ ( π‘˜Gen β€˜ 𝐽 ) ) )
16 12 restuni2 ⊒ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ V ) β†’ ( 𝐾 ∩ βˆͺ 𝐽 ) = βˆͺ ( 𝐽 β†Ύt 𝐾 ) )
17 7 16 sylan2 ⊒ ( ( 𝐽 ∈ Top ∧ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ∈ Comp ) β†’ ( 𝐾 ∩ βˆͺ 𝐽 ) = βˆͺ ( 𝐽 β†Ύt 𝐾 ) )
18 kgenftop ⊒ ( 𝐽 ∈ Top β†’ ( π‘˜Gen β€˜ 𝐽 ) ∈ Top )
19 eqid ⊒ βˆͺ ( π‘˜Gen β€˜ 𝐽 ) = βˆͺ ( π‘˜Gen β€˜ 𝐽 )
20 19 restuni2 ⊒ ( ( ( π‘˜Gen β€˜ 𝐽 ) ∈ Top ∧ 𝐾 ∈ V ) β†’ ( 𝐾 ∩ βˆͺ ( π‘˜Gen β€˜ 𝐽 ) ) = βˆͺ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) )
21 18 7 20 syl2an ⊒ ( ( 𝐽 ∈ Top ∧ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ∈ Comp ) β†’ ( 𝐾 ∩ βˆͺ ( π‘˜Gen β€˜ 𝐽 ) ) = βˆͺ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) )
22 15 17 21 3eqtr3d ⊒ ( ( 𝐽 ∈ Top ∧ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ∈ Comp ) β†’ βˆͺ ( 𝐽 β†Ύt 𝐾 ) = βˆͺ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) )
23 22 fveq2d ⊒ ( ( 𝐽 ∈ Top ∧ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ∈ Comp ) β†’ ( TopOn β€˜ βˆͺ ( 𝐽 β†Ύt 𝐾 ) ) = ( TopOn β€˜ βˆͺ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ) )
24 11 23 eleqtrd ⊒ ( ( 𝐽 ∈ Top ∧ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ∈ Comp ) β†’ ( 𝐽 β†Ύt 𝐾 ) ∈ ( TopOn β€˜ βˆͺ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ) )
25 simpr ⊒ ( ( 𝐽 ∈ Top ∧ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ∈ Comp ) β†’ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ∈ Comp )
26 kgenss ⊒ ( 𝐽 ∈ Top β†’ 𝐽 βŠ† ( π‘˜Gen β€˜ 𝐽 ) )
27 26 adantr ⊒ ( ( 𝐽 ∈ Top ∧ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ∈ Comp ) β†’ 𝐽 βŠ† ( π‘˜Gen β€˜ 𝐽 ) )
28 ssrest ⊒ ( ( ( π‘˜Gen β€˜ 𝐽 ) ∈ Top ∧ 𝐽 βŠ† ( π‘˜Gen β€˜ 𝐽 ) ) β†’ ( 𝐽 β†Ύt 𝐾 ) βŠ† ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) )
29 18 27 28 syl2an2r ⊒ ( ( 𝐽 ∈ Top ∧ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ∈ Comp ) β†’ ( 𝐽 β†Ύt 𝐾 ) βŠ† ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) )
30 eqid ⊒ βˆͺ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) = βˆͺ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 )
31 30 sscmp ⊒ ( ( ( 𝐽 β†Ύt 𝐾 ) ∈ ( TopOn β€˜ βˆͺ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ) ∧ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ∈ Comp ∧ ( 𝐽 β†Ύt 𝐾 ) βŠ† ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ) β†’ ( 𝐽 β†Ύt 𝐾 ) ∈ Comp )
32 24 25 29 31 syl3anc ⊒ ( ( 𝐽 ∈ Top ∧ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ∈ Comp ) β†’ ( 𝐽 β†Ύt 𝐾 ) ∈ Comp )
33 3 32 impbida ⊒ ( 𝐽 ∈ Top β†’ ( ( 𝐽 β†Ύt 𝐾 ) ∈ Comp ↔ ( ( π‘˜Gen β€˜ 𝐽 ) β†Ύt 𝐾 ) ∈ Comp ) )