Theorem 1stcelcls 23470

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 10476. 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 766	. . . . 5 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝐽 ∈ 1stω)
2		1stctop 23452	. . . . . . 7 ⊢ (𝐽 ∈ 1stω → 𝐽 ∈ Top)
3		1stcelcls.1	. . . . . . . 8 ⊢ 𝑋 = ∪ 𝐽
4	3	clsss3 23068	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋)
5	2, 4	sylan 580	. . . . . 6 ⊢ ((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋)
6	5	sselda 3982	. . . . 5 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑃 ∈ 𝑋)
7	3	1stcfb 23454	. . . . 5 ⊢ ((𝐽 ∈ 1stω ∧ 𝑃 ∈ 𝑋) → ∃𝑔(𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥)))
8	1, 6, 7	syl2anc 584	. . . 4 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → ∃𝑔(𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥)))
9		simpr2 1195	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)))
10		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) → 𝑃 ∈ (𝑔‘𝑘))
11	10	ralimi 3082	. . . . . . . . . . . 12 ⊢ (∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) → ∀𝑘 ∈ ℕ 𝑃 ∈ (𝑔‘𝑘))
12	9, 11	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∀𝑘 ∈ ℕ 𝑃 ∈ (𝑔‘𝑘))
13		fveq2 6905	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → (𝑔‘𝑘) = (𝑔‘𝑛))
14	13	eleq2d 2826	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → (𝑃 ∈ (𝑔‘𝑘) ↔ 𝑃 ∈ (𝑔‘𝑛)))
15	14	rspccva 3620	. . . . . . . . . . 11 ⊢ ((∀𝑘 ∈ ℕ 𝑃 ∈ (𝑔‘𝑘) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ (𝑔‘𝑛))
16	12, 15	sylan 580	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ (𝑔‘𝑛))
17		eleq2 2829	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑔‘𝑛) → (𝑃 ∈ 𝑦 ↔ 𝑃 ∈ (𝑔‘𝑛)))
18		ineq1 4212	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑔‘𝑛) → (𝑦 ∩ 𝑆) = ((𝑔‘𝑛) ∩ 𝑆))
19	18	neeq1d 2999	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑔‘𝑛) → ((𝑦 ∩ 𝑆) ≠ ∅ ↔ ((𝑔‘𝑛) ∩ 𝑆) ≠ ∅))
20	17, 19	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑔‘𝑛) → ((𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅) ↔ (𝑃 ∈ (𝑔‘𝑛) → ((𝑔‘𝑛) ∩ 𝑆) ≠ ∅)))
21	3	elcls2 23083	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅))))
22	2, 21	sylan 580	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅))))
23	22	simplbda 499	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅))
24	23	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅))
25		simpr1 1194	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → 𝑔:ℕ⟶𝐽)
26	25	ffvelcdmda 7103	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → (𝑔‘𝑛) ∈ 𝐽)
27	20, 24, 26	rspcdva 3622	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → (𝑃 ∈ (𝑔‘𝑛) → ((𝑔‘𝑛) ∩ 𝑆) ≠ ∅))
28	16, 27	mpd 15	. . . . . . . . 9 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ((𝑔‘𝑛) ∩ 𝑆) ≠ ∅)
29		elin 3966	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((𝑔‘𝑛) ∩ 𝑆) ↔ (𝑥 ∈ (𝑔‘𝑛) ∧ 𝑥 ∈ 𝑆))
30	29	biancomi 462	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ((𝑔‘𝑛) ∩ 𝑆) ↔ (𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑔‘𝑛)))
31	30	exbii 1847	. . . . . . . . . 10 ⊢ (∃𝑥 𝑥 ∈ ((𝑔‘𝑛) ∩ 𝑆) ↔ ∃𝑥(𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑔‘𝑛)))
32		n0 4352	. . . . . . . . . 10 ⊢ (((𝑔‘𝑛) ∩ 𝑆) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ ((𝑔‘𝑛) ∩ 𝑆))
33		df-rex 3070	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝑆 𝑥 ∈ (𝑔‘𝑛) ↔ ∃𝑥(𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑔‘𝑛)))
34	31, 32, 33	3bitr4i 303	. . . . . . . . 9 ⊢ (((𝑔‘𝑛) ∩ 𝑆) ≠ ∅ ↔ ∃𝑥 ∈ 𝑆 𝑥 ∈ (𝑔‘𝑛))
35	28, 34	sylib 218	. . . . . . . 8 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ∃𝑥 ∈ 𝑆 𝑥 ∈ (𝑔‘𝑛))
36	2	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝐽 ∈ Top)
37	3	topopn 22913	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
38	36, 37	syl 17	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑋 ∈ 𝐽)
39		simplr 768	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ⊆ 𝑋)
40	38, 39	ssexd 5323	. . . . . . . . . 10 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ∈ V)
41		fvi 6984	. . . . . . . . . 10 ⊢ (𝑆 ∈ V → ( I ‘𝑆) = 𝑆)
42	40, 41	syl 17	. . . . . . . . 9 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → ( I ‘𝑆) = 𝑆)
43	42	ad2antrr 726	. . . . . . . 8 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ( I ‘𝑆) = 𝑆)
44	35, 43	rexeqtrrdv 3330	. . . . . . 7 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ∃𝑥 ∈ ( I ‘𝑆)𝑥 ∈ (𝑔‘𝑛))
45	44	ralrimiva 3145	. . . . . 6 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∀𝑛 ∈ ℕ ∃𝑥 ∈ ( I ‘𝑆)𝑥 ∈ (𝑔‘𝑛))
46		fvex 6918	. . . . . . 7 ⊢ ( I ‘𝑆) ∈ V
47		nnenom 14022	. . . . . . 7 ⊢ ℕ ≈ ω
48		eleq1 2828	. . . . . . 7 ⊢ (𝑥 = (𝑓‘𝑛) → (𝑥 ∈ (𝑔‘𝑛) ↔ (𝑓‘𝑛) ∈ (𝑔‘𝑛)))
49	46, 47, 48	axcc4 10480	. . . . . 6 ⊢ (∀𝑛 ∈ ℕ ∃𝑥 ∈ ( I ‘𝑆)𝑥 ∈ (𝑔‘𝑛) → ∃𝑓(𝑓:ℕ⟶( I ‘𝑆) ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)))
50	45, 49	syl 17	. . . . 5 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∃𝑓(𝑓:ℕ⟶( I ‘𝑆) ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)))
51	42	feq3d 6722	. . . . . . . . 9 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → (𝑓:ℕ⟶( I ‘𝑆) ↔ 𝑓:ℕ⟶𝑆))
52	51	biimpd 229	. . . . . . . 8 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → (𝑓:ℕ⟶( I ‘𝑆) → 𝑓:ℕ⟶𝑆))
53	52	adantr 480	. . . . . . 7 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → (𝑓:ℕ⟶( I ‘𝑆) → 𝑓:ℕ⟶𝑆))
54	6	ad2antrr 726	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝑃 ∈ 𝑋)
55		simplr3 1217	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))
56		eleq2 2829	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑃 ∈ 𝑥 ↔ 𝑃 ∈ 𝑦))
57		fveq2 6905	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → (𝑔‘𝑘) = (𝑔‘𝑗))
58	57	sseq1d 4014	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑗 → ((𝑔‘𝑘) ⊆ 𝑥 ↔ (𝑔‘𝑗) ⊆ 𝑥))
59	58	cbvrexvw 3237	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥 ↔ ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑥)
60		sseq2 4009	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → ((𝑔‘𝑗) ⊆ 𝑥 ↔ (𝑔‘𝑗) ⊆ 𝑦))
61	60	rexbidv 3178	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑥 ↔ ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦))
62	59, 61	bitrid 283	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥 ↔ ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦))
63	56, 62	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥) ↔ (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦)))
64	63	rspccva 3620	. . . . . . . . . . . . 13 ⊢ ((∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥) ∧ 𝑦 ∈ 𝐽) → (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦))
65	55, 64	sylan 580	. . . . . . . . . . . 12 ⊢ ((((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ 𝑦 ∈ 𝐽) → (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦))
66		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) → (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘))
67	66	ralimi 3082	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘))
68	9, 67	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘))
69	68	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘))
70		simprrr 781	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → 𝑗 ∈ ℕ)
71		fveq2 6905	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑗 → (𝑔‘𝑛) = (𝑔‘𝑗))
72	71	sseq1d 4014	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑗 → ((𝑔‘𝑛) ⊆ (𝑔‘𝑗) ↔ (𝑔‘𝑗) ⊆ (𝑔‘𝑗)))
73	72	imbi2d 340	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑗 → (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑛) ⊆ (𝑔‘𝑗)) ↔ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑗) ⊆ (𝑔‘𝑗))))
74		fveq2 6905	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑚 → (𝑔‘𝑛) = (𝑔‘𝑚))
75	74	sseq1d 4014	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑚 → ((𝑔‘𝑛) ⊆ (𝑔‘𝑗) ↔ (𝑔‘𝑚) ⊆ (𝑔‘𝑗)))
76	75	imbi2d 340	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑚 → (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑛) ⊆ (𝑔‘𝑗)) ↔ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑚) ⊆ (𝑔‘𝑗))))
77		fveq2 6905	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = (𝑚 + 1) → (𝑔‘𝑛) = (𝑔‘(𝑚 + 1)))
78	77	sseq1d 4014	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = (𝑚 + 1) → ((𝑔‘𝑛) ⊆ (𝑔‘𝑗) ↔ (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑗)))
79	78	imbi2d 340	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = (𝑚 + 1) → (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑛) ⊆ (𝑔‘𝑗)) ↔ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑗))))
80		ssid 4005	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔‘𝑗) ⊆ (𝑔‘𝑗)
81	80	2a1i 12	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ ℤ → ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑗) ⊆ (𝑔‘𝑗)))
82		eluznn 12961	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ ℕ ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → 𝑚 ∈ ℕ)
83		fvoveq1 7455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝑚 → (𝑔‘(𝑘 + 1)) = (𝑔‘(𝑚 + 1)))
84		fveq2 6905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝑚 → (𝑔‘𝑘) = (𝑔‘𝑚))
85	83, 84	sseq12d 4016	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 𝑚 → ((𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ↔ (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑚)))
86	85	rspccva 3620	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑚 ∈ ℕ) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑚))
87	82, 86	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ (𝑗 ∈ ℕ ∧ 𝑚 ∈ (ℤ≥‘𝑗))) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑚))
88	87	anassrs 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑚))
89		sstr2 3989	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑚) → ((𝑔‘𝑚) ⊆ (𝑔‘𝑗) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑗)))
90	88, 89	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → ((𝑔‘𝑚) ⊆ (𝑔‘𝑗) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑗)))
91	90	expcom 413	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ (ℤ≥‘𝑗) → ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → ((𝑔‘𝑚) ⊆ (𝑔‘𝑗) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑗))))
92	91	a2d 29	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ (ℤ≥‘𝑗) → (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑚) ⊆ (𝑔‘𝑗)) → ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑗))))
93	73, 76, 79, 76, 81, 92	uzind4 12949	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ (ℤ≥‘𝑗) → ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑚) ⊆ (𝑔‘𝑗)))
94	93	com12 32	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑚 ∈ (ℤ≥‘𝑗) → (𝑔‘𝑚) ⊆ (𝑔‘𝑗)))
95	94	ralrimiv 3144	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑔‘𝑚) ⊆ (𝑔‘𝑗))
96	69, 70, 95	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑔‘𝑚) ⊆ (𝑔‘𝑗))
97		fveq2 6905	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑚 → (𝑓‘𝑛) = (𝑓‘𝑚))
98	97, 74	eleq12d 2834	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑚 → ((𝑓‘𝑛) ∈ (𝑔‘𝑛) ↔ (𝑓‘𝑚) ∈ (𝑔‘𝑚)))
99		simplr 768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ)) → ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))
100	99	ad2antlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))
101	70, 82	sylan 580	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → 𝑚 ∈ ℕ)
102	98, 100, 101	rspcdva 3622	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (𝑓‘𝑚) ∈ (𝑔‘𝑚))
103	102	ralrimiva 3145	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ (𝑔‘𝑚))
104		r19.26 3110	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑚 ∈ (ℤ≥‘𝑗)((𝑔‘𝑚) ⊆ (𝑔‘𝑗) ∧ (𝑓‘𝑚) ∈ (𝑔‘𝑚)) ↔ (∀𝑚 ∈ (ℤ≥‘𝑗)(𝑔‘𝑚) ⊆ (𝑔‘𝑗) ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ (𝑔‘𝑚)))
105	96, 103, 104	sylanbrc 583	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ∀𝑚 ∈ (ℤ≥‘𝑗)((𝑔‘𝑚) ⊆ (𝑔‘𝑗) ∧ (𝑓‘𝑚) ∈ (𝑔‘𝑚)))
106		ssel2 3977	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑔‘𝑚) ⊆ (𝑔‘𝑗) ∧ (𝑓‘𝑚) ∈ (𝑔‘𝑚)) → (𝑓‘𝑚) ∈ (𝑔‘𝑗))
107	106	ralimi 3082	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑚 ∈ (ℤ≥‘𝑗)((𝑔‘𝑚) ⊆ (𝑔‘𝑗) ∧ (𝑓‘𝑚) ∈ (𝑔‘𝑚)) → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ (𝑔‘𝑗))
108	105, 107	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ (𝑔‘𝑗))
109		ssel 3976	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔‘𝑗) ⊆ 𝑦 → ((𝑓‘𝑚) ∈ (𝑔‘𝑗) → (𝑓‘𝑚) ∈ 𝑦))
110	109	ralimdv 3168	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔‘𝑗) ⊆ 𝑦 → (∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ (𝑔‘𝑗) → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))
111	108, 110	syl5com 31	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ((𝑔‘𝑗) ⊆ 𝑦 → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))
112	111	anassrs 467	. . . . . . . . . . . . . 14 ⊢ ((((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ)) → ((𝑔‘𝑗) ⊆ 𝑦 → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))
113	112	anassrs 467	. . . . . . . . . . . . 13 ⊢ (((((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ 𝑦 ∈ 𝐽) ∧ 𝑗 ∈ ℕ) → ((𝑔‘𝑗) ⊆ 𝑦 → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))
114	113	reximdva 3167	. . . . . . . . . . . 12 ⊢ ((((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ 𝑦 ∈ 𝐽) → (∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦 → ∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))
115	65, 114	syld 47	. . . . . . . . . . 11 ⊢ ((((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ 𝑦 ∈ 𝐽) → (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))
116	115	ralrimiva 3145	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))
117	36	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝐽 ∈ Top)
118	3	toptopon 22924	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
119	117, 118	sylib 218	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝐽 ∈ (TopOn‘𝑋))
120		nnuz 12922	. . . . . . . . . . 11 ⊢ ℕ = (ℤ≥‘1)
121		1zzd 12650	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 1 ∈ ℤ)
122		simprl 770	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝑓:ℕ⟶𝑆)
123	39	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝑆 ⊆ 𝑋)
124	122, 123	fssd 6752	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝑓:ℕ⟶𝑋)
125		eqidd 2737	. . . . . . . . . . 11 ⊢ ((((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ 𝑚 ∈ ℕ) → (𝑓‘𝑚) = (𝑓‘𝑚))
126	119, 120, 121, 124, 125	lmbrf 23269	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → (𝑓(⇝𝑡‘𝐽)𝑃 ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))))
127	54, 116, 126	mpbir2and 713	. . . . . . . . 9 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝑓(⇝𝑡‘𝐽)𝑃)
128	127	expr 456	. . . . . . . 8 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑓:ℕ⟶𝑆) → (∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛) → 𝑓(⇝𝑡‘𝐽)𝑃))
129	128	imdistanda 571	. . . . . . 7 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) → (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)))
130	53, 129	syland 603	. . . . . 6 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ((𝑓:ℕ⟶( I ‘𝑆) ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) → (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)))
131	130	eximdv 1916	. . . . 5 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → (∃𝑓(𝑓:ℕ⟶( I ‘𝑆) ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) → ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)))
132	50, 131	mpd 15	. . . 4 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃))
133	8, 132	exlimddv 1934	. . 3 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃))
134	133	ex 412	. 2 ⊢ ((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) → ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)))
135	2	ad2antrr 726	. . . . . 6 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝐽 ∈ Top)
136	135, 118	sylib 218	. . . . 5 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝐽 ∈ (TopOn‘𝑋))
137		1zzd 12650	. . . . 5 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 1 ∈ ℤ)
138		simprr 772	. . . . 5 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝑓(⇝𝑡‘𝐽)𝑃)
139		simprl 770	. . . . . 6 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝑓:ℕ⟶𝑆)
140	139	ffvelcdmda 7103	. . . . 5 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) ∈ 𝑆)
141		simplr 768	. . . . 5 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝑆 ⊆ 𝑋)
142	120, 136, 137, 138, 140, 141	lmcls 23311	. . . 4 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝑃 ∈ ((cls‘𝐽)‘𝑆))
143	142	ex 412	. . 3 ⊢ ((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) → ((𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → 𝑃 ∈ ((cls‘𝐽)‘𝑆)))
144	143	exlimdv 1932	. 2 ⊢ ((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) → (∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → 𝑃 ∈ ((cls‘𝐽)‘𝑆)))
145	134, 144	impbid 212	1 ⊢ ((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1539  ∃wex 1778   ∈ wcel 2107   ≠ wne 2939  ∀wral 3060  ∃wrex 3069  Vcvv 3479   ∩ cin 3949   ⊆ wss 3950  ∅c0 4332  ∪ cuni 4906   class class class wbr 5142   I cid 5576  ⟶wf 6556  ‘cfv 6560  (class class class)co 7432  1c1 11157   + caddc 11159  ℕcn 12267  ℤcz 12615  ℤ_≥cuz 12879  Topctop 22900  TopOnctopon 22917  clsccl 23027  ⇝_𝑡clm 23235  1^stωc1stc 23446

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-inf2 9682  ax-cc 10476  ax-cnex 11212  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-mulcom 11220  ax-addass 11221  ax-mulass 11222  ax-distr 11223  ax-i2m1 11224  ax-1ne0 11225  ax-1rid 11226  ax-rnegex 11227  ax-rrecex 11228  ax-cnre 11229  ax-pre-lttri 11230  ax-pre-lttrn 11231  ax-pre-ltadd 11232  ax-pre-mulgt0 11233

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-int 4946  df-iun 4992  df-iin 4993  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-om 7889  df-1st 8015  df-2nd 8016  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-1o 8507  df-2o 8508  df-er 8746  df-pm 8870  df-en 8987  df-dom 8988  df-sdom 8989  df-fin 8990  df-pnf 11298  df-mnf 11299  df-xr 11300  df-ltxr 11301  df-le 11302  df-sub 11495  df-neg 11496  df-nn 12268  df-n0 12529  df-z 12616  df-uz 12880  df-fz 13549  df-top 22901  df-topon 22918  df-cld 23028  df-ntr 23029  df-cls 23030  df-lm 23238  df-1stc 23448

This theorem is referenced by:  1stccnp  23471  hausmapdom  23509  1stckgen  23563  metelcls  25340