Metamath Proof Explorer


Theorem 1stckgen

Description: A first-countable space is compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion 1stckgen ( 𝐽 ∈ 1stω → 𝐽 ∈ ran 𝑘Gen )

Proof

Step Hyp Ref Expression
1 1stctop ( 𝐽 ∈ 1stω → 𝐽 ∈ Top )
2 difss ( 𝐽𝑥 ) ⊆ 𝐽
3 eqid 𝐽 = 𝐽
4 3 1stcelcls ( ( 𝐽 ∈ 1stω ∧ ( 𝐽𝑥 ) ⊆ 𝐽 ) → ( 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐽𝑥 ) ) ↔ ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) )
5 2 4 mpan2 ( 𝐽 ∈ 1stω → ( 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐽𝑥 ) ) ↔ ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) )
6 5 adantr ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) → ( 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐽𝑥 ) ) ↔ ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) )
7 1 adantr ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) → 𝐽 ∈ Top )
8 7 adantr ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → 𝐽 ∈ Top )
9 toptopon2 ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝐽 ) )
10 8 9 sylib ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → 𝐽 ∈ ( TopOn ‘ 𝐽 ) )
11 simprr ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → 𝑓 ( ⇝𝑡𝐽 ) 𝑦 )
12 lmcl ( ( 𝐽 ∈ ( TopOn ‘ 𝐽 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) → 𝑦 𝐽 )
13 10 11 12 syl2anc ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → 𝑦 𝐽 )
14 nnuz ℕ = ( ℤ ‘ 1 )
15 vex 𝑓 ∈ V
16 15 rnex ran 𝑓 ∈ V
17 snex { 𝑦 } ∈ V
18 16 17 unex ( ran 𝑓 ∪ { 𝑦 } ) ∈ V
19 resttop ( ( 𝐽 ∈ Top ∧ ( ran 𝑓 ∪ { 𝑦 } ) ∈ V ) → ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) ∈ Top )
20 8 18 19 sylancl ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) ∈ Top )
21 toptopon2 ( ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) ∈ Top ↔ ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) ∈ ( TopOn ‘ ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) ) )
22 20 21 sylib ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) ∈ ( TopOn ‘ ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) ) )
23 1zzd ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → 1 ∈ ℤ )
24 eqid ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) = ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) )
25 18 a1i ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → ( ran 𝑓 ∪ { 𝑦 } ) ∈ V )
26 ssun2 { 𝑦 } ⊆ ( ran 𝑓 ∪ { 𝑦 } )
27 vex 𝑦 ∈ V
28 27 snss ( 𝑦 ∈ ( ran 𝑓 ∪ { 𝑦 } ) ↔ { 𝑦 } ⊆ ( ran 𝑓 ∪ { 𝑦 } ) )
29 26 28 mpbir 𝑦 ∈ ( ran 𝑓 ∪ { 𝑦 } )
30 29 a1i ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → 𝑦 ∈ ( ran 𝑓 ∪ { 𝑦 } ) )
31 ffn ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) → 𝑓 Fn ℕ )
32 31 ad2antrl ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → 𝑓 Fn ℕ )
33 dffn3 ( 𝑓 Fn ℕ ↔ 𝑓 : ℕ ⟶ ran 𝑓 )
34 32 33 sylib ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → 𝑓 : ℕ ⟶ ran 𝑓 )
35 ssun1 ran 𝑓 ⊆ ( ran 𝑓 ∪ { 𝑦 } )
36 fss ( ( 𝑓 : ℕ ⟶ ran 𝑓 ∧ ran 𝑓 ⊆ ( ran 𝑓 ∪ { 𝑦 } ) ) → 𝑓 : ℕ ⟶ ( ran 𝑓 ∪ { 𝑦 } ) )
37 34 35 36 sylancl ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → 𝑓 : ℕ ⟶ ( ran 𝑓 ∪ { 𝑦 } ) )
38 24 14 25 8 30 23 37 lmss ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → ( 𝑓 ( ⇝𝑡𝐽 ) 𝑦𝑓 ( ⇝𝑡 ‘ ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) ) 𝑦 ) )
39 11 38 mpbid ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → 𝑓 ( ⇝𝑡 ‘ ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) ) 𝑦 )
40 37 ffvelrnda ( ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑓𝑘 ) ∈ ( ran 𝑓 ∪ { 𝑦 } ) )
41 simprl ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) )
42 41 ffvelrnda ( ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑓𝑘 ) ∈ ( 𝐽𝑥 ) )
43 42 eldifbd ( ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) ∧ 𝑘 ∈ ℕ ) → ¬ ( 𝑓𝑘 ) ∈ 𝑥 )
44 40 43 eldifd ( ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑓𝑘 ) ∈ ( ( ran 𝑓 ∪ { 𝑦 } ) ∖ 𝑥 ) )
45 difin ( ( ran 𝑓 ∪ { 𝑦 } ) ∖ ( ( ran 𝑓 ∪ { 𝑦 } ) ∩ 𝑥 ) ) = ( ( ran 𝑓 ∪ { 𝑦 } ) ∖ 𝑥 )
46 frn ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) → ran 𝑓 ⊆ ( 𝐽𝑥 ) )
47 46 ad2antrl ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → ran 𝑓 ⊆ ( 𝐽𝑥 ) )
48 47 difss2d ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → ran 𝑓 𝐽 )
49 13 snssd ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → { 𝑦 } ⊆ 𝐽 )
50 48 49 unssd ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → ( ran 𝑓 ∪ { 𝑦 } ) ⊆ 𝐽 )
51 3 restuni ( ( 𝐽 ∈ Top ∧ ( ran 𝑓 ∪ { 𝑦 } ) ⊆ 𝐽 ) → ( ran 𝑓 ∪ { 𝑦 } ) = ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) )
52 8 50 51 syl2anc ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → ( ran 𝑓 ∪ { 𝑦 } ) = ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) )
53 52 difeq1d ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → ( ( ran 𝑓 ∪ { 𝑦 } ) ∖ ( ( ran 𝑓 ∪ { 𝑦 } ) ∩ 𝑥 ) ) = ( ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) ∖ ( ( ran 𝑓 ∪ { 𝑦 } ) ∩ 𝑥 ) ) )
54 45 53 eqtr3id ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → ( ( ran 𝑓 ∪ { 𝑦 } ) ∖ 𝑥 ) = ( ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) ∖ ( ( ran 𝑓 ∪ { 𝑦 } ) ∩ 𝑥 ) ) )
55 incom ( ( ran 𝑓 ∪ { 𝑦 } ) ∩ 𝑥 ) = ( 𝑥 ∩ ( ran 𝑓 ∪ { 𝑦 } ) )
56 simplr ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) )
57 fss ( ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ ( 𝐽𝑥 ) ⊆ 𝐽 ) → 𝑓 : ℕ ⟶ 𝐽 )
58 41 2 57 sylancl ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → 𝑓 : ℕ ⟶ 𝐽 )
59 10 58 11 1stckgenlem ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) ∈ Comp )
60 kgeni ( ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) ∈ Comp ) → ( 𝑥 ∩ ( ran 𝑓 ∪ { 𝑦 } ) ) ∈ ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) )
61 56 59 60 syl2anc ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → ( 𝑥 ∩ ( ran 𝑓 ∪ { 𝑦 } ) ) ∈ ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) )
62 55 61 eqeltrid ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → ( ( ran 𝑓 ∪ { 𝑦 } ) ∩ 𝑥 ) ∈ ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) )
63 eqid ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) = ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) )
64 63 opncld ( ( ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) ∈ Top ∧ ( ( ran 𝑓 ∪ { 𝑦 } ) ∩ 𝑥 ) ∈ ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) ) → ( ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) ∖ ( ( ran 𝑓 ∪ { 𝑦 } ) ∩ 𝑥 ) ) ∈ ( Clsd ‘ ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) ) )
65 20 62 64 syl2anc ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → ( ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) ∖ ( ( ran 𝑓 ∪ { 𝑦 } ) ∩ 𝑥 ) ) ∈ ( Clsd ‘ ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) ) )
66 54 65 eqeltrd ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → ( ( ran 𝑓 ∪ { 𝑦 } ) ∖ 𝑥 ) ∈ ( Clsd ‘ ( 𝐽t ( ran 𝑓 ∪ { 𝑦 } ) ) ) )
67 14 22 23 39 44 66 lmcld ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → 𝑦 ∈ ( ( ran 𝑓 ∪ { 𝑦 } ) ∖ 𝑥 ) )
68 67 eldifbd ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → ¬ 𝑦𝑥 )
69 13 68 eldifd ( ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) ) → 𝑦 ∈ ( 𝐽𝑥 ) )
70 69 ex ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) → ( ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) → 𝑦 ∈ ( 𝐽𝑥 ) ) )
71 70 exlimdv ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) → ( ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( 𝐽𝑥 ) ∧ 𝑓 ( ⇝𝑡𝐽 ) 𝑦 ) → 𝑦 ∈ ( 𝐽𝑥 ) ) )
72 6 71 sylbid ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) → ( 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐽𝑥 ) ) → 𝑦 ∈ ( 𝐽𝑥 ) ) )
73 72 ssrdv ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝐽𝑥 ) ) ⊆ ( 𝐽𝑥 ) )
74 3 iscld4 ( ( 𝐽 ∈ Top ∧ ( 𝐽𝑥 ) ⊆ 𝐽 ) → ( ( 𝐽𝑥 ) ∈ ( Clsd ‘ 𝐽 ) ↔ ( ( cls ‘ 𝐽 ) ‘ ( 𝐽𝑥 ) ) ⊆ ( 𝐽𝑥 ) ) )
75 7 2 74 sylancl ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) → ( ( 𝐽𝑥 ) ∈ ( Clsd ‘ 𝐽 ) ↔ ( ( cls ‘ 𝐽 ) ‘ ( 𝐽𝑥 ) ) ⊆ ( 𝐽𝑥 ) ) )
76 73 75 mpbird ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) → ( 𝐽𝑥 ) ∈ ( Clsd ‘ 𝐽 ) )
77 elssuni ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) → 𝑥 ( 𝑘Gen ‘ 𝐽 ) )
78 77 adantl ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) → 𝑥 ( 𝑘Gen ‘ 𝐽 ) )
79 3 kgenuni ( 𝐽 ∈ Top → 𝐽 = ( 𝑘Gen ‘ 𝐽 ) )
80 7 79 syl ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) → 𝐽 = ( 𝑘Gen ‘ 𝐽 ) )
81 78 80 sseqtrrd ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) → 𝑥 𝐽 )
82 3 isopn2 ( ( 𝐽 ∈ Top ∧ 𝑥 𝐽 ) → ( 𝑥𝐽 ↔ ( 𝐽𝑥 ) ∈ ( Clsd ‘ 𝐽 ) ) )
83 7 81 82 syl2anc ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) → ( 𝑥𝐽 ↔ ( 𝐽𝑥 ) ∈ ( Clsd ‘ 𝐽 ) ) )
84 76 83 mpbird ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) → 𝑥𝐽 )
85 84 ex ( 𝐽 ∈ 1stω → ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) → 𝑥𝐽 ) )
86 85 ssrdv ( 𝐽 ∈ 1stω → ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 )
87 iskgen2 ( 𝐽 ∈ ran 𝑘Gen ↔ ( 𝐽 ∈ Top ∧ ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 ) )
88 1 86 87 sylanbrc ( 𝐽 ∈ 1stω → 𝐽 ∈ ran 𝑘Gen )