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 eqtrid ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ ( 𝑦 ∈ 𝒫 𝐽 ∧ ( 𝐽t 𝑦 ) ∈ Comp ) ) → ( ( ( 𝑓𝑥 ) ∩ ( 𝑓 “ ( 𝑓𝑦 ) ) ) ∩ 𝑦 ) = ( ( 𝑓𝑥 ) ∩ 𝑦 ) )
24 14 23 eqtrd ( ( ( ( ( 𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐾 ) ) ∧ ( 𝑦 ∈ 𝒫 𝐽 ∧ ( 𝐽t 𝑦 ) ∈ Comp ) ) → ( ( 𝑓 “ ( 𝑥 ∩ ( 𝑓𝑦 ) ) ) ∩ 𝑦 ) = ( ( 𝑓𝑥 ) ∩ 𝑦 ) )
25 9 24 eqtrid ( ( ( ( ( 𝐽 ∈ 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 ‘ 𝐾 ) ) )