Metamath Proof Explorer

Theorem kgencn3

Description: The set of continuous functions from J to K is unaffected by k-ification of K , if J is already compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion kgencn3 ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) → ( 𝐽 Cn 𝐾 ) = ( 𝐽 Cn ( 𝑘Gen ‘ 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
2 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
3 1 2 cnf ⊢ ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) → 𝑓 : ∪ 𝐽 ⟶ ∪ 𝐾 )
4 3 adantl ⊢ ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝑓 : ∪ 𝐽 ⟶ ∪ 𝐾 )
5 cnvimass ⊢ ( ◡ 𝑓 “ 𝑥 ) ⊆ dom 𝑓
6 4 fdmd ⊢ ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) → dom 𝑓 = ∪ 𝐽 )
7 6 adantr ⊢ ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) → dom 𝑓 = ∪ 𝐽 )
8 5 7 sseqtrid ⊢ ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) → ( ◡ 𝑓 “ 𝑥 ) ⊆ ∪ 𝐽 )
9 cnvresima ⊢ ( ◡ ( 𝑓 ↾ 𝑦 ) “ ( 𝑥 ∩ ( 𝑓 “ 𝑦 ) ) ) = ( ( ◡ 𝑓 “ ( 𝑥 ∩ ( 𝑓 “ 𝑦 ) ) ) ∩ 𝑦 )
10 4 ad2antrr ⊢ ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ ( 𝑦 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Comp ) ) → 𝑓 : ∪ 𝐽 ⟶ ∪ 𝐾 )
11 ffun ⊢ ( 𝑓 : ∪ 𝐽 ⟶ ∪ 𝐾 → Fun 𝑓 )
12 inpreima ⊢ ( Fun 𝑓 → ( ◡ 𝑓 “ ( 𝑥 ∩ ( 𝑓 “ 𝑦 ) ) ) = ( ( ◡ 𝑓 “ 𝑥 ) ∩ ( ◡ 𝑓 “ ( 𝑓 “ 𝑦 ) ) ) )
13 10 11 12 3syl ⊢ ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ ( 𝑦 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Comp ) ) → ( ◡ 𝑓 “ ( 𝑥 ∩ ( 𝑓 “ 𝑦 ) ) ) = ( ( ◡ 𝑓 “ 𝑥 ) ∩ ( ◡ 𝑓 “ ( 𝑓 “ 𝑦 ) ) ) )
14 13 ineq1d ⊢ ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ ( 𝑦 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Comp ) ) → ( ( ◡ 𝑓 “ ( 𝑥 ∩ ( 𝑓 “ 𝑦 ) ) ) ∩ 𝑦 ) = ( ( ( ◡ 𝑓 “ 𝑥 ) ∩ ( ◡ 𝑓 “ ( 𝑓 “ 𝑦 ) ) ) ∩ 𝑦 ) )
15 in32 ⊢ ( ( ( ◡ 𝑓 “ 𝑥 ) ∩ ( ◡ 𝑓 “ ( 𝑓 “ 𝑦 ) ) ) ∩ 𝑦 ) = ( ( ( ◡ 𝑓 “ 𝑥 ) ∩ 𝑦 ) ∩ ( ◡ 𝑓 “ ( 𝑓 “ 𝑦 ) ) )
16 ssrin ⊢ ( ( ◡ 𝑓 “ 𝑥 ) ⊆ dom 𝑓 → ( ( ◡ 𝑓 “ 𝑥 ) ∩ 𝑦 ) ⊆ ( dom 𝑓 ∩ 𝑦 ) )
17 5 16 ax-mp ⊢ ( ( ◡ 𝑓 “ 𝑥 ) ∩ 𝑦 ) ⊆ ( dom 𝑓 ∩ 𝑦 )
18 dminss ⊢ ( dom 𝑓 ∩ 𝑦 ) ⊆ ( ◡ 𝑓 “ ( 𝑓 “ 𝑦 ) )
19 17 18 sstri ⊢ ( ( ◡ 𝑓 “ 𝑥 ) ∩ 𝑦 ) ⊆ ( ◡ 𝑓 “ ( 𝑓 “ 𝑦 ) )
20 19 a1i ⊢ ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ ( 𝑦 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Comp ) ) → ( ( ◡ 𝑓 “ 𝑥 ) ∩ 𝑦 ) ⊆ ( ◡ 𝑓 “ ( 𝑓 “ 𝑦 ) ) )
21 df-ss ⊢ ( ( ( ◡ 𝑓 “ 𝑥 ) ∩ 𝑦 ) ⊆ ( ◡ 𝑓 “ ( 𝑓 “ 𝑦 ) ) ↔ ( ( ( ◡ 𝑓 “ 𝑥 ) ∩ 𝑦 ) ∩ ( ◡ 𝑓 “ ( 𝑓 “ 𝑦 ) ) ) = ( ( ◡ 𝑓 “ 𝑥 ) ∩ 𝑦 ) )
22 20 21 sylib ⊢ ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ ( 𝑦 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Comp ) ) → ( ( ( ◡ 𝑓 “ 𝑥 ) ∩ 𝑦 ) ∩ ( ◡ 𝑓 “ ( 𝑓 “ 𝑦 ) ) ) = ( ( ◡ 𝑓 “ 𝑥 ) ∩ 𝑦 ) )
23 15 22 syl5eq ⊢ ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ ( 𝑦 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Comp ) ) → ( ( ( ◡ 𝑓 “ 𝑥 ) ∩ ( ◡ 𝑓 “ ( 𝑓 “ 𝑦 ) ) ) ∩ 𝑦 ) = ( ( ◡ 𝑓 “ 𝑥 ) ∩ 𝑦 ) )
24 14 23 eqtrd ⊢ ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ ( 𝑦 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Comp ) ) → ( ( ◡ 𝑓 “ ( 𝑥 ∩ ( 𝑓 “ 𝑦 ) ) ) ∩ 𝑦 ) = ( ( ◡ 𝑓 “ 𝑥 ) ∩ 𝑦 ) )
25 9 24 syl5eq ⊢ ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ ( 𝑦 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Comp ) ) → ( ◡ ( 𝑓 ↾ 𝑦 ) “ ( 𝑥 ∩ ( 𝑓 “ 𝑦 ) ) ) = ( ( ◡ 𝑓 “ 𝑥 ) ∩ 𝑦 ) )
26 simpr ⊢ ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝑓 ∈ ( 𝐽 Cn 𝐾 ) )
27 26 ad2antrr ⊢ ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ ( 𝑦 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Comp ) ) → 𝑓 ∈ ( 𝐽 Cn 𝐾 ) )
28 elpwi ⊢ ( 𝑦 ∈ 𝒫 ∪ 𝐽 → 𝑦 ⊆ ∪ 𝐽 )
29 28 ad2antrl ⊢ ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ ( 𝑦 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Comp ) ) → 𝑦 ⊆ ∪ 𝐽 )
30 1 cnrest ⊢ ( ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑦 ⊆ ∪ 𝐽 ) → ( 𝑓 ↾ 𝑦 ) ∈ ( ( 𝐽 ↾t 𝑦 ) Cn 𝐾 ) )
31 27 29 30 syl2anc ⊢ ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ ( 𝑦 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Comp ) ) → ( 𝑓 ↾ 𝑦 ) ∈ ( ( 𝐽 ↾t 𝑦 ) Cn 𝐾 ) )
32 simpr ⊢ ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) → 𝐾 ∈ Top )
33 32 ad3antrrr ⊢ ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ ( 𝑦 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Comp ) ) → 𝐾 ∈ Top )
34 toptopon2 ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
35 33 34 sylib ⊢ ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ ( 𝑦 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Comp ) ) → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
36 df-ima ⊢ ( 𝑓 “ 𝑦 ) = ran ( 𝑓 ↾ 𝑦 )
37 36 eqimss2i ⊢ ran ( 𝑓 ↾ 𝑦 ) ⊆ ( 𝑓 “ 𝑦 )
38 37 a1i ⊢ ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ ( 𝑦 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Comp ) ) → ran ( 𝑓 ↾ 𝑦 ) ⊆ ( 𝑓 “ 𝑦 ) )
39 imassrn ⊢ ( 𝑓 “ 𝑦 ) ⊆ ran 𝑓
40 10 frnd ⊢ ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ ( 𝑦 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Comp ) ) → ran 𝑓 ⊆ ∪ 𝐾 )
41 39 40 sstrid ⊢ ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ ( 𝑦 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Comp ) ) → ( 𝑓 “ 𝑦 ) ⊆ ∪ 𝐾 )
42 cnrest2 ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ∧ ran ( 𝑓 ↾ 𝑦 ) ⊆ ( 𝑓 “ 𝑦 ) ∧ ( 𝑓 “ 𝑦 ) ⊆ ∪ 𝐾 ) → ( ( 𝑓 ↾ 𝑦 ) ∈ ( ( 𝐽 ↾t 𝑦 ) Cn 𝐾 ) ↔ ( 𝑓 ↾ 𝑦 ) ∈ ( ( 𝐽 ↾t 𝑦 ) Cn ( 𝐾 ↾t ( 𝑓 “ 𝑦 ) ) ) ) )
43 35 38 41 42 syl3anc ⊢ ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ ( 𝑦 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Comp ) ) → ( ( 𝑓 ↾ 𝑦 ) ∈ ( ( 𝐽 ↾t 𝑦 ) Cn 𝐾 ) ↔ ( 𝑓 ↾ 𝑦 ) ∈ ( ( 𝐽 ↾t 𝑦 ) Cn ( 𝐾 ↾t ( 𝑓 “ 𝑦 ) ) ) ) )
44 31 43 mpbid ⊢ ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ ( 𝑦 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Comp ) ) → ( 𝑓 ↾ 𝑦 ) ∈ ( ( 𝐽 ↾t 𝑦 ) Cn ( 𝐾 ↾t ( 𝑓 “ 𝑦 ) ) ) )
45 simplr ⊢ ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ ( 𝑦 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Comp ) ) → 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) )
46 simprr ⊢ ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ ( 𝑦 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Comp ) ) → ( 𝐽 ↾t 𝑦 ) ∈ Comp )
47 imacmp ⊢ ( ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( 𝐽 ↾t 𝑦 ) ∈ Comp ) → ( 𝐾 ↾t ( 𝑓 “ 𝑦 ) ) ∈ Comp )
48 27 46 47 syl2anc ⊢ ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ ( 𝑦 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Comp ) ) → ( 𝐾 ↾t ( 𝑓 “ 𝑦 ) ) ∈ Comp )
49 kgeni ⊢ ( ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ∧ ( 𝐾 ↾t ( 𝑓 “ 𝑦 ) ) ∈ Comp ) → ( 𝑥 ∩ ( 𝑓 “ 𝑦 ) ) ∈ ( 𝐾 ↾t ( 𝑓 “ 𝑦 ) ) )
50 45 48 49 syl2anc ⊢ ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ ( 𝑦 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Comp ) ) → ( 𝑥 ∩ ( 𝑓 “ 𝑦 ) ) ∈ ( 𝐾 ↾t ( 𝑓 “ 𝑦 ) ) )
51 cnima ⊢ ( ( ( 𝑓 ↾ 𝑦 ) ∈ ( ( 𝐽 ↾t 𝑦 ) Cn ( 𝐾 ↾t ( 𝑓 “ 𝑦 ) ) ) ∧ ( 𝑥 ∩ ( 𝑓 “ 𝑦 ) ) ∈ ( 𝐾 ↾t ( 𝑓 “ 𝑦 ) ) ) → ( ◡ ( 𝑓 ↾ 𝑦 ) “ ( 𝑥 ∩ ( 𝑓 “ 𝑦 ) ) ) ∈ ( 𝐽 ↾t 𝑦 ) )
52 44 50 51 syl2anc ⊢ ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ ( 𝑦 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Comp ) ) → ( ◡ ( 𝑓 ↾ 𝑦 ) “ ( 𝑥 ∩ ( 𝑓 “ 𝑦 ) ) ) ∈ ( 𝐽 ↾t 𝑦 ) )
53 25 52 eqeltrrd ⊢ ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ ( 𝑦 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Comp ) ) → ( ( ◡ 𝑓 “ 𝑥 ) ∩ 𝑦 ) ∈ ( 𝐽 ↾t 𝑦 ) )
54 53 expr ⊢ ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ 𝑦 ∈ 𝒫 ∪ 𝐽 ) → ( ( 𝐽 ↾t 𝑦 ) ∈ Comp → ( ( ◡ 𝑓 “ 𝑥 ) ∩ 𝑦 ) ∈ ( 𝐽 ↾t 𝑦 ) ) )
55 54 ralrimiva ⊢ ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) → ∀ 𝑦 ∈ 𝒫 ∪ 𝐽 ( ( 𝐽 ↾t 𝑦 ) ∈ Comp → ( ( ◡ 𝑓 “ 𝑥 ) ∩ 𝑦 ) ∈ ( 𝐽 ↾t 𝑦 ) ) )
56 kgentop ⊢ ( 𝐽 ∈ ran 𝑘Gen → 𝐽 ∈ Top )
57 56 ad3antrrr ⊢ ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) → 𝐽 ∈ Top )
58 toptopon2 ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
59 57 58 sylib ⊢ ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
60 elkgen ⊢ ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) → ( ( ◡ 𝑓 “ 𝑥 ) ∈ ( 𝑘Gen ‘ 𝐽 ) ↔ ( ( ◡ 𝑓 “ 𝑥 ) ⊆ ∪ 𝐽 ∧ ∀ 𝑦 ∈ 𝒫 ∪ 𝐽 ( ( 𝐽 ↾t 𝑦 ) ∈ Comp → ( ( ◡ 𝑓 “ 𝑥 ) ∩ 𝑦 ) ∈ ( 𝐽 ↾t 𝑦 ) ) ) ) )
61 59 60 syl ⊢ ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) → ( ( ◡ 𝑓 “ 𝑥 ) ∈ ( 𝑘Gen ‘ 𝐽 ) ↔ ( ( ◡ 𝑓 “ 𝑥 ) ⊆ ∪ 𝐽 ∧ ∀ 𝑦 ∈ 𝒫 ∪ 𝐽 ( ( 𝐽 ↾t 𝑦 ) ∈ Comp → ( ( ◡ 𝑓 “ 𝑥 ) ∩ 𝑦 ) ∈ ( 𝐽 ↾t 𝑦 ) ) ) ) )
62 8 55 61 mpbir2and ⊢ ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) → ( ◡ 𝑓 “ 𝑥 ) ∈ ( 𝑘Gen ‘ 𝐽 ) )
63 kgenidm ⊢ ( 𝐽 ∈ ran 𝑘Gen → ( 𝑘Gen ‘ 𝐽 ) = 𝐽 )
64 63 ad3antrrr ⊢ ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) → ( 𝑘Gen ‘ 𝐽 ) = 𝐽 )
65 62 64 eleqtrd ⊢ ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) → ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 )
66 65 ralrimiva ⊢ ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) → ∀ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 )
67 56 58 sylib ⊢ ( 𝐽 ∈ ran 𝑘Gen → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
68 kgentopon ⊢ ( 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) → ( 𝑘Gen ‘ 𝐾 ) ∈ ( TopOn ‘ ∪ 𝐾 ) )
69 34 68 sylbi ⊢ ( 𝐾 ∈ Top → ( 𝑘Gen ‘ 𝐾 ) ∈ ( TopOn ‘ ∪ 𝐾 ) )
70 iscn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ ( 𝑘Gen ‘ 𝐾 ) ∈ ( TopOn ‘ ∪ 𝐾 ) ) → ( 𝑓 ∈ ( 𝐽 Cn ( 𝑘Gen ‘ 𝐾 ) ) ↔ ( 𝑓 : ∪ 𝐽 ⟶ ∪ 𝐾 ∧ ∀ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 ) ) )
71 67 69 70 syl2an ⊢ ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) → ( 𝑓 ∈ ( 𝐽 Cn ( 𝑘Gen ‘ 𝐾 ) ) ↔ ( 𝑓 : ∪ 𝐽 ⟶ ∪ 𝐾 ∧ ∀ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 ) ) )
72 71 adantr ⊢ ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝑓 ∈ ( 𝐽 Cn ( 𝑘Gen ‘ 𝐾 ) ) ↔ ( 𝑓 : ∪ 𝐽 ⟶ ∪ 𝐾 ∧ ∀ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 ) ) )
73 4 66 72 mpbir2and ⊢ ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝑓 ∈ ( 𝐽 Cn ( 𝑘Gen ‘ 𝐾 ) ) )
74 73 ex ⊢ ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) → ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) → 𝑓 ∈ ( 𝐽 Cn ( 𝑘Gen ‘ 𝐾 ) ) ) )
75 74 ssrdv ⊢ ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) → ( 𝐽 Cn 𝐾 ) ⊆ ( 𝐽 Cn ( 𝑘Gen ‘ 𝐾 ) ) )
76 69 adantl ⊢ ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) → ( 𝑘Gen ‘ 𝐾 ) ∈ ( TopOn ‘ ∪ 𝐾 ) )
77 toponcom ⊢ ( ( 𝐾 ∈ Top ∧ ( 𝑘Gen ‘ 𝐾 ) ∈ ( TopOn ‘ ∪ 𝐾 ) ) → 𝐾 ∈ ( TopOn ‘ ∪ ( 𝑘Gen ‘ 𝐾 ) ) )
78 32 76 77 syl2anc ⊢ ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) → 𝐾 ∈ ( TopOn ‘ ∪ ( 𝑘Gen ‘ 𝐾 ) ) )
79 kgenss ⊢ ( 𝐾 ∈ Top → 𝐾 ⊆ ( 𝑘Gen ‘ 𝐾 ) )
80 79 adantl ⊢ ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) → 𝐾 ⊆ ( 𝑘Gen ‘ 𝐾 ) )
81 eqid ⊢ ∪ ( 𝑘Gen ‘ 𝐾 ) = ∪ ( 𝑘Gen ‘ 𝐾 )
82 81 cnss2 ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ∪ ( 𝑘Gen ‘ 𝐾 ) ) ∧ 𝐾 ⊆ ( 𝑘Gen ‘ 𝐾 ) ) → ( 𝐽 Cn ( 𝑘Gen ‘ 𝐾 ) ) ⊆ ( 𝐽 Cn 𝐾 ) )
83 78 80 82 syl2anc ⊢ ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) → ( 𝐽 Cn ( 𝑘Gen ‘ 𝐾 ) ) ⊆ ( 𝐽 Cn 𝐾 ) )
84 75 83 eqssd ⊢ ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) → ( 𝐽 Cn 𝐾 ) = ( 𝐽 Cn ( 𝑘Gen ‘ 𝐾 ) ) )