Theorem 1stcelcls 22612

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 10191. 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 764	. . . . 5 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝐽 ∈ 1stω)
2		1stctop 22594	. . . . . . 7 ⊢ (𝐽 ∈ 1stω → 𝐽 ∈ Top)
3		1stcelcls.1	. . . . . . . 8 ⊢ 𝑋 = ∪ 𝐽
4	3	clsss3 22210	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋)
5	2, 4	sylan 580	. . . . . 6 ⊢ ((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋)
6	5	sselda 3921	. . . . 5 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑃 ∈ 𝑋)
7	3	1stcfb 22596	. . . . 5 ⊢ ((𝐽 ∈ 1stω ∧ 𝑃 ∈ 𝑋) → ∃𝑔(𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥)))
8	1, 6, 7	syl2anc 584	. . . 4 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → ∃𝑔(𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥)))
9		simpr2 1194	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)))
10		simpl 483	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) → 𝑃 ∈ (𝑔‘𝑘))
11	10	ralimi 3087	. . . . . . . . . . . 12 ⊢ (∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) → ∀𝑘 ∈ ℕ 𝑃 ∈ (𝑔‘𝑘))
12	9, 11	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∀𝑘 ∈ ℕ 𝑃 ∈ (𝑔‘𝑘))
13		fveq2 6774	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → (𝑔‘𝑘) = (𝑔‘𝑛))
14	13	eleq2d 2824	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → (𝑃 ∈ (𝑔‘𝑘) ↔ 𝑃 ∈ (𝑔‘𝑛)))
15	14	rspccva 3560	. . . . . . . . . . 11 ⊢ ((∀𝑘 ∈ ℕ 𝑃 ∈ (𝑔‘𝑘) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ (𝑔‘𝑛))
16	12, 15	sylan 580	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ (𝑔‘𝑛))
17		eleq2 2827	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑔‘𝑛) → (𝑃 ∈ 𝑦 ↔ 𝑃 ∈ (𝑔‘𝑛)))
18		ineq1 4139	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑔‘𝑛) → (𝑦 ∩ 𝑆) = ((𝑔‘𝑛) ∩ 𝑆))
19	18	neeq1d 3003	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑔‘𝑛) → ((𝑦 ∩ 𝑆) ≠ ∅ ↔ ((𝑔‘𝑛) ∩ 𝑆) ≠ ∅))
20	17, 19	imbi12d 345	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑔‘𝑛) → ((𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅) ↔ (𝑃 ∈ (𝑔‘𝑛) → ((𝑔‘𝑛) ∩ 𝑆) ≠ ∅)))
21	3	elcls2 22225	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅))))
22	2, 21	sylan 580	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅))))
23	22	simplbda 500	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅))
24	23	ad2antrr 723	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅))
25		simpr1 1193	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → 𝑔:ℕ⟶𝐽)
26	25	ffvelrnda 6961	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → (𝑔‘𝑛) ∈ 𝐽)
27	20, 24, 26	rspcdva 3562	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → (𝑃 ∈ (𝑔‘𝑛) → ((𝑔‘𝑛) ∩ 𝑆) ≠ ∅))
28	16, 27	mpd 15	. . . . . . . . 9 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ((𝑔‘𝑛) ∩ 𝑆) ≠ ∅)
29		elin 3903	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((𝑔‘𝑛) ∩ 𝑆) ↔ (𝑥 ∈ (𝑔‘𝑛) ∧ 𝑥 ∈ 𝑆))
30	29	biancomi 463	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ((𝑔‘𝑛) ∩ 𝑆) ↔ (𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑔‘𝑛)))
31	30	exbii 1850	. . . . . . . . . 10 ⊢ (∃𝑥 𝑥 ∈ ((𝑔‘𝑛) ∩ 𝑆) ↔ ∃𝑥(𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑔‘𝑛)))
32		n0 4280	. . . . . . . . . 10 ⊢ (((𝑔‘𝑛) ∩ 𝑆) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ ((𝑔‘𝑛) ∩ 𝑆))
33		df-rex 3070	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝑆 𝑥 ∈ (𝑔‘𝑛) ↔ ∃𝑥(𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑔‘𝑛)))
34	31, 32, 33	3bitr4i 303	. . . . . . . . 9 ⊢ (((𝑔‘𝑛) ∩ 𝑆) ≠ ∅ ↔ ∃𝑥 ∈ 𝑆 𝑥 ∈ (𝑔‘𝑛))
35	28, 34	sylib 217	. . . . . . . 8 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ∃𝑥 ∈ 𝑆 𝑥 ∈ (𝑔‘𝑛))
36	2	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝐽 ∈ Top)
37	3	topopn 22055	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
38	36, 37	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑋 ∈ 𝐽)
39		simplr 766	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ⊆ 𝑋)
40	38, 39	ssexd 5248	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ∈ V)
41		fvi 6844	. . . . . . . . . . 11 ⊢ (𝑆 ∈ V → ( I ‘𝑆) = 𝑆)
42	40, 41	syl 17	. . . . . . . . . 10 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → ( I ‘𝑆) = 𝑆)
43	42	ad2antrr 723	. . . . . . . . 9 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ( I ‘𝑆) = 𝑆)
44	43	rexeqdv 3349	. . . . . . . 8 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → (∃𝑥 ∈ ( I ‘𝑆)𝑥 ∈ (𝑔‘𝑛) ↔ ∃𝑥 ∈ 𝑆 𝑥 ∈ (𝑔‘𝑛)))
45	35, 44	mpbird 256	. . . . . . 7 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ∃𝑥 ∈ ( I ‘𝑆)𝑥 ∈ (𝑔‘𝑛))
46	45	ralrimiva 3103	. . . . . 6 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∀𝑛 ∈ ℕ ∃𝑥 ∈ ( I ‘𝑆)𝑥 ∈ (𝑔‘𝑛))
47		fvex 6787	. . . . . . 7 ⊢ ( I ‘𝑆) ∈ V
48		nnenom 13700	. . . . . . 7 ⊢ ℕ ≈ ω
49		eleq1 2826	. . . . . . 7 ⊢ (𝑥 = (𝑓‘𝑛) → (𝑥 ∈ (𝑔‘𝑛) ↔ (𝑓‘𝑛) ∈ (𝑔‘𝑛)))
50	47, 48, 49	axcc4 10195	. . . . . 6 ⊢ (∀𝑛 ∈ ℕ ∃𝑥 ∈ ( I ‘𝑆)𝑥 ∈ (𝑔‘𝑛) → ∃𝑓(𝑓:ℕ⟶( I ‘𝑆) ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)))
51	46, 50	syl 17	. . . . 5 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∃𝑓(𝑓:ℕ⟶( I ‘𝑆) ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)))
52	42	feq3d 6587	. . . . . . . . 9 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → (𝑓:ℕ⟶( I ‘𝑆) ↔ 𝑓:ℕ⟶𝑆))
53	52	biimpd 228	. . . . . . . 8 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → (𝑓:ℕ⟶( I ‘𝑆) → 𝑓:ℕ⟶𝑆))
54	53	adantr 481	. . . . . . 7 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → (𝑓:ℕ⟶( I ‘𝑆) → 𝑓:ℕ⟶𝑆))
55	6	ad2antrr 723	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝑃 ∈ 𝑋)
56		simplr3 1216	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))
57		eleq2 2827	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑃 ∈ 𝑥 ↔ 𝑃 ∈ 𝑦))
58		fveq2 6774	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → (𝑔‘𝑘) = (𝑔‘𝑗))
59	58	sseq1d 3952	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑗 → ((𝑔‘𝑘) ⊆ 𝑥 ↔ (𝑔‘𝑗) ⊆ 𝑥))
60	59	cbvrexvw 3384	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥 ↔ ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑥)
61		sseq2 3947	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → ((𝑔‘𝑗) ⊆ 𝑥 ↔ (𝑔‘𝑗) ⊆ 𝑦))
62	61	rexbidv 3226	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑥 ↔ ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦))
63	60, 62	bitrid 282	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥 ↔ ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦))
64	57, 63	imbi12d 345	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥) ↔ (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦)))
65	64	rspccva 3560	. . . . . . . . . . . . 13 ⊢ ((∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥) ∧ 𝑦 ∈ 𝐽) → (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦))
66	56, 65	sylan 580	. . . . . . . . . . . 12 ⊢ ((((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ 𝑦 ∈ 𝐽) → (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦))
67		simpr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) → (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘))
68	67	ralimi 3087	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘))
69	9, 68	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘))
70	69	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘))
71		simprrr 779	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → 𝑗 ∈ ℕ)
72		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑗 → (𝑔‘𝑛) = (𝑔‘𝑗))
73	72	sseq1d 3952	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑗 → ((𝑔‘𝑛) ⊆ (𝑔‘𝑗) ↔ (𝑔‘𝑗) ⊆ (𝑔‘𝑗)))
74	73	imbi2d 341	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑗 → (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑛) ⊆ (𝑔‘𝑗)) ↔ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑗) ⊆ (𝑔‘𝑗))))
75		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑚 → (𝑔‘𝑛) = (𝑔‘𝑚))
76	75	sseq1d 3952	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑚 → ((𝑔‘𝑛) ⊆ (𝑔‘𝑗) ↔ (𝑔‘𝑚) ⊆ (𝑔‘𝑗)))
77	76	imbi2d 341	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑚 → (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑛) ⊆ (𝑔‘𝑗)) ↔ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑚) ⊆ (𝑔‘𝑗))))
78		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = (𝑚 + 1) → (𝑔‘𝑛) = (𝑔‘(𝑚 + 1)))
79	78	sseq1d 3952	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = (𝑚 + 1) → ((𝑔‘𝑛) ⊆ (𝑔‘𝑗) ↔ (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑗)))
80	79	imbi2d 341	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = (𝑚 + 1) → (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑛) ⊆ (𝑔‘𝑗)) ↔ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑗))))
81		ssid 3943	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔‘𝑗) ⊆ (𝑔‘𝑗)
82	81	2a1i 12	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ ℤ → ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑗) ⊆ (𝑔‘𝑗)))
83		eluznn 12658	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ ℕ ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → 𝑚 ∈ ℕ)
84		fvoveq1 7298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝑚 → (𝑔‘(𝑘 + 1)) = (𝑔‘(𝑚 + 1)))
85		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝑚 → (𝑔‘𝑘) = (𝑔‘𝑚))
86	84, 85	sseq12d 3954	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 𝑚 → ((𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ↔ (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑚)))
87	86	rspccva 3560	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑚 ∈ ℕ) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑚))
88	83, 87	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ (𝑗 ∈ ℕ ∧ 𝑚 ∈ (ℤ≥‘𝑗))) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑚))
89	88	anassrs 468	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑚))
90		sstr2 3928	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑚) → ((𝑔‘𝑚) ⊆ (𝑔‘𝑗) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑗)))
91	89, 90	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → ((𝑔‘𝑚) ⊆ (𝑔‘𝑗) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑗)))
92	91	expcom 414	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ (ℤ≥‘𝑗) → ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → ((𝑔‘𝑚) ⊆ (𝑔‘𝑗) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑗))))
93	92	a2d 29	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ (ℤ≥‘𝑗) → (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑚) ⊆ (𝑔‘𝑗)) → ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑗))))
94	74, 77, 80, 77, 82, 93	uzind4 12646	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ (ℤ≥‘𝑗) → ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑚) ⊆ (𝑔‘𝑗)))
95	94	com12 32	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑚 ∈ (ℤ≥‘𝑗) → (𝑔‘𝑚) ⊆ (𝑔‘𝑗)))
96	95	ralrimiv 3102	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑔‘𝑚) ⊆ (𝑔‘𝑗))
97	70, 71, 96	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑔‘𝑚) ⊆ (𝑔‘𝑗))
98		fveq2 6774	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑚 → (𝑓‘𝑛) = (𝑓‘𝑚))
99	98, 75	eleq12d 2833	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑚 → ((𝑓‘𝑛) ∈ (𝑔‘𝑛) ↔ (𝑓‘𝑚) ∈ (𝑔‘𝑚)))
100		simplr 766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ)) → ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))
101	100	ad2antlr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))
102	71, 83	sylan 580	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → 𝑚 ∈ ℕ)
103	99, 101, 102	rspcdva 3562	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (𝑓‘𝑚) ∈ (𝑔‘𝑚))
104	103	ralrimiva 3103	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ (𝑔‘𝑚))
105		r19.26 3095	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑚 ∈ (ℤ≥‘𝑗)((𝑔‘𝑚) ⊆ (𝑔‘𝑗) ∧ (𝑓‘𝑚) ∈ (𝑔‘𝑚)) ↔ (∀𝑚 ∈ (ℤ≥‘𝑗)(𝑔‘𝑚) ⊆ (𝑔‘𝑗) ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ (𝑔‘𝑚)))
106	97, 104, 105	sylanbrc 583	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ∀𝑚 ∈ (ℤ≥‘𝑗)((𝑔‘𝑚) ⊆ (𝑔‘𝑗) ∧ (𝑓‘𝑚) ∈ (𝑔‘𝑚)))
107		ssel2 3916	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑔‘𝑚) ⊆ (𝑔‘𝑗) ∧ (𝑓‘𝑚) ∈ (𝑔‘𝑚)) → (𝑓‘𝑚) ∈ (𝑔‘𝑗))
108	107	ralimi 3087	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑚 ∈ (ℤ≥‘𝑗)((𝑔‘𝑚) ⊆ (𝑔‘𝑗) ∧ (𝑓‘𝑚) ∈ (𝑔‘𝑚)) → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ (𝑔‘𝑗))
109	106, 108	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ (𝑔‘𝑗))
110		ssel 3914	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔‘𝑗) ⊆ 𝑦 → ((𝑓‘𝑚) ∈ (𝑔‘𝑗) → (𝑓‘𝑚) ∈ 𝑦))
111	110	ralimdv 3109	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔‘𝑗) ⊆ 𝑦 → (∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ (𝑔‘𝑗) → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))
112	109, 111	syl5com 31	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ((𝑔‘𝑗) ⊆ 𝑦 → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))
113	112	anassrs 468	. . . . . . . . . . . . . 14 ⊢ ((((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ)) → ((𝑔‘𝑗) ⊆ 𝑦 → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))
114	113	anassrs 468	. . . . . . . . . . . . 13 ⊢ (((((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ 𝑦 ∈ 𝐽) ∧ 𝑗 ∈ ℕ) → ((𝑔‘𝑗) ⊆ 𝑦 → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))
115	114	reximdva 3203	. . . . . . . . . . . 12 ⊢ ((((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ 𝑦 ∈ 𝐽) → (∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦 → ∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))
116	66, 115	syld 47	. . . . . . . . . . 11 ⊢ ((((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ 𝑦 ∈ 𝐽) → (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))
117	116	ralrimiva 3103	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))
118	36	ad2antrr 723	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝐽 ∈ Top)
119	3	toptopon 22066	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
120	118, 119	sylib 217	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝐽 ∈ (TopOn‘𝑋))
121		nnuz 12621	. . . . . . . . . . 11 ⊢ ℕ = (ℤ≥‘1)
122		1zzd 12351	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 1 ∈ ℤ)
123		simprl 768	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝑓:ℕ⟶𝑆)
124	39	ad2antrr 723	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝑆 ⊆ 𝑋)
125	123, 124	fssd 6618	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝑓:ℕ⟶𝑋)
126		eqidd 2739	. . . . . . . . . . 11 ⊢ ((((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ 𝑚 ∈ ℕ) → (𝑓‘𝑚) = (𝑓‘𝑚))
127	120, 121, 122, 125, 126	lmbrf 22411	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → (𝑓(⇝𝑡‘𝐽)𝑃 ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦))))
128	55, 117, 127	mpbir2and 710	. . . . . . . . 9 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝑓(⇝𝑡‘𝐽)𝑃)
129	128	expr 457	. . . . . . . 8 ⊢ (((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑓:ℕ⟶𝑆) → (∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛) → 𝑓(⇝𝑡‘𝐽)𝑃))
130	129	imdistanda 572	. . . . . . 7 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) → (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)))
131	54, 130	syland 603	. . . . . 6 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ((𝑓:ℕ⟶( I ‘𝑆) ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) → (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)))
132	131	eximdv 1920	. . . . 5 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → (∃𝑓(𝑓:ℕ⟶( I ‘𝑆) ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) → ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)))
133	51, 132	mpd 15	. . . 4 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃))
134	8, 133	exlimddv 1938	. . 3 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃))
135	134	ex 413	. 2 ⊢ ((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) → ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)))
136	2	ad2antrr 723	. . . . . 6 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝐽 ∈ Top)
137	136, 119	sylib 217	. . . . 5 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝐽 ∈ (TopOn‘𝑋))
138		1zzd 12351	. . . . 5 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 1 ∈ ℤ)
139		simprr 770	. . . . 5 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝑓(⇝𝑡‘𝐽)𝑃)
140		simprl 768	. . . . . 6 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝑓:ℕ⟶𝑆)
141	140	ffvelrnda 6961	. . . . 5 ⊢ ((((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) ∈ 𝑆)
142		simplr 766	. . . . 5 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝑆 ⊆ 𝑋)
143	121, 137, 138, 139, 141, 142	lmcls 22453	. . . 4 ⊢ (((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝑃 ∈ ((cls‘𝐽)‘𝑆))
144	143	ex 413	. . 3 ⊢ ((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) → ((𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → 𝑃 ∈ ((cls‘𝐽)‘𝑆)))
145	144	exlimdv 1936	. 2 ⊢ ((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) → (∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → 𝑃 ∈ ((cls‘𝐽)‘𝑆)))
146	135, 145	impbid 211	1 ⊢ ((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086   = wceq 1539  ∃wex 1782   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3065  Vcvv 3432   ∩ cin 3886   ⊆ wss 3887  ∅c0 4256  ∪ cuni 4839   class class class wbr 5074   I cid 5488  ⟶wf 6429  ‘cfv 6433  (class class class)co 7275  1c1 10872   + caddc 10874  ℕcn 11973  ℤcz 12319  ℤ_≥cuz 12582  Topctop 22042  TopOnctopon 22059  clsccl 22169  ⇝_𝑡clm 22377  1^stωc1stc 22588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-inf2 9399  ax-cc 10191  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-iin 4927  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-1st 7831  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-er 8498  df-pm 8618  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-nn 11974  df-n0 12234  df-z 12320  df-uz 12583  df-fz 13240  df-top 22043  df-topon 22060  df-cld 22170  df-ntr 22171  df-cls 22172  df-lm 22380  df-1stc 22590

This theorem is referenced by:  1stccnp  22613  hausmapdom  22651  1stckgen  22705  metelcls  24469