1stcelcls

Description: A point belongs to the closure of a subset iff there is a sequence in the subset converging to it. Theorem 1.4-6(a) of Kreyszig p. 30. This proof uses countable choice ax-cc . A space satisfying the conclusion of this theorem is called a sequential space, so the theorem can also be stated as "every first-countable space is a sequential space". (Contributed by Mario Carneiro, 21-Mar-2015)

		Ref	Expression
	Hypothesis	1stcelcls.1	⊢ 𝑋 = ∪ 𝐽
	Assertion	1stcelcls	⊢ ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) )

Proof

Step	Hyp	Ref	Expression
1		1stcelcls.1	⊢ 𝑋 = ∪ 𝐽
2		simpll	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝐽 ∈ 1^stω )
3		1stctop	⊢ ( 𝐽 ∈ 1^stω → 𝐽 ∈ Top )
4	1	clsss3	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 )
5	3 4	sylan	⊢ ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 )
6	5	sselda	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑃 ∈ 𝑋 )
7	1	1stcfb	⊢ ( ( 𝐽 ∈ 1^stω ∧ 𝑃 ∈ 𝑋 ) → ∃ 𝑔 ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) )
8	2 6 7	syl2anc	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ∃ 𝑔 ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) )
9		simpr2	⊢ ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) → ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) )
10		simpl	⊢ ( ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) → 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) )
11	10	ralimi	⊢ ( ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) → ∀ 𝑘 ∈ ℕ 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) )
12	9 11	syl	⊢ ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) → ∀ 𝑘 ∈ ℕ 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) )
13		fveq2	⊢ ( 𝑘 = 𝑛 → ( 𝑔 ‘ 𝑘 ) = ( 𝑔 ‘ 𝑛 ) )
14	13	eleq2d	⊢ ( 𝑘 = 𝑛 → ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ↔ 𝑃 ∈ ( 𝑔 ‘ 𝑛 ) ) )
15	14	rspccva	⊢ ( ( ∀ 𝑘 ∈ ℕ 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ 𝑛 ∈ ℕ ) → 𝑃 ∈ ( 𝑔 ‘ 𝑛 ) )
16	12 15	sylan	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ 𝑛 ∈ ℕ ) → 𝑃 ∈ ( 𝑔 ‘ 𝑛 ) )
17		eleq2	⊢ ( 𝑦 = ( 𝑔 ‘ 𝑛 ) → ( 𝑃 ∈ 𝑦 ↔ 𝑃 ∈ ( 𝑔 ‘ 𝑛 ) ) )
18		ineq1	⊢ ( 𝑦 = ( 𝑔 ‘ 𝑛 ) → ( 𝑦 ∩ 𝑆 ) = ( ( 𝑔 ‘ 𝑛 ) ∩ 𝑆 ) )
19	18	neeq1d	⊢ ( 𝑦 = ( 𝑔 ‘ 𝑛 ) → ( ( 𝑦 ∩ 𝑆 ) ≠ ∅ ↔ ( ( 𝑔 ‘ 𝑛 ) ∩ 𝑆 ) ≠ ∅ ) )
20	17 19	imbi12d	⊢ ( 𝑦 = ( 𝑔 ‘ 𝑛 ) → ( ( 𝑃 ∈ 𝑦 → ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) ↔ ( 𝑃 ∈ ( 𝑔 ‘ 𝑛 ) → ( ( 𝑔 ‘ 𝑛 ) ∩ 𝑆 ) ≠ ∅ ) ) )
21	1	elcls2	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑃 ∈ 𝑋 ∧ ∀ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 → ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) ) ) )
22	3 21	sylan	⊢ ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑃 ∈ 𝑋 ∧ ∀ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 → ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) ) ) )
23	22	simplbda	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ∀ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 → ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) )
24	23	ad2antrr	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ 𝑛 ∈ ℕ ) → ∀ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 → ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) )
25		simpr1	⊢ ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) → 𝑔 : ℕ ⟶ 𝐽 )
26	25	ffvelcdmda	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑔 ‘ 𝑛 ) ∈ 𝐽 )
27	20 24 26	rspcdva	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑃 ∈ ( 𝑔 ‘ 𝑛 ) → ( ( 𝑔 ‘ 𝑛 ) ∩ 𝑆 ) ≠ ∅ ) )
28	16 27	mpd	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑔 ‘ 𝑛 ) ∩ 𝑆 ) ≠ ∅ )
29		elin	⊢ ( 𝑥 ∈ ( ( 𝑔 ‘ 𝑛 ) ∩ 𝑆 ) ↔ ( 𝑥 ∈ ( 𝑔 ‘ 𝑛 ) ∧ 𝑥 ∈ 𝑆 ) )
30	29	biancomi	⊢ ( 𝑥 ∈ ( ( 𝑔 ‘ 𝑛 ) ∩ 𝑆 ) ↔ ( 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑔 ‘ 𝑛 ) ) )
31	30	exbii	⊢ ( ∃ 𝑥 𝑥 ∈ ( ( 𝑔 ‘ 𝑛 ) ∩ 𝑆 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑔 ‘ 𝑛 ) ) )
32		n0	⊢ ( ( ( 𝑔 ‘ 𝑛 ) ∩ 𝑆 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( ( 𝑔 ‘ 𝑛 ) ∩ 𝑆 ) )
33		df-rex	⊢ ( ∃ 𝑥 ∈ 𝑆 𝑥 ∈ ( 𝑔 ‘ 𝑛 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑔 ‘ 𝑛 ) ) )
34	31 32 33	3bitr4i	⊢ ( ( ( 𝑔 ‘ 𝑛 ) ∩ 𝑆 ) ≠ ∅ ↔ ∃ 𝑥 ∈ 𝑆 𝑥 ∈ ( 𝑔 ‘ 𝑛 ) )
35	28 34	sylib	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ 𝑛 ∈ ℕ ) → ∃ 𝑥 ∈ 𝑆 𝑥 ∈ ( 𝑔 ‘ 𝑛 ) )
36	3	ad2antrr	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝐽 ∈ Top )
37	1	topopn	⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
38	36 37	syl	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑋 ∈ 𝐽 )
39		simplr	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ⊆ 𝑋 )
40	38 39	ssexd	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ∈ V )
41		fvi	⊢ ( 𝑆 ∈ V → ( I ‘ 𝑆 ) = 𝑆 )
42	40 41	syl	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( I ‘ 𝑆 ) = 𝑆 )
43	42	ad2antrr	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( I ‘ 𝑆 ) = 𝑆 )
44	35 43	rexeqtrrdv	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ 𝑛 ∈ ℕ ) → ∃ 𝑥 ∈ ( I ‘ 𝑆 ) 𝑥 ∈ ( 𝑔 ‘ 𝑛 ) )
45	44	ralrimiva	⊢ ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) → ∀ 𝑛 ∈ ℕ ∃ 𝑥 ∈ ( I ‘ 𝑆 ) 𝑥 ∈ ( 𝑔 ‘ 𝑛 ) )
46		fvex	⊢ ( I ‘ 𝑆 ) ∈ V
47		nnenom	⊢ ℕ ≈ ω
48		eleq1	⊢ ( 𝑥 = ( 𝑓 ‘ 𝑛 ) → ( 𝑥 ∈ ( 𝑔 ‘ 𝑛 ) ↔ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) )
49	46 47 48	axcc4	⊢ ( ∀ 𝑛 ∈ ℕ ∃ 𝑥 ∈ ( I ‘ 𝑆 ) 𝑥 ∈ ( 𝑔 ‘ 𝑛 ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( I ‘ 𝑆 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) )
50	45 49	syl	⊢ ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( I ‘ 𝑆 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) )
51	42	feq3d	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑓 : ℕ ⟶ ( I ‘ 𝑆 ) ↔ 𝑓 : ℕ ⟶ 𝑆 ) )
52	51	biimpd	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑓 : ℕ ⟶ ( I ‘ 𝑆 ) → 𝑓 : ℕ ⟶ 𝑆 ) )
53	52	adantr	⊢ ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) → ( 𝑓 : ℕ ⟶ ( I ‘ 𝑆 ) → 𝑓 : ℕ ⟶ 𝑆 ) )
54	6	ad2antrr	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) → 𝑃 ∈ 𝑋 )
55		simplr3	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) → ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) )
56		eleq2	⊢ ( 𝑥 = 𝑦 → ( 𝑃 ∈ 𝑥 ↔ 𝑃 ∈ 𝑦 ) )
57		fveq2	⊢ ( 𝑘 = 𝑗 → ( 𝑔 ‘ 𝑘 ) = ( 𝑔 ‘ 𝑗 ) )
58	57	sseq1d	⊢ ( 𝑘 = 𝑗 → ( ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ↔ ( 𝑔 ‘ 𝑗 ) ⊆ 𝑥 ) )
59	58	cbvrexvw	⊢ ( ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ↔ ∃ 𝑗 ∈ ℕ ( 𝑔 ‘ 𝑗 ) ⊆ 𝑥 )
60		sseq2	⊢ ( 𝑥 = 𝑦 → ( ( 𝑔 ‘ 𝑗 ) ⊆ 𝑥 ↔ ( 𝑔 ‘ 𝑗 ) ⊆ 𝑦 ) )
61	60	rexbidv	⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑗 ∈ ℕ ( 𝑔 ‘ 𝑗 ) ⊆ 𝑥 ↔ ∃ 𝑗 ∈ ℕ ( 𝑔 ‘ 𝑗 ) ⊆ 𝑦 ) )
62	59 61	bitrid	⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ↔ ∃ 𝑗 ∈ ℕ ( 𝑔 ‘ 𝑗 ) ⊆ 𝑦 ) )
63	56 62	imbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ↔ ( 𝑃 ∈ 𝑦 → ∃ 𝑗 ∈ ℕ ( 𝑔 ‘ 𝑗 ) ⊆ 𝑦 ) ) )
64	63	rspccva	⊢ ( ( ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑃 ∈ 𝑦 → ∃ 𝑗 ∈ ℕ ( 𝑔 ‘ 𝑗 ) ⊆ 𝑦 ) )
65	55 64	sylan	⊢ ( ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑃 ∈ 𝑦 → ∃ 𝑗 ∈ ℕ ( 𝑔 ‘ 𝑗 ) ⊆ 𝑦 ) )
66		simpr	⊢ ( ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) → ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) )
67	66	ralimi	⊢ ( ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) → ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) )
68	9 67	syl	⊢ ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) → ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) )
69	68	adantr	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ ) ) ) → ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) )
70		simprrr	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ ) ) ) → 𝑗 ∈ ℕ )
71		fveq2	⊢ ( 𝑛 = 𝑗 → ( 𝑔 ‘ 𝑛 ) = ( 𝑔 ‘ 𝑗 ) )
72	71	sseq1d	⊢ ( 𝑛 = 𝑗 → ( ( 𝑔 ‘ 𝑛 ) ⊆ ( 𝑔 ‘ 𝑗 ) ↔ ( 𝑔 ‘ 𝑗 ) ⊆ ( 𝑔 ‘ 𝑗 ) ) )
73	72	imbi2d	⊢ ( 𝑛 = 𝑗 → ( ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) → ( 𝑔 ‘ 𝑛 ) ⊆ ( 𝑔 ‘ 𝑗 ) ) ↔ ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) → ( 𝑔 ‘ 𝑗 ) ⊆ ( 𝑔 ‘ 𝑗 ) ) ) )
74		fveq2	⊢ ( 𝑛 = 𝑚 → ( 𝑔 ‘ 𝑛 ) = ( 𝑔 ‘ 𝑚 ) )
75	74	sseq1d	⊢ ( 𝑛 = 𝑚 → ( ( 𝑔 ‘ 𝑛 ) ⊆ ( 𝑔 ‘ 𝑗 ) ↔ ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) ) )
76	75	imbi2d	⊢ ( 𝑛 = 𝑚 → ( ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) → ( 𝑔 ‘ 𝑛 ) ⊆ ( 𝑔 ‘ 𝑗 ) ) ↔ ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) → ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) ) ) )
77		fveq2	⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑔 ‘ 𝑛 ) = ( 𝑔 ‘ ( 𝑚 + 1 ) ) )
78	77	sseq1d	⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝑔 ‘ 𝑛 ) ⊆ ( 𝑔 ‘ 𝑗 ) ↔ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑗 ) ) )
79	78	imbi2d	⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) → ( 𝑔 ‘ 𝑛 ) ⊆ ( 𝑔 ‘ 𝑗 ) ) ↔ ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) → ( 𝑔 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑗 ) ) ) )
80		ssid	⊢ ( 𝑔 ‘ 𝑗 ) ⊆ ( 𝑔 ‘ 𝑗 )
81	80	2a1i	⊢ ( 𝑗 ∈ ℤ → ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) → ( 𝑔 ‘ 𝑗 ) ⊆ ( 𝑔 ‘ 𝑗 ) ) )
82		eluznn	⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → 𝑚 ∈ ℕ )
83		fvoveq1	⊢ ( 𝑘 = 𝑚 → ( 𝑔 ‘ ( 𝑘 + 1 ) ) = ( 𝑔 ‘ ( 𝑚 + 1 ) ) )
84		fveq2	⊢ ( 𝑘 = 𝑚 → ( 𝑔 ‘ 𝑘 ) = ( 𝑔 ‘ 𝑚 ) )
85	83 84	sseq12d	⊢ ( 𝑘 = 𝑚 → ( ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ↔ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑚 ) ) )
86	85	rspccva	⊢ ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑚 ∈ ℕ ) → ( 𝑔 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑚 ) )
87	82 86	sylan2	⊢ ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ) ) → ( 𝑔 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑚 ) )
88	87	anassrs	⊢ ( ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → ( 𝑔 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑚 ) )
89		sstr2	⊢ ( ( 𝑔 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑚 ) → ( ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) → ( 𝑔 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑗 ) ) )
90	88 89	syl	⊢ ( ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → ( ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) → ( 𝑔 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑗 ) ) )
91	90	expcom	⊢ ( 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) → ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) → ( 𝑔 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑗 ) ) ) )
92	91	a2d	⊢ ( 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) → ( ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) → ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) ) → ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) → ( 𝑔 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑗 ) ) ) )
93	73 76 79 76 81 92	uzind4	⊢ ( 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) → ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) → ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) ) )
94	93	com12	⊢ ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) → ( 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) → ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) ) )
95	94	ralrimiv	⊢ ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) → ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) )
96	69 70 95	syl2anc	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ ) ) ) → ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) )
97		fveq2	⊢ ( 𝑛 = 𝑚 → ( 𝑓 ‘ 𝑛 ) = ( 𝑓 ‘ 𝑚 ) )
98	97 74	eleq12d	⊢ ( 𝑛 = 𝑚 → ( ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ↔ ( 𝑓 ‘ 𝑚 ) ∈ ( 𝑔 ‘ 𝑚 ) ) )
99		simplr	⊢ ( ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ ) ) → ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) )
100	99	ad2antlr	⊢ ( ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ ) ) ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) )
101	70 82	sylan	⊢ ( ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ ) ) ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → 𝑚 ∈ ℕ )
102	98 100 101	rspcdva	⊢ ( ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ ) ) ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → ( 𝑓 ‘ 𝑚 ) ∈ ( 𝑔 ‘ 𝑚 ) )
103	102	ralrimiva	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ ) ) ) → ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑓 ‘ 𝑚 ) ∈ ( 𝑔 ‘ 𝑚 ) )
104		r19.26	⊢ ( ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) ∧ ( 𝑓 ‘ 𝑚 ) ∈ ( 𝑔 ‘ 𝑚 ) ) ↔ ( ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) ∧ ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑓 ‘ 𝑚 ) ∈ ( 𝑔 ‘ 𝑚 ) ) )
105	96 103 104	sylanbrc	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ ) ) ) → ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) ∧ ( 𝑓 ‘ 𝑚 ) ∈ ( 𝑔 ‘ 𝑚 ) ) )
106		ssel2	⊢ ( ( ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) ∧ ( 𝑓 ‘ 𝑚 ) ∈ ( 𝑔 ‘ 𝑚 ) ) → ( 𝑓 ‘ 𝑚 ) ∈ ( 𝑔 ‘ 𝑗 ) )
107	106	ralimi	⊢ ( ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) ∧ ( 𝑓 ‘ 𝑚 ) ∈ ( 𝑔 ‘ 𝑚 ) ) → ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑓 ‘ 𝑚 ) ∈ ( 𝑔 ‘ 𝑗 ) )
108	105 107	syl	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ ) ) ) → ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑓 ‘ 𝑚 ) ∈ ( 𝑔 ‘ 𝑗 ) )
109		ssel	⊢ ( ( 𝑔 ‘ 𝑗 ) ⊆ 𝑦 → ( ( 𝑓 ‘ 𝑚 ) ∈ ( 𝑔 ‘ 𝑗 ) → ( 𝑓 ‘ 𝑚 ) ∈ 𝑦 ) )
110	109	ralimdv	⊢ ( ( 𝑔 ‘ 𝑗 ) ⊆ 𝑦 → ( ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑓 ‘ 𝑚 ) ∈ ( 𝑔 ‘ 𝑗 ) → ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑓 ‘ 𝑚 ) ∈ 𝑦 ) )
111	108 110	syl5com	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ ) ) ) → ( ( 𝑔 ‘ 𝑗 ) ⊆ 𝑦 → ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑓 ‘ 𝑚 ) ∈ 𝑦 ) )
112	111	anassrs	⊢ ( ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ ) ) → ( ( 𝑔 ‘ 𝑗 ) ⊆ 𝑦 → ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑓 ‘ 𝑚 ) ∈ 𝑦 ) )
113	112	anassrs	⊢ ( ( ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝑔 ‘ 𝑗 ) ⊆ 𝑦 → ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑓 ‘ 𝑚 ) ∈ 𝑦 ) )
114	113	reximdva	⊢ ( ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ 𝐽 ) → ( ∃ 𝑗 ∈ ℕ ( 𝑔 ‘ 𝑗 ) ⊆ 𝑦 → ∃ 𝑗 ∈ ℕ ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑓 ‘ 𝑚 ) ∈ 𝑦 ) )
115	65 114	syld	⊢ ( ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑃 ∈ 𝑦 → ∃ 𝑗 ∈ ℕ ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑓 ‘ 𝑚 ) ∈ 𝑦 ) )
116	115	ralrimiva	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) → ∀ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 → ∃ 𝑗 ∈ ℕ ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑓 ‘ 𝑚 ) ∈ 𝑦 ) )
117	36	ad2antrr	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) → 𝐽 ∈ Top )
118	1	toptopon	⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
119	117 118	sylib	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
120		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
121		1zzd	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) → 1 ∈ ℤ )
122		simprl	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) → 𝑓 : ℕ ⟶ 𝑆 )
123	39	ad2antrr	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) → 𝑆 ⊆ 𝑋 )
124	122 123	fssd	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) → 𝑓 : ℕ ⟶ 𝑋 )
125		eqidd	⊢ ( ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) ∧ 𝑚 ∈ ℕ ) → ( 𝑓 ‘ 𝑚 ) = ( 𝑓 ‘ 𝑚 ) )
126	119 120 121 124 125	lmbrf	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) → ( 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝑃 ∈ 𝑋 ∧ ∀ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 → ∃ 𝑗 ∈ ℕ ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑓 ‘ 𝑚 ) ∈ 𝑦 ) ) ) )
127	54 116 126	mpbir2and	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) → 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 )
128	127	expr	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ 𝑓 : ℕ ⟶ 𝑆 ) → ( ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) → 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) )
129	128	imdistanda	⊢ ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) → ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) → ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) )
130	53 129	syland	⊢ ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) → ( ( 𝑓 : ℕ ⟶ ( I ‘ 𝑆 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) → ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) )
131	130	eximdv	⊢ ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) → ( ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( I ‘ 𝑆 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) )
132	50 131	mpd	⊢ ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) )
133	8 132	exlimddv	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) )
134	133	ex	⊢ ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) )
135	3	ad2antrr	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) → 𝐽 ∈ Top )
136	135 118	sylib	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
137		1zzd	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) → 1 ∈ ℤ )
138		simprr	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) → 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 )
139		simprl	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) → 𝑓 : ℕ ⟶ 𝑆 )
140	139	ffvelcdmda	⊢ ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑓 ‘ 𝑘 ) ∈ 𝑆 )
141		simplr	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) → 𝑆 ⊆ 𝑋 )
142	120 136 137 138 140 141	lmcls	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) → 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
143	142	ex	⊢ ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) → 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
144	143	exlimdv	⊢ ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) → ( ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) → 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
145	134 144	impbid	⊢ ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) )

Metamath Proof Explorer

Theorem 1stcelcls

Proof