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 )