Theorem 1stcelcls 21264

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 9257. 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.)

Hypothesis

Ref	Expression
1stcelcls.1	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
1stcelcls	⊢ ((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)))

Distinct variable groups:   𝑓,𝐽   𝑃,𝑓   𝑆,𝑓   𝑓,𝑋

Proof of Theorem 1stcelcls

Dummy variables 𝑔 𝑗 𝑘 𝑚 𝑛 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpll 790	. . . . 5 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝐽 ∈ 1st𝜔)
2		1stctop 21246	. . . . . . 7 ⊢ (𝐽 ∈ 1st𝜔 → 𝐽 ∈ Top)
3		1stcelcls.1	. . . . . . . 8 ⊢ 𝑋 = ∪ 𝐽
4	3	clsss3 20863	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋)
5	2, 4	sylan 488	. . . . . 6 ⊢ ((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋)
6	5	sselda 3603	. . . . 5 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑃 ∈ 𝑋)
7	3	1stcfb 21248	. . . . 5 ⊢ ((𝐽 ∈ 1st𝜔 ∧ 𝑃 ∈ 𝑋) → ∃𝑔(𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥)))
8	1, 6, 7	syl2anc 693	. . . 4 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → ∃𝑔(𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥)))
9		simpr1 1067	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → 𝑔:ℕ⟶𝐽)
10	9	ffvelrnda 6359	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → (𝑔‘𝑛) ∈ 𝐽)
11	3	elcls2 20878	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅))))
12	2, 11	sylan 488	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅))))
13	12	simplbda 654	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅))
14	13	ad2antrr 762	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅))
15		simpr2 1068	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)))
16		simpl 473	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) → 𝑃 ∈ (𝑔‘𝑘))
17	16	ralimi 2952	. . . . . . . . . . . 12 ⊢ (∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) → ∀𝑘 ∈ ℕ 𝑃 ∈ (𝑔‘𝑘))
18	15, 17	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∀𝑘 ∈ ℕ 𝑃 ∈ (𝑔‘𝑘))
19		fveq2 6191	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → (𝑔‘𝑘) = (𝑔‘𝑛))
20	19	eleq2d 2687	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → (𝑃 ∈ (𝑔‘𝑘) ↔ 𝑃 ∈ (𝑔‘𝑛)))
21	20	rspccva 3308	. . . . . . . . . . 11 ⊢ ((∀𝑘 ∈ ℕ 𝑃 ∈ (𝑔‘𝑘) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ (𝑔‘𝑛))
22	18, 21	sylan 488	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ (𝑔‘𝑛))
23		eleq2 2690	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑔‘𝑛) → (𝑃 ∈ 𝑦 ↔ 𝑃 ∈ (𝑔‘𝑛)))
24		ineq1 3807	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑔‘𝑛) → (𝑦 ∩ 𝑆) = ((𝑔‘𝑛) ∩ 𝑆))
25	24	neeq1d 2853	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑔‘𝑛) → ((𝑦 ∩ 𝑆) ≠ ∅ ↔ ((𝑔‘𝑛) ∩ 𝑆) ≠ ∅))
26	23, 25	imbi12d 334	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑔‘𝑛) → ((𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅) ↔ (𝑃 ∈ (𝑔‘𝑛) → ((𝑔‘𝑛) ∩ 𝑆) ≠ ∅)))
27	26	rspcv 3305	. . . . . . . . . 10 ⊢ ((𝑔‘𝑛) ∈ 𝐽 → (∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅) → (𝑃 ∈ (𝑔‘𝑛) → ((𝑔‘𝑛) ∩ 𝑆) ≠ ∅)))
28	10, 14, 22, 27	syl3c 66	. . . . . . . . 9 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ((𝑔‘𝑛) ∩ 𝑆) ≠ ∅)
29		elin 3796	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((𝑔‘𝑛) ∩ 𝑆) ↔ (𝑥 ∈ (𝑔‘𝑛) ∧ 𝑥 ∈ 𝑆))
30		ancom 466	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (𝑔‘𝑛) ∧ 𝑥 ∈ 𝑆) ↔ (𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑔‘𝑛)))
31	29, 30	bitri 264	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ((𝑔‘𝑛) ∩ 𝑆) ↔ (𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑔‘𝑛)))
32	31	exbii 1774	. . . . . . . . . 10 ⊢ (∃𝑥 𝑥 ∈ ((𝑔‘𝑛) ∩ 𝑆) ↔ ∃𝑥(𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑔‘𝑛)))
33		n0 3931	. . . . . . . . . 10 ⊢ (((𝑔‘𝑛) ∩ 𝑆) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ ((𝑔‘𝑛) ∩ 𝑆))
34		df-rex 2918	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝑆 𝑥 ∈ (𝑔‘𝑛) ↔ ∃𝑥(𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑔‘𝑛)))
35	32, 33, 34	3bitr4i 292	. . . . . . . . 9 ⊢ (((𝑔‘𝑛) ∩ 𝑆) ≠ ∅ ↔ ∃𝑥 ∈ 𝑆 𝑥 ∈ (𝑔‘𝑛))
36	28, 35	sylib 208	. . . . . . . 8 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ∃𝑥 ∈ 𝑆 𝑥 ∈ (𝑔‘𝑛))
37	2	ad2antrr 762	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝐽 ∈ Top)
38	3	topopn 20711	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
39	37, 38	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑋 ∈ 𝐽)
40		simplr 792	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ⊆ 𝑋)
41	39, 40	ssexd 4805	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ∈ V)
42		fvi 6255	. . . . . . . . . . 11 ⊢ (𝑆 ∈ V → ( I ‘𝑆) = 𝑆)
43	41, 42	syl 17	. . . . . . . . . 10 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → ( I ‘𝑆) = 𝑆)
44	43	ad2antrr 762	. . . . . . . . 9 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ( I ‘𝑆) = 𝑆)
45	44	rexeqdv 3145	. . . . . . . 8 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → (∃𝑥 ∈ ( I ‘𝑆)𝑥 ∈ (𝑔‘𝑛) ↔ ∃𝑥 ∈ 𝑆 𝑥 ∈ (𝑔‘𝑛)))
46	36, 45	mpbird 247	. . . . . . 7 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ∃𝑥 ∈ ( I ‘𝑆)𝑥 ∈ (𝑔‘𝑛))
47	46	ralrimiva 2966	. . . . . 6 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∀𝑛 ∈ ℕ ∃𝑥 ∈ ( I ‘𝑆)𝑥 ∈ (𝑔‘𝑛))
48		fvex 6201	. . . . . . 7 ⊢ ( I ‘𝑆) ∈ V
49		nnenom 12779	. . . . . . 7 ⊢ ℕ ≈ ω
50		eleq1 2689	. . . . . . 7 ⊢ (𝑥 = (𝑓‘𝑛) → (𝑥 ∈ (𝑔‘𝑛) ↔ (𝑓‘𝑛) ∈ (𝑔‘𝑛)))
51	48, 49, 50	axcc4 9261	. . . . . 6 ⊢ (∀𝑛 ∈ ℕ ∃𝑥 ∈ ( I ‘𝑆)𝑥 ∈ (𝑔‘𝑛) → ∃𝑓(𝑓:ℕ⟶( I ‘𝑆) ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)))
52	47, 51	syl 17	. . . . 5 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∃𝑓(𝑓:ℕ⟶( I ‘𝑆) ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)))
53	43	feq3d 6032	. . . . . . . . 9 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → (𝑓:ℕ⟶( I ‘𝑆) ↔ 𝑓:ℕ⟶𝑆))
54	53	biimpd 219	. . . . . . . 8 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → (𝑓:ℕ⟶( I ‘𝑆) → 𝑓:ℕ⟶𝑆))
55	54	adantr 481	. . . . . . 7 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → (𝑓:ℕ⟶( I ‘𝑆) → 𝑓:ℕ⟶𝑆))
56	6	ad2antrr 762	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝑃 ∈ 𝑋)
57		simplr3 1105	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))
58		eleq2 2690	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑃 ∈ 𝑥 ↔ 𝑃 ∈ 𝑦))
59		fveq2 6191	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → (𝑔‘𝑘) = (𝑔‘𝑗))
60	59	sseq1d 3632	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑗 → ((𝑔‘𝑘) ⊆ 𝑥 ↔ (𝑔‘𝑗) ⊆ 𝑥))
61	60	cbvrexv 3172	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥 ↔ ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑥)
62		sseq2 3627	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → ((𝑔‘𝑗) ⊆ 𝑥 ↔ (𝑔‘𝑗) ⊆ 𝑦))
63	62	rexbidv 3052	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑥 ↔ ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦))
64	61, 63	syl5bb 272	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥 ↔ ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦))
65	58, 64	imbi12d 334	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥) ↔ (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦)))
66	65	rspccva 3308	. . . . . . . . . . . . 13 ⊢ ((∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥) ∧ 𝑦 ∈ 𝐽) → (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦))
67	57, 66	sylan 488	. . . . . . . . . . . 12 ⊢ ((((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ 𝑦 ∈ 𝐽) → (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦))
68		simpr 477	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) → (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘))
69	68	ralimi 2952	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘))
70	15, 69	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘))
71	70	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘))
72		simprrr 805	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → 𝑗 ∈ ℕ)
73		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑗 → (𝑔‘𝑛) = (𝑔‘𝑗))
74	73	sseq1d 3632	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑗 → ((𝑔‘𝑛) ⊆ (𝑔‘𝑗) ↔ (𝑔‘𝑗) ⊆ (𝑔‘𝑗)))
75	74	imbi2d 330	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑗 → (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑛) ⊆ (𝑔‘𝑗)) ↔ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑗) ⊆ (𝑔‘𝑗))))
76		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑚 → (𝑔‘𝑛) = (𝑔‘𝑚))
77	76	sseq1d 3632	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑚 → ((𝑔‘𝑛) ⊆ (𝑔‘𝑗) ↔ (𝑔‘𝑚) ⊆ (𝑔‘𝑗)))
78	77	imbi2d 330	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑚 → (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑛) ⊆ (𝑔‘𝑗)) ↔ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑚) ⊆ (𝑔‘𝑗))))
79		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = (𝑚 + 1) → (𝑔‘𝑛) = (𝑔‘(𝑚 + 1)))
80	79	sseq1d 3632	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = (𝑚 + 1) → ((𝑔‘𝑛) ⊆ (𝑔‘𝑗) ↔ (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑗)))
81	80	imbi2d 330	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = (𝑚 + 1) → (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑛) ⊆ (𝑔‘𝑗)) ↔ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑗))))
82		ssid 3624	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔‘𝑗) ⊆ (𝑔‘𝑗)
83	82	2a1i 12	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ ℤ → ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑗) ⊆ (𝑔‘𝑗)))
84		eluznn 11758	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ ℕ ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → 𝑚 ∈ ℕ)
85		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 = 𝑚 → (𝑘 + 1) = (𝑚 + 1))
86	85	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝑚 → (𝑔‘(𝑘 + 1)) = (𝑔‘(𝑚 + 1)))
87		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝑚 → (𝑔‘𝑘) = (𝑔‘𝑚))
88	86, 87	sseq12d 3634	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 𝑚 → ((𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ↔ (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑚)))
89	88	rspccva 3308	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑚 ∈ ℕ) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑚))
90	84, 89	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ (𝑗 ∈ ℕ ∧ 𝑚 ∈ (ℤ≥‘𝑗))) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑚))
91	90	anassrs 680	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑚))
92		sstr2 3610	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑚) → ((𝑔‘𝑚) ⊆ (𝑔‘𝑗) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑗)))
93	91, 92	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → ((𝑔‘𝑚) ⊆ (𝑔‘𝑗) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑗)))
94	93	expcom 451	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ (ℤ≥‘𝑗) → ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → ((𝑔‘𝑚) ⊆ (𝑔‘𝑗) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑗))))
95	94	a2d 29	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ (ℤ≥‘𝑗) → (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑚) ⊆ (𝑔‘𝑗)) → ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑗))))
96	75, 78, 81, 78, 83, 95	uzind4 11746	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ (ℤ≥‘𝑗) → ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑚) ⊆ (𝑔‘𝑗)))
97	96	com12 32	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑚 ∈ (ℤ≥‘𝑗) → (𝑔‘𝑚) ⊆ (𝑔‘𝑗)))
98	97	ralrimiv 2965	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑔‘𝑚) ⊆ (𝑔‘𝑗))
99	71, 72, 98	syl2anc 693	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑔‘𝑚) ⊆ (𝑔‘𝑗))
100	72, 84	sylan 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → 𝑚 ∈ ℕ)
101		simplr 792	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ)) → ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))
102	101	ad2antlr 763	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))
103		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑚 → (𝑓‘𝑛) = (𝑓‘𝑚))
104	103, 76	eleq12d 2695	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑚 → ((𝑓‘𝑛) ∈ (𝑔‘𝑛) ↔ (𝑓‘𝑚) ∈ (𝑔‘𝑚)))
105	104	rspcv 3305	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ ℕ → (∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛) → (𝑓‘𝑚) ∈ (𝑔‘𝑚)))
106	100, 102, 105	sylc 65	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (𝑓‘𝑚) ∈ (𝑔‘𝑚))
107	106	ralrimiva 2966	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ (𝑔‘𝑚))
108		r19.26 3064	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑚 ∈ (ℤ≥‘𝑗)((𝑔‘𝑚) ⊆ (𝑔‘𝑗) ∧ (𝑓‘𝑚) ∈ (𝑔‘𝑚)) ↔ (∀𝑚 ∈ (ℤ≥‘𝑗)(𝑔‘𝑚) ⊆ (𝑔‘𝑗) ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ (𝑔‘𝑚)))
109	99, 107, 108	sylanbrc 698	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ∀𝑚 ∈ (ℤ≥‘𝑗)((𝑔‘𝑚) ⊆ (𝑔‘𝑗) ∧ (𝑓‘𝑚) ∈ (𝑔‘𝑚)))
110		ssel2 3598	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑔‘𝑚) ⊆ (𝑔‘𝑗) ∧ (𝑓‘𝑚) ∈ (𝑔‘𝑚)) → (𝑓‘𝑚) ∈ (𝑔‘𝑗))
111	110	ralimi 2952	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑚 ∈ (ℤ≥‘𝑗)((𝑔‘𝑚) ⊆ (𝑔‘𝑗) ∧ (𝑓‘𝑚) ∈ (𝑔‘𝑚)) → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ (𝑔‘𝑗))
112	109, 111	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ (𝑔‘𝑗))
113		ssel 3597	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔‘𝑗) ⊆ 𝑦 → ((𝑓‘𝑚) ∈ (𝑔‘𝑗) → (𝑓‘𝑚) ∈ 𝑦))
114	113	ralimdv 2963	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔‘𝑗) ⊆ 𝑦 → (∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ (𝑔‘𝑗) → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))
115	112, 114	syl5com 31	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ((𝑔‘𝑗) ⊆ 𝑦 → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))
116	115	anassrs 680	. . . . . . . . . . . . . 14 ⊢ ((((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ)) → ((𝑔‘𝑗) ⊆ 𝑦 → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))
117	116	anassrs 680	. . . . . . . . . . . . 13 ⊢ (((((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ 𝑦 ∈ 𝐽) ∧ 𝑗 ∈ ℕ) → ((𝑔‘𝑗) ⊆ 𝑦 → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))
118	117	reximdva 3017	. . . . . . . . . . . 12 ⊢ ((((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ 𝑦 ∈ 𝐽) → (∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦 → ∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))
119	67, 118	syld 47	. . . . . . . . . . 11 ⊢ ((((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ 𝑦 ∈ 𝐽) → (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))
120	119	ralrimiva 2966	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))
121	37	ad2antrr 762	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝐽 ∈ Top)
122	3	toptopon 20722	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
123	121, 122	sylib 208	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝐽 ∈ (TopOn‘𝑋))
124		nnuz 11723	. . . . . . . . . . 11 ⊢ ℕ = (ℤ≥‘1)
125		1zzd 11408	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 1 ∈ ℤ)
126		simprl 794	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝑓:ℕ⟶𝑆)
127	40	ad2antrr 762	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝑆 ⊆ 𝑋)
128	126, 127	fssd 6057	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝑓:ℕ⟶𝑋)
129		eqidd 2623	. . . . . . . . . . 11 ⊢ ((((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ 𝑚 ∈ ℕ) → (𝑓‘𝑚) = (𝑓‘𝑚))
130	123, 124, 125, 128, 129	lmbrf 21064	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → (𝑓(⇝𝑡‘𝐽)𝑃 ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))))
131	56, 120, 130	mpbir2and 957	. . . . . . . . 9 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝑓(⇝𝑡‘𝐽)𝑃)
132	131	expr 643	. . . . . . . 8 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑓:ℕ⟶𝑆) → (∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛) → 𝑓(⇝𝑡‘𝐽)𝑃))
133	132	imdistanda 729	. . . . . . 7 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) → (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)))
134	55, 133	syland 498	. . . . . 6 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ((𝑓:ℕ⟶( I ‘𝑆) ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) → (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)))
135	134	eximdv 1846	. . . . 5 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → (∃𝑓(𝑓:ℕ⟶( I ‘𝑆) ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) → ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)))
136	52, 135	mpd 15	. . . 4 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃))
137	8, 136	exlimddv 1863	. . 3 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃))
138	137	ex 450	. 2 ⊢ ((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) → ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)))
139	2	ad2antrr 762	. . . . . 6 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝐽 ∈ Top)
140	139, 122	sylib 208	. . . . 5 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝐽 ∈ (TopOn‘𝑋))
141		1zzd 11408	. . . . 5 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 1 ∈ ℤ)
142		simprr 796	. . . . 5 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝑓(⇝𝑡‘𝐽)𝑃)
143		simprl 794	. . . . . 6 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝑓:ℕ⟶𝑆)
144	143	ffvelrnda 6359	. . . . 5 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) ∈ 𝑆)
145		simplr 792	. . . . 5 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝑆 ⊆ 𝑋)
146	124, 140, 141, 142, 144, 145	lmcls 21106	. . . 4 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝑃 ∈ ((cls‘𝐽)‘𝑆))
147	146	ex 450	. . 3 ⊢ ((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) → ((𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → 𝑃 ∈ ((cls‘𝐽)‘𝑆)))
148	147	exlimdv 1861	. 2 ⊢ ((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) → (∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → 𝑃 ∈ ((cls‘𝐽)‘𝑆)))
149	138, 148	impbid 202	1 ⊢ ((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1037   = wceq 1483  ∃wex 1704   ∈ wcel 1990   ≠ wne 2794  ∀wral 2912  ∃wrex 2913  Vcvv 3200   ∩ cin 3573   ⊆ wss 3574  ∅c0 3915  ∪ cuni 4436   class class class wbr 4653   I cid 5023  ⟶wf 5884  ‘cfv 5888  (class class class)co 6650  1c1 9937   + caddc 9939  ℕcn 11020  ℤcz 11377  ℤ_≥cuz 11687  Topctop 20698  TopOnctopon 20715  clsccl 20822  ⇝_𝑡clm 21030  1^st𝜔c1stc 21240

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cc 9257  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-n0 11293  df-z 11378  df-uz 11688  df-fz 12327  df-top 20699  df-topon 20716  df-cld 20823  df-ntr 20824  df-cls 20825  df-lm 21033  df-1stc 21242

This theorem is referenced by:  1stccnp  21265  hausmapdom  21303  1stckgen  21357  metelcls  23103