Theorem 1stcelcls 23485

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 10473. 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 767	. . . . 5 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝐽 ∈ 1stω)
2		1stctop 23467	. . . . . . 7 ⊢ (𝐽 ∈ 1stω → 𝐽 ∈ Top)
3		1stcelcls.1	. . . . . . . 8 ⊢ 𝑋 = ∪ 𝐽
4	3	clsss3 23083	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋)
5	2, 4	sylan 580	. . . . . 6 ⊢ ((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋)
6	5	sselda 3995	. . . . 5 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑃 ∈ 𝑋)
7	3	1stcfb 23469	. . . . 5 ⊢ ((𝐽 ∈ 1stω ∧ 𝑃 ∈ 𝑋) → ∃𝑔(𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥)))
8	1, 6, 7	syl2anc 584	. . . 4 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → ∃𝑔(𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥)))
9		simpr2 1194	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)))
10		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) → 𝑃 ∈ (𝑔‘𝑘))
11	10	ralimi 3081	. . . . . . . . . . . 12 ⊢ (∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) → ∀𝑘 ∈ ℕ 𝑃 ∈ (𝑔‘𝑘))
12	9, 11	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∀𝑘 ∈ ℕ 𝑃 ∈ (𝑔‘𝑘))
13		fveq2 6907	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → (𝑔‘𝑘) = (𝑔‘𝑛))
14	13	eleq2d 2825	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → (𝑃 ∈ (𝑔‘𝑘) ↔ 𝑃 ∈ (𝑔‘𝑛)))
15	14	rspccva 3621	. . . . . . . . . . 11 ⊢ ((∀𝑘 ∈ ℕ 𝑃 ∈ (𝑔‘𝑘) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ (𝑔‘𝑛))
16	12, 15	sylan 580	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ (𝑔‘𝑛))
17		eleq2 2828	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑔‘𝑛) → (𝑃 ∈ 𝑦 ↔ 𝑃 ∈ (𝑔‘𝑛)))
18		ineq1 4221	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑔‘𝑛) → (𝑦 ∩ 𝑆) = ((𝑔‘𝑛) ∩ 𝑆))
19	18	neeq1d 2998	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑔‘𝑛) → ((𝑦 ∩ 𝑆) ≠ ∅ ↔ ((𝑔‘𝑛) ∩ 𝑆) ≠ ∅))
20	17, 19	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑔‘𝑛) → ((𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅) ↔ (𝑃 ∈ (𝑔‘𝑛) → ((𝑔‘𝑛) ∩ 𝑆) ≠ ∅)))
21	3	elcls2 23098	. . . . . . . . . . . . . 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 1193	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → 𝑔:ℕ⟶𝐽)
26	25	ffvelcdmda 7104	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → (𝑔‘𝑛) ∈ 𝐽)
27	20, 24, 26	rspcdva 3623	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → (𝑃 ∈ (𝑔‘𝑛) → ((𝑔‘𝑛) ∩ 𝑆) ≠ ∅))
28	16, 27	mpd 15	. . . . . . . . 9 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ((𝑔‘𝑛) ∩ 𝑆) ≠ ∅)
29		elin 3979	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((𝑔‘𝑛) ∩ 𝑆) ↔ (𝑥 ∈ (𝑔‘𝑛) ∧ 𝑥 ∈ 𝑆))
30	29	biancomi 462	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ((𝑔‘𝑛) ∩ 𝑆) ↔ (𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑔‘𝑛)))
31	30	exbii 1845	. . . . . . . . . 10 ⊢ (∃𝑥 𝑥 ∈ ((𝑔‘𝑛) ∩ 𝑆) ↔ ∃𝑥(𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑔‘𝑛)))
32		n0 4359	. . . . . . . . . 10 ⊢ (((𝑔‘𝑛) ∩ 𝑆) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ ((𝑔‘𝑛) ∩ 𝑆))
33		df-rex 3069	. . . . . . . . . 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 22928	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
38	36, 37	syl 17	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑋 ∈ 𝐽)
39		simplr 769	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ⊆ 𝑋)
40	38, 39	ssexd 5330	. . . . . . . . . 10 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ∈ V)
41		fvi 6985	. . . . . . . . . 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 3329	. . . . . . 7 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ∃𝑥 ∈ ( I ‘𝑆)𝑥 ∈ (𝑔‘𝑛))
45	44	ralrimiva 3144	. . . . . 6 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∀𝑛 ∈ ℕ ∃𝑥 ∈ ( I ‘𝑆)𝑥 ∈ (𝑔‘𝑛))
46		fvex 6920	. . . . . . 7 ⊢ ( I ‘𝑆) ∈ V
47		nnenom 14018	. . . . . . 7 ⊢ ℕ ≈ ω
48		eleq1 2827	. . . . . . 7 ⊢ (𝑥 = (𝑓‘𝑛) → (𝑥 ∈ (𝑔‘𝑛) ↔ (𝑓‘𝑛) ∈ (𝑔‘𝑛)))
49	46, 47, 48	axcc4 10477	. . . . . 6 ⊢ (∀𝑛 ∈ ℕ ∃𝑥 ∈ ( I ‘𝑆)𝑥 ∈ (𝑔‘𝑛) → ∃𝑓(𝑓:ℕ⟶( I ‘𝑆) ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)))
50	45, 49	syl 17	. . . . 5 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∃𝑓(𝑓:ℕ⟶( I ‘𝑆) ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)))
51	42	feq3d 6724	. . . . . . . . 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 1216	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))
56		eleq2 2828	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑃 ∈ 𝑥 ↔ 𝑃 ∈ 𝑦))
57		fveq2 6907	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → (𝑔‘𝑘) = (𝑔‘𝑗))
58	57	sseq1d 4027	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑗 → ((𝑔‘𝑘) ⊆ 𝑥 ↔ (𝑔‘𝑗) ⊆ 𝑥))
59	58	cbvrexvw 3236	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥 ↔ ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑥)
60		sseq2 4022	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → ((𝑔‘𝑗) ⊆ 𝑥 ↔ (𝑔‘𝑗) ⊆ 𝑦))
61	60	rexbidv 3177	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑥 ↔ ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦))
62	59, 61	bitrid 283	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥 ↔ ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦))
63	56, 62	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥) ↔ (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦)))
64	63	rspccva 3621	. . . . . . . . . . . . 13 ⊢ ((∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥) ∧ 𝑦 ∈ 𝐽) → (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦))
65	55, 64	sylan 580	. . . . . . . . . . . 12 ⊢ ((((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ 𝑦 ∈ 𝐽) → (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦))
66		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) → (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘))
67	66	ralimi 3081	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘))
68	9, 67	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘))
69	68	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘))
70		simprrr 782	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → 𝑗 ∈ ℕ)
71		fveq2 6907	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑗 → (𝑔‘𝑛) = (𝑔‘𝑗))
72	71	sseq1d 4027	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑗 → ((𝑔‘𝑛) ⊆ (𝑔‘𝑗) ↔ (𝑔‘𝑗) ⊆ (𝑔‘𝑗)))
73	72	imbi2d 340	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑗 → (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑛) ⊆ (𝑔‘𝑗)) ↔ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑗) ⊆ (𝑔‘𝑗))))
74		fveq2 6907	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑚 → (𝑔‘𝑛) = (𝑔‘𝑚))
75	74	sseq1d 4027	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑚 → ((𝑔‘𝑛) ⊆ (𝑔‘𝑗) ↔ (𝑔‘𝑚) ⊆ (𝑔‘𝑗)))
76	75	imbi2d 340	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑚 → (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑛) ⊆ (𝑔‘𝑗)) ↔ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑚) ⊆ (𝑔‘𝑗))))
77		fveq2 6907	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = (𝑚 + 1) → (𝑔‘𝑛) = (𝑔‘(𝑚 + 1)))
78	77	sseq1d 4027	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = (𝑚 + 1) → ((𝑔‘𝑛) ⊆ (𝑔‘𝑗) ↔ (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑗)))
79	78	imbi2d 340	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = (𝑚 + 1) → (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑛) ⊆ (𝑔‘𝑗)) ↔ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑗))))
80		ssid 4018	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔‘𝑗) ⊆ (𝑔‘𝑗)
81	80	2a1i 12	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ ℤ → ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑗) ⊆ (𝑔‘𝑗)))
82		eluznn 12958	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ ℕ ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → 𝑚 ∈ ℕ)
83		fvoveq1 7454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝑚 → (𝑔‘(𝑘 + 1)) = (𝑔‘(𝑚 + 1)))
84		fveq2 6907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝑚 → (𝑔‘𝑘) = (𝑔‘𝑚))
85	83, 84	sseq12d 4029	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 𝑚 → ((𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ↔ (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑚)))
86	85	rspccva 3621	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑚 ∈ ℕ) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑚))
87	82, 86	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ (𝑗 ∈ ℕ ∧ 𝑚 ∈ (ℤ≥‘𝑗))) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑚))
88	87	anassrs 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑚))
89		sstr2 4002	. . . . . . . . . . . . . . . . . . . . . . . . 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 12946	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ (ℤ≥‘𝑗) → ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑚) ⊆ (𝑔‘𝑗)))
94	93	com12 32	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑚 ∈ (ℤ≥‘𝑗) → (𝑔‘𝑚) ⊆ (𝑔‘𝑗)))
95	94	ralrimiv 3143	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑔‘𝑚) ⊆ (𝑔‘𝑗))
96	69, 70, 95	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑔‘𝑚) ⊆ (𝑔‘𝑗))
97		fveq2 6907	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑚 → (𝑓‘𝑛) = (𝑓‘𝑚))
98	97, 74	eleq12d 2833	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑚 → ((𝑓‘𝑛) ∈ (𝑔‘𝑛) ↔ (𝑓‘𝑚) ∈ (𝑔‘𝑚)))
99		simplr 769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ)) → ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))
100	99	ad2antlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))
101	70, 82	sylan 580	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → 𝑚 ∈ ℕ)
102	98, 100, 101	rspcdva 3623	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (𝑓‘𝑚) ∈ (𝑔‘𝑚))
103	102	ralrimiva 3144	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ (𝑔‘𝑚))
104		r19.26 3109	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑚 ∈ (ℤ≥‘𝑗)((𝑔‘𝑚) ⊆ (𝑔‘𝑗) ∧ (𝑓‘𝑚) ∈ (𝑔‘𝑚)) ↔ (∀𝑚 ∈ (ℤ≥‘𝑗)(𝑔‘𝑚) ⊆ (𝑔‘𝑗) ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ (𝑔‘𝑚)))
105	96, 103, 104	sylanbrc 583	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ∀𝑚 ∈ (ℤ≥‘𝑗)((𝑔‘𝑚) ⊆ (𝑔‘𝑗) ∧ (𝑓‘𝑚) ∈ (𝑔‘𝑚)))
106		ssel2 3990	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑔‘𝑚) ⊆ (𝑔‘𝑗) ∧ (𝑓‘𝑚) ∈ (𝑔‘𝑚)) → (𝑓‘𝑚) ∈ (𝑔‘𝑗))
107	106	ralimi 3081	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑚 ∈ (ℤ≥‘𝑗)((𝑔‘𝑚) ⊆ (𝑔‘𝑗) ∧ (𝑓‘𝑚) ∈ (𝑔‘𝑚)) → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ (𝑔‘𝑗))
108	105, 107	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ (𝑔‘𝑗))
109		ssel 3989	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔‘𝑗) ⊆ 𝑦 → ((𝑓‘𝑚) ∈ (𝑔‘𝑗) → (𝑓‘𝑚) ∈ 𝑦))
110	109	ralimdv 3167	. . . . . . . . . . . . . . . 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 3166	. . . . . . . . . . . 12 ⊢ ((((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ 𝑦 ∈ 𝐽) → (∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦 → ∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))
115	65, 114	syld 47	. . . . . . . . . . 11 ⊢ ((((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ 𝑦 ∈ 𝐽) → (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))
116	115	ralrimiva 3144	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))
117	36	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝐽 ∈ Top)
118	3	toptopon 22939	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
119	117, 118	sylib 218	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝐽 ∈ (TopOn‘𝑋))
120		nnuz 12919	. . . . . . . . . . 11 ⊢ ℕ = (ℤ≥‘1)
121		1zzd 12646	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 1 ∈ ℤ)
122		simprl 771	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝑓:ℕ⟶𝑆)
123	39	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝑆 ⊆ 𝑋)
124	122, 123	fssd 6754	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝑓:ℕ⟶𝑋)
125		eqidd 2736	. . . . . . . . . . 11 ⊢ ((((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ 𝑚 ∈ ℕ) → (𝑓‘𝑚) = (𝑓‘𝑚))
126	119, 120, 121, 124, 125	lmbrf 23284	. . . . . . . . . 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 1915	. . . . 5 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → (∃𝑓(𝑓:ℕ⟶( I ‘𝑆) ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) → ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)))
132	50, 131	mpd 15	. . . 4 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃))
133	8, 132	exlimddv 1933	. . 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 12646	. . . . 5 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 1 ∈ ℤ)
138		simprr 773	. . . . 5 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝑓(⇝𝑡‘𝐽)𝑃)
139		simprl 771	. . . . . 6 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝑓:ℕ⟶𝑆)
140	139	ffvelcdmda 7104	. . . . 5 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) ∈ 𝑆)
141		simplr 769	. . . . 5 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝑆 ⊆ 𝑋)
142	120, 136, 137, 138, 140, 141	lmcls 23326	. . . 4 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝑃 ∈ ((cls‘𝐽)‘𝑆))
143	142	ex 412	. . 3 ⊢ ((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) → ((𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → 𝑃 ∈ ((cls‘𝐽)‘𝑆)))
144	143	exlimdv 1931	. 2 ⊢ ((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) → (∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → 𝑃 ∈ ((cls‘𝐽)‘𝑆)))
145	134, 144	impbid 212	1 ⊢ ((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1537  ∃wex 1776   ∈ wcel 2106   ≠ wne 2938  ∀wral 3059  ∃wrex 3068  Vcvv 3478   ∩ cin 3962   ⊆ wss 3963  ∅c0 4339  ∪ cuni 4912   class class class wbr 5148   I cid 5582  ⟶wf 6559  ‘cfv 6563  (class class class)co 7431  1c1 11154   + caddc 11156  ℕcn 12264  ℤcz 12611  ℤ_≥cuz 12876  Topctop 22915  TopOnctopon 22932  clsccl 23042  ⇝_𝑡clm 23250  1^stωc1stc 23461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-inf2 9679  ax-cc 10473  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-2o 8506  df-er 8744  df-pm 8868  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-nn 12265  df-n0 12525  df-z 12612  df-uz 12877  df-fz 13545  df-top 22916  df-topon 22933  df-cld 23043  df-ntr 23044  df-cls 23045  df-lm 23253  df-1stc 23463

This theorem is referenced by:  1stccnp  23486  hausmapdom  23524  1stckgen  23578  metelcls  25353