1stckgen

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

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

Proof

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

Metamath Proof Explorer

Theorem 1stckgen

Proof