Metamath Proof Explorer

Theorem kgeni

Description: Property of the open sets in the compact generator. (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Assertion kgeni ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐴 ∩ 𝐾 ) ∈ ( 𝐽 ↾t 𝐾 ) )

Proof

Step Hyp Ref Expression
1 inass ⊢ ( ( 𝐴 ∩ 𝐾 ) ∩ ∪ 𝐽 ) = ( 𝐴 ∩ ( 𝐾 ∩ ∪ 𝐽 ) )
2 in32 ⊢ ( ( 𝐴 ∩ 𝐾 ) ∩ ∪ 𝐽 ) = ( ( 𝐴 ∩ ∪ 𝐽 ) ∩ 𝐾 )
3 1 2 eqtr3i ⊢ ( 𝐴 ∩ ( 𝐾 ∩ ∪ 𝐽 ) ) = ( ( 𝐴 ∩ ∪ 𝐽 ) ∩ 𝐾 )
4 df-kgen ⊢ 𝑘Gen = ( 𝑗 ∈ Top ↦ { 𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ∀ 𝑦 ∈ 𝒫 ∪ 𝑗 ( ( 𝑗 ↾t 𝑦 ) ∈ Comp → ( 𝑥 ∩ 𝑦 ) ∈ ( 𝑗 ↾t 𝑦 ) ) } )
5 4 mptrcl ⊢ ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) → 𝐽 ∈ Top )
6 5 adantr ⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → 𝐽 ∈ Top )
7 toptopon2 ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
8 6 7 sylib ⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
9 simpl ⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) )
10 elkgen ⊢ ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) → ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ↔ ( 𝐴 ⊆ ∪ 𝐽 ∧ ∀ 𝑦 ∈ 𝒫 ∪ 𝐽 ( ( 𝐽 ↾t 𝑦 ) ∈ Comp → ( 𝐴 ∩ 𝑦 ) ∈ ( 𝐽 ↾t 𝑦 ) ) ) ) )
11 10 biimpa ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ) → ( 𝐴 ⊆ ∪ 𝐽 ∧ ∀ 𝑦 ∈ 𝒫 ∪ 𝐽 ( ( 𝐽 ↾t 𝑦 ) ∈ Comp → ( 𝐴 ∩ 𝑦 ) ∈ ( 𝐽 ↾t 𝑦 ) ) ) )
12 8 9 11 syl2anc ⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐴 ⊆ ∪ 𝐽 ∧ ∀ 𝑦 ∈ 𝒫 ∪ 𝐽 ( ( 𝐽 ↾t 𝑦 ) ∈ Comp → ( 𝐴 ∩ 𝑦 ) ∈ ( 𝐽 ↾t 𝑦 ) ) ) )
13 12 simpld ⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → 𝐴 ⊆ ∪ 𝐽 )
14 df-ss ⊢ ( 𝐴 ⊆ ∪ 𝐽 ↔ ( 𝐴 ∩ ∪ 𝐽 ) = 𝐴 )
15 13 14 sylib ⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐴 ∩ ∪ 𝐽 ) = 𝐴 )
16 15 ineq1d ⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( ( 𝐴 ∩ ∪ 𝐽 ) ∩ 𝐾 ) = ( 𝐴 ∩ 𝐾 ) )
17 3 16 eqtrid ⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐴 ∩ ( 𝐾 ∩ ∪ 𝐽 ) ) = ( 𝐴 ∩ 𝐾 ) )
18 cmptop ⊢ ( ( 𝐽 ↾t 𝐾 ) ∈ Comp → ( 𝐽 ↾t 𝐾 ) ∈ Top )
19 18 adantl ⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐽 ↾t 𝐾 ) ∈ Top )
20 restrcl ⊢ ( ( 𝐽 ↾t 𝐾 ) ∈ Top → ( 𝐽 ∈ V ∧ 𝐾 ∈ V ) )
21 20 simprd ⊢ ( ( 𝐽 ↾t 𝐾 ) ∈ Top → 𝐾 ∈ V )
22 19 21 syl ⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → 𝐾 ∈ V )
23 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
24 23 restin ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ V ) → ( 𝐽 ↾t 𝐾 ) = ( 𝐽 ↾t ( 𝐾 ∩ ∪ 𝐽 ) ) )
25 6 22 24 syl2anc ⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐽 ↾t 𝐾 ) = ( 𝐽 ↾t ( 𝐾 ∩ ∪ 𝐽 ) ) )
26 simpr ⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐽 ↾t 𝐾 ) ∈ Comp )
27 25 26 eqeltrrd ⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐽 ↾t ( 𝐾 ∩ ∪ 𝐽 ) ) ∈ Comp )
28 oveq2 ⊢ ( 𝑦 = ( 𝐾 ∩ ∪ 𝐽 ) → ( 𝐽 ↾t 𝑦 ) = ( 𝐽 ↾t ( 𝐾 ∩ ∪ 𝐽 ) ) )
29 28 eleq1d ⊢ ( 𝑦 = ( 𝐾 ∩ ∪ 𝐽 ) → ( ( 𝐽 ↾t 𝑦 ) ∈ Comp ↔ ( 𝐽 ↾t ( 𝐾 ∩ ∪ 𝐽 ) ) ∈ Comp ) )
30 ineq2 ⊢ ( 𝑦 = ( 𝐾 ∩ ∪ 𝐽 ) → ( 𝐴 ∩ 𝑦 ) = ( 𝐴 ∩ ( 𝐾 ∩ ∪ 𝐽 ) ) )
31 30 28 eleq12d ⊢ ( 𝑦 = ( 𝐾 ∩ ∪ 𝐽 ) → ( ( 𝐴 ∩ 𝑦 ) ∈ ( 𝐽 ↾t 𝑦 ) ↔ ( 𝐴 ∩ ( 𝐾 ∩ ∪ 𝐽 ) ) ∈ ( 𝐽 ↾t ( 𝐾 ∩ ∪ 𝐽 ) ) ) )
32 29 31 imbi12d ⊢ ( 𝑦 = ( 𝐾 ∩ ∪ 𝐽 ) → ( ( ( 𝐽 ↾t 𝑦 ) ∈ Comp → ( 𝐴 ∩ 𝑦 ) ∈ ( 𝐽 ↾t 𝑦 ) ) ↔ ( ( 𝐽 ↾t ( 𝐾 ∩ ∪ 𝐽 ) ) ∈ Comp → ( 𝐴 ∩ ( 𝐾 ∩ ∪ 𝐽 ) ) ∈ ( 𝐽 ↾t ( 𝐾 ∩ ∪ 𝐽 ) ) ) ) )
33 12 simprd ⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ∀ 𝑦 ∈ 𝒫 ∪ 𝐽 ( ( 𝐽 ↾t 𝑦 ) ∈ Comp → ( 𝐴 ∩ 𝑦 ) ∈ ( 𝐽 ↾t 𝑦 ) ) )
34 inss2 ⊢ ( 𝐾 ∩ ∪ 𝐽 ) ⊆ ∪ 𝐽
35 inex1g ⊢ ( 𝐾 ∈ V → ( 𝐾 ∩ ∪ 𝐽 ) ∈ V )
36 elpwg ⊢ ( ( 𝐾 ∩ ∪ 𝐽 ) ∈ V → ( ( 𝐾 ∩ ∪ 𝐽 ) ∈ 𝒫 ∪ 𝐽 ↔ ( 𝐾 ∩ ∪ 𝐽 ) ⊆ ∪ 𝐽 ) )
37 22 35 36 3syl ⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( ( 𝐾 ∩ ∪ 𝐽 ) ∈ 𝒫 ∪ 𝐽 ↔ ( 𝐾 ∩ ∪ 𝐽 ) ⊆ ∪ 𝐽 ) )
38 34 37 mpbiri ⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐾 ∩ ∪ 𝐽 ) ∈ 𝒫 ∪ 𝐽 )
39 32 33 38 rspcdva ⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( ( 𝐽 ↾t ( 𝐾 ∩ ∪ 𝐽 ) ) ∈ Comp → ( 𝐴 ∩ ( 𝐾 ∩ ∪ 𝐽 ) ) ∈ ( 𝐽 ↾t ( 𝐾 ∩ ∪ 𝐽 ) ) ) )
40 27 39 mpd ⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐴 ∩ ( 𝐾 ∩ ∪ 𝐽 ) ) ∈ ( 𝐽 ↾t ( 𝐾 ∩ ∪ 𝐽 ) ) )
41 17 40 eqeltrrd ⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐴 ∩ 𝐾 ) ∈ ( 𝐽 ↾t ( 𝐾 ∩ ∪ 𝐽 ) ) )
42 41 25 eleqtrrd ⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐴 ∩ 𝐾 ) ∈ ( 𝐽 ↾t 𝐾 ) )