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	ffvelrnda	⊢ ( ( ( ( ( 𝐽 ∈ 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	43	rexeqdv	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( ∃ 𝑥 ∈ ( I ‘ 𝑆 ) 𝑥 ∈ ( 𝑔 ‘ 𝑛 ) ↔ ∃ 𝑥 ∈ 𝑆 𝑥 ∈ ( 𝑔 ‘ 𝑛 ) ) )
45	35 44	mpbird	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ 𝑛 ∈ ℕ ) → ∃ 𝑥 ∈ ( I ‘ 𝑆 ) 𝑥 ∈ ( 𝑔 ‘ 𝑛 ) )
46	45	ralrimiva	⊢ ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) → ∀ 𝑛 ∈ ℕ ∃ 𝑥 ∈ ( I ‘ 𝑆 ) 𝑥 ∈ ( 𝑔 ‘ 𝑛 ) )
47		fvex	⊢ ( I ‘ 𝑆 ) ∈ V
48		nnenom	⊢ ℕ ≈ ω
49		eleq1	⊢ ( 𝑥 = ( 𝑓 ‘ 𝑛 ) → ( 𝑥 ∈ ( 𝑔 ‘ 𝑛 ) ↔ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) )
50	47 48 49	axcc4	⊢ ( ∀ 𝑛 ∈ ℕ ∃ 𝑥 ∈ ( I ‘ 𝑆 ) 𝑥 ∈ ( 𝑔 ‘ 𝑛 ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( I ‘ 𝑆 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) )
51	46 50	syl	⊢ ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( I ‘ 𝑆 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) )
52	42	feq3d	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑓 : ℕ ⟶ ( I ‘ 𝑆 ) ↔ 𝑓 : ℕ ⟶ 𝑆 ) )
53	52	biimpd	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑓 : ℕ ⟶ ( I ‘ 𝑆 ) → 𝑓 : ℕ ⟶ 𝑆 ) )
54	53	adantr	⊢ ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) → ( 𝑓 : ℕ ⟶ ( I ‘ 𝑆 ) → 𝑓 : ℕ ⟶ 𝑆 ) )
55	6	ad2antrr	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) → 𝑃 ∈ 𝑋 )
56		simplr3	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) → ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) )
57		eleq2	⊢ ( 𝑥 = 𝑦 → ( 𝑃 ∈ 𝑥 ↔ 𝑃 ∈ 𝑦 ) )
58		fveq2	⊢ ( 𝑘 = 𝑗 → ( 𝑔 ‘ 𝑘 ) = ( 𝑔 ‘ 𝑗 ) )
59	58	sseq1d	⊢ ( 𝑘 = 𝑗 → ( ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ↔ ( 𝑔 ‘ 𝑗 ) ⊆ 𝑥 ) )
60	59	cbvrexvw	⊢ ( ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ↔ ∃ 𝑗 ∈ ℕ ( 𝑔 ‘ 𝑗 ) ⊆ 𝑥 )
61		sseq2	⊢ ( 𝑥 = 𝑦 → ( ( 𝑔 ‘ 𝑗 ) ⊆ 𝑥 ↔ ( 𝑔 ‘ 𝑗 ) ⊆ 𝑦 ) )
62	61	rexbidv	⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑗 ∈ ℕ ( 𝑔 ‘ 𝑗 ) ⊆ 𝑥 ↔ ∃ 𝑗 ∈ ℕ ( 𝑔 ‘ 𝑗 ) ⊆ 𝑦 ) )
63	60 62	syl5bb	⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ↔ ∃ 𝑗 ∈ ℕ ( 𝑔 ‘ 𝑗 ) ⊆ 𝑦 ) )
64	57 63	imbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ↔ ( 𝑃 ∈ 𝑦 → ∃ 𝑗 ∈ ℕ ( 𝑔 ‘ 𝑗 ) ⊆ 𝑦 ) ) )
65	64	rspccva	⊢ ( ( ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑃 ∈ 𝑦 → ∃ 𝑗 ∈ ℕ ( 𝑔 ‘ 𝑗 ) ⊆ 𝑦 ) )
66	56 65	sylan	⊢ ( ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑃 ∈ 𝑦 → ∃ 𝑗 ∈ ℕ ( 𝑔 ‘ 𝑗 ) ⊆ 𝑦 ) )
67		simpr	⊢ ( ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) → ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) )
68	67	ralimi	⊢ ( ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) → ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) )
69	9 68	syl	⊢ ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) → ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) )
70	69	adantr	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ ) ) ) → ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) )
71		simprrr	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ ) ) ) → 𝑗 ∈ ℕ )
72		fveq2	⊢ ( 𝑛 = 𝑗 → ( 𝑔 ‘ 𝑛 ) = ( 𝑔 ‘ 𝑗 ) )
73	72	sseq1d	⊢ ( 𝑛 = 𝑗 → ( ( 𝑔 ‘ 𝑛 ) ⊆ ( 𝑔 ‘ 𝑗 ) ↔ ( 𝑔 ‘ 𝑗 ) ⊆ ( 𝑔 ‘ 𝑗 ) ) )
74	73	imbi2d	⊢ ( 𝑛 = 𝑗 → ( ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) → ( 𝑔 ‘ 𝑛 ) ⊆ ( 𝑔 ‘ 𝑗 ) ) ↔ ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) → ( 𝑔 ‘ 𝑗 ) ⊆ ( 𝑔 ‘ 𝑗 ) ) ) )
75		fveq2	⊢ ( 𝑛 = 𝑚 → ( 𝑔 ‘ 𝑛 ) = ( 𝑔 ‘ 𝑚 ) )
76	75	sseq1d	⊢ ( 𝑛 = 𝑚 → ( ( 𝑔 ‘ 𝑛 ) ⊆ ( 𝑔 ‘ 𝑗 ) ↔ ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) ) )
77	76	imbi2d	⊢ ( 𝑛 = 𝑚 → ( ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) → ( 𝑔 ‘ 𝑛 ) ⊆ ( 𝑔 ‘ 𝑗 ) ) ↔ ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) → ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) ) ) )
78		fveq2	⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑔 ‘ 𝑛 ) = ( 𝑔 ‘ ( 𝑚 + 1 ) ) )
79	78	sseq1d	⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝑔 ‘ 𝑛 ) ⊆ ( 𝑔 ‘ 𝑗 ) ↔ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑗 ) ) )
80	79	imbi2d	⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) → ( 𝑔 ‘ 𝑛 ) ⊆ ( 𝑔 ‘ 𝑗 ) ) ↔ ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) → ( 𝑔 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑗 ) ) ) )
81		ssid	⊢ ( 𝑔 ‘ 𝑗 ) ⊆ ( 𝑔 ‘ 𝑗 )
82	81	2a1i	⊢ ( 𝑗 ∈ ℤ → ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) → ( 𝑔 ‘ 𝑗 ) ⊆ ( 𝑔 ‘ 𝑗 ) ) )
83		eluznn	⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → 𝑚 ∈ ℕ )
84		fvoveq1	⊢ ( 𝑘 = 𝑚 → ( 𝑔 ‘ ( 𝑘 + 1 ) ) = ( 𝑔 ‘ ( 𝑚 + 1 ) ) )
85		fveq2	⊢ ( 𝑘 = 𝑚 → ( 𝑔 ‘ 𝑘 ) = ( 𝑔 ‘ 𝑚 ) )
86	84 85	sseq12d	⊢ ( 𝑘 = 𝑚 → ( ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ↔ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑚 ) ) )
87	86	rspccva	⊢ ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑚 ∈ ℕ ) → ( 𝑔 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑚 ) )
88	83 87	sylan2	⊢ ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ) ) → ( 𝑔 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑚 ) )
89	88	anassrs	⊢ ( ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → ( 𝑔 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑚 ) )
90		sstr2	⊢ ( ( 𝑔 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑚 ) → ( ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) → ( 𝑔 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑗 ) ) )
91	89 90	syl	⊢ ( ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → ( ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) → ( 𝑔 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑗 ) ) )
92	91	expcom	⊢ ( 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) → ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) → ( 𝑔 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑗 ) ) ) )
93	92	a2d	⊢ ( 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) → ( ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) → ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) ) → ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) → ( 𝑔 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑗 ) ) ) )
94	74 77 80 77 82 93	uzind4	⊢ ( 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) → ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) → ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) ) )
95	94	com12	⊢ ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) → ( 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) → ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) ) )
96	95	ralrimiv	⊢ ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ∧ 𝑗 ∈ ℕ ) → ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) )
97	70 71 96	syl2anc	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ ) ) ) → ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) )
98		fveq2	⊢ ( 𝑛 = 𝑚 → ( 𝑓 ‘ 𝑛 ) = ( 𝑓 ‘ 𝑚 ) )
99	98 75	eleq12d	⊢ ( 𝑛 = 𝑚 → ( ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ↔ ( 𝑓 ‘ 𝑚 ) ∈ ( 𝑔 ‘ 𝑚 ) ) )
100		simplr	⊢ ( ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ ) ) → ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) )
101	100	ad2antlr	⊢ ( ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ ) ) ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) )
102	71 83	sylan	⊢ ( ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ ) ) ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → 𝑚 ∈ ℕ )
103	99 101 102	rspcdva	⊢ ( ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ ) ) ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → ( 𝑓 ‘ 𝑚 ) ∈ ( 𝑔 ‘ 𝑚 ) )
104	103	ralrimiva	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ ) ) ) → ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑓 ‘ 𝑚 ) ∈ ( 𝑔 ‘ 𝑚 ) )
105		r19.26	⊢ ( ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) ∧ ( 𝑓 ‘ 𝑚 ) ∈ ( 𝑔 ‘ 𝑚 ) ) ↔ ( ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) ∧ ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑓 ‘ 𝑚 ) ∈ ( 𝑔 ‘ 𝑚 ) ) )
106	97 104 105	sylanbrc	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ ) ) ) → ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) ∧ ( 𝑓 ‘ 𝑚 ) ∈ ( 𝑔 ‘ 𝑚 ) ) )
107		ssel2	⊢ ( ( ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) ∧ ( 𝑓 ‘ 𝑚 ) ∈ ( 𝑔 ‘ 𝑚 ) ) → ( 𝑓 ‘ 𝑚 ) ∈ ( 𝑔 ‘ 𝑗 ) )
108	107	ralimi	⊢ ( ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝑔 ‘ 𝑚 ) ⊆ ( 𝑔 ‘ 𝑗 ) ∧ ( 𝑓 ‘ 𝑚 ) ∈ ( 𝑔 ‘ 𝑚 ) ) → ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑓 ‘ 𝑚 ) ∈ ( 𝑔 ‘ 𝑗 ) )
109	106 108	syl	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ ) ) ) → ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑓 ‘ 𝑚 ) ∈ ( 𝑔 ‘ 𝑗 ) )
110		ssel	⊢ ( ( 𝑔 ‘ 𝑗 ) ⊆ 𝑦 → ( ( 𝑓 ‘ 𝑚 ) ∈ ( 𝑔 ‘ 𝑗 ) → ( 𝑓 ‘ 𝑚 ) ∈ 𝑦 ) )
111	110	ralimdv	⊢ ( ( 𝑔 ‘ 𝑗 ) ⊆ 𝑦 → ( ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑓 ‘ 𝑚 ) ∈ ( 𝑔 ‘ 𝑗 ) → ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑓 ‘ 𝑚 ) ∈ 𝑦 ) )
112	109 111	syl5com	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ ) ) ) → ( ( 𝑔 ‘ 𝑗 ) ⊆ 𝑦 → ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑓 ‘ 𝑚 ) ∈ 𝑦 ) )
113	112	anassrs	⊢ ( ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ ) ) → ( ( 𝑔 ‘ 𝑗 ) ⊆ 𝑦 → ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑓 ‘ 𝑚 ) ∈ 𝑦 ) )
114	113	anassrs	⊢ ( ( ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝑔 ‘ 𝑗 ) ⊆ 𝑦 → ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑓 ‘ 𝑚 ) ∈ 𝑦 ) )
115	114	reximdva	⊢ ( ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ 𝐽 ) → ( ∃ 𝑗 ∈ ℕ ( 𝑔 ‘ 𝑗 ) ⊆ 𝑦 → ∃ 𝑗 ∈ ℕ ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑓 ‘ 𝑚 ) ∈ 𝑦 ) )
116	66 115	syld	⊢ ( ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑃 ∈ 𝑦 → ∃ 𝑗 ∈ ℕ ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑓 ‘ 𝑚 ) ∈ 𝑦 ) )
117	116	ralrimiva	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) → ∀ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 → ∃ 𝑗 ∈ ℕ ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑓 ‘ 𝑚 ) ∈ 𝑦 ) )
118	36	ad2antrr	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) → 𝐽 ∈ Top )
119	1	toptopon	⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
120	118 119	sylib	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
121		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
122		1zzd	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) → 1 ∈ ℤ )
123		simprl	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) → 𝑓 : ℕ ⟶ 𝑆 )
124	39	ad2antrr	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) → 𝑆 ⊆ 𝑋 )
125	123 124	fssd	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) → 𝑓 : ℕ ⟶ 𝑋 )
126		eqidd	⊢ ( ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) ∧ 𝑚 ∈ ℕ ) → ( 𝑓 ‘ 𝑚 ) = ( 𝑓 ‘ 𝑚 ) )
127	120 121 122 125 126	lmbrf	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) → ( 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝑃 ∈ 𝑋 ∧ ∀ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 → ∃ 𝑗 ∈ ℕ ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝑓 ‘ 𝑚 ) ∈ 𝑦 ) ) ) )
128	55 117 127	mpbir2and	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) ) → 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 )
129	128	expr	⊢ ( ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) ∧ 𝑓 : ℕ ⟶ 𝑆 ) → ( ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) → 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) )
130	129	imdistanda	⊢ ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) → ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) → ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) )
131	54 130	syland	⊢ ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) → ( ( 𝑓 : ℕ ⟶ ( I ‘ 𝑆 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) → ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) )
132	131	eximdv	⊢ ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) → ( ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( I ‘ 𝑆 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) )
133	51 132	mpd	⊢ ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( 𝑔 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝑃 ∈ ( 𝑔 ‘ 𝑘 ) ∧ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) ) ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑥 ) ) ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) )
134	8 133	exlimddv	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) )
135	134	ex	⊢ ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) )
136	3	ad2antrr	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) → 𝐽 ∈ Top )
137	136 119	sylib	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
138		1zzd	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) → 1 ∈ ℤ )
139		simprr	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) → 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 )
140		simprl	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) → 𝑓 : ℕ ⟶ 𝑆 )
141	140	ffvelrnda	⊢ ( ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑓 ‘ 𝑘 ) ∈ 𝑆 )
142		simplr	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) → 𝑆 ⊆ 𝑋 )
143	121 137 138 139 141 142	lmcls	⊢ ( ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) → 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
144	143	ex	⊢ ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) → 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
145	144	exlimdv	⊢ ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) → ( ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) → 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
146	135 145	impbid	⊢ ( ( 𝐽 ∈ 1^stω ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ) ) )

Metamath Proof Explorer

Theorem 1stcelcls

Proof