Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  1stcelcls Structured version   Visualization version   GIF version

Theorem 1stcelcls 22073
 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 9848. 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.
StepHypRef Expression
1 simpll 766 . . . . 5 (((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝐽 ∈ 1stω)
2 1stctop 22055 . . . . . . 7 (𝐽 ∈ 1stω → 𝐽 ∈ Top)
3 1stcelcls.1 . . . . . . . 8 𝑋 = 𝐽
43clsss3 21671 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋)
52, 4sylan 583 . . . . . 6 ((𝐽 ∈ 1stω ∧ 𝑆𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋)
65sselda 3915 . . . . 5 (((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑃𝑋)
731stcfb 22057 . . . . 5 ((𝐽 ∈ 1stω ∧ 𝑃𝑋) → ∃𝑔(𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥)))
81, 6, 7syl2anc 587 . . . 4 (((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → ∃𝑔(𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥)))
9 simpr2 1192 . . . . . . . . . . . 12 ((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) → ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)))
10 simpl 486 . . . . . . . . . . . . 13 ((𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) → 𝑃 ∈ (𝑔𝑘))
1110ralimi 3128 . . . . . . . . . . . 12 (∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) → ∀𝑘 ∈ ℕ 𝑃 ∈ (𝑔𝑘))
129, 11syl 17 . . . . . . . . . . 11 ((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) → ∀𝑘 ∈ ℕ 𝑃 ∈ (𝑔𝑘))
13 fveq2 6645 . . . . . . . . . . . . 13 (𝑘 = 𝑛 → (𝑔𝑘) = (𝑔𝑛))
1413eleq2d 2875 . . . . . . . . . . . 12 (𝑘 = 𝑛 → (𝑃 ∈ (𝑔𝑘) ↔ 𝑃 ∈ (𝑔𝑛)))
1514rspccva 3570 . . . . . . . . . . 11 ((∀𝑘 ∈ ℕ 𝑃 ∈ (𝑔𝑘) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ (𝑔𝑛))
1612, 15sylan 583 . . . . . . . . . 10 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ (𝑔𝑛))
17 eleq2 2878 . . . . . . . . . . . 12 (𝑦 = (𝑔𝑛) → (𝑃𝑦𝑃 ∈ (𝑔𝑛)))
18 ineq1 4131 . . . . . . . . . . . . 13 (𝑦 = (𝑔𝑛) → (𝑦𝑆) = ((𝑔𝑛) ∩ 𝑆))
1918neeq1d 3046 . . . . . . . . . . . 12 (𝑦 = (𝑔𝑛) → ((𝑦𝑆) ≠ ∅ ↔ ((𝑔𝑛) ∩ 𝑆) ≠ ∅))
2017, 19imbi12d 348 . . . . . . . . . . 11 (𝑦 = (𝑔𝑛) → ((𝑃𝑦 → (𝑦𝑆) ≠ ∅) ↔ (𝑃 ∈ (𝑔𝑛) → ((𝑔𝑛) ∩ 𝑆) ≠ ∅)))
213elcls2 21686 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ 𝑆𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ (𝑃𝑋 ∧ ∀𝑦𝐽 (𝑃𝑦 → (𝑦𝑆) ≠ ∅))))
222, 21sylan 583 . . . . . . . . . . . . 13 ((𝐽 ∈ 1stω ∧ 𝑆𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ (𝑃𝑋 ∧ ∀𝑦𝐽 (𝑃𝑦 → (𝑦𝑆) ≠ ∅))))
2322simplbda 503 . . . . . . . . . . . 12 (((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → ∀𝑦𝐽 (𝑃𝑦 → (𝑦𝑆) ≠ ∅))
2423ad2antrr 725 . . . . . . . . . . 11 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ∀𝑦𝐽 (𝑃𝑦 → (𝑦𝑆) ≠ ∅))
25 simpr1 1191 . . . . . . . . . . . 12 ((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) → 𝑔:ℕ⟶𝐽)
2625ffvelrnda 6828 . . . . . . . . . . 11 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → (𝑔𝑛) ∈ 𝐽)
2720, 24, 26rspcdva 3573 . . . . . . . . . 10 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → (𝑃 ∈ (𝑔𝑛) → ((𝑔𝑛) ∩ 𝑆) ≠ ∅))
2816, 27mpd 15 . . . . . . . . 9 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ((𝑔𝑛) ∩ 𝑆) ≠ ∅)
29 elin 3897 . . . . . . . . . . . 12 (𝑥 ∈ ((𝑔𝑛) ∩ 𝑆) ↔ (𝑥 ∈ (𝑔𝑛) ∧ 𝑥𝑆))
3029biancomi 466 . . . . . . . . . . 11 (𝑥 ∈ ((𝑔𝑛) ∩ 𝑆) ↔ (𝑥𝑆𝑥 ∈ (𝑔𝑛)))
3130exbii 1849 . . . . . . . . . 10 (∃𝑥 𝑥 ∈ ((𝑔𝑛) ∩ 𝑆) ↔ ∃𝑥(𝑥𝑆𝑥 ∈ (𝑔𝑛)))
32 n0 4260 . . . . . . . . . 10 (((𝑔𝑛) ∩ 𝑆) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ ((𝑔𝑛) ∩ 𝑆))
33 df-rex 3112 . . . . . . . . . 10 (∃𝑥𝑆 𝑥 ∈ (𝑔𝑛) ↔ ∃𝑥(𝑥𝑆𝑥 ∈ (𝑔𝑛)))
3431, 32, 333bitr4i 306 . . . . . . . . 9 (((𝑔𝑛) ∩ 𝑆) ≠ ∅ ↔ ∃𝑥𝑆 𝑥 ∈ (𝑔𝑛))
3528, 34sylib 221 . . . . . . . 8 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ∃𝑥𝑆 𝑥 ∈ (𝑔𝑛))
362ad2antrr 725 . . . . . . . . . . . . 13 (((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝐽 ∈ Top)
373topopn 21518 . . . . . . . . . . . . 13 (𝐽 ∈ Top → 𝑋𝐽)
3836, 37syl 17 . . . . . . . . . . . 12 (((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑋𝐽)
39 simplr 768 . . . . . . . . . . . 12 (((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆𝑋)
4038, 39ssexd 5192 . . . . . . . . . . 11 (((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ∈ V)
41 fvi 6715 . . . . . . . . . . 11 (𝑆 ∈ V → ( I ‘𝑆) = 𝑆)
4240, 41syl 17 . . . . . . . . . 10 (((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → ( I ‘𝑆) = 𝑆)
4342ad2antrr 725 . . . . . . . . 9 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ( I ‘𝑆) = 𝑆)
4443rexeqdv 3365 . . . . . . . 8 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → (∃𝑥 ∈ ( I ‘𝑆)𝑥 ∈ (𝑔𝑛) ↔ ∃𝑥𝑆 𝑥 ∈ (𝑔𝑛)))
4535, 44mpbird 260 . . . . . . 7 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ∃𝑥 ∈ ( I ‘𝑆)𝑥 ∈ (𝑔𝑛))
4645ralrimiva 3149 . . . . . 6 ((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) → ∀𝑛 ∈ ℕ ∃𝑥 ∈ ( I ‘𝑆)𝑥 ∈ (𝑔𝑛))
47 fvex 6658 . . . . . . 7 ( I ‘𝑆) ∈ V
48 nnenom 13345 . . . . . . 7 ℕ ≈ ω
49 eleq1 2877 . . . . . . 7 (𝑥 = (𝑓𝑛) → (𝑥 ∈ (𝑔𝑛) ↔ (𝑓𝑛) ∈ (𝑔𝑛)))
5047, 48, 49axcc4 9852 . . . . . 6 (∀𝑛 ∈ ℕ ∃𝑥 ∈ ( I ‘𝑆)𝑥 ∈ (𝑔𝑛) → ∃𝑓(𝑓:ℕ⟶( I ‘𝑆) ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛)))
5146, 50syl 17 . . . . 5 ((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) → ∃𝑓(𝑓:ℕ⟶( I ‘𝑆) ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛)))
5242feq3d 6474 . . . . . . . . 9 (((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → (𝑓:ℕ⟶( I ‘𝑆) ↔ 𝑓:ℕ⟶𝑆))
5352biimpd 232 . . . . . . . 8 (((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → (𝑓:ℕ⟶( I ‘𝑆) → 𝑓:ℕ⟶𝑆))
5453adantr 484 . . . . . . 7 ((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) → (𝑓:ℕ⟶( I ‘𝑆) → 𝑓:ℕ⟶𝑆))
556ad2antrr 725 . . . . . . . . . 10 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛))) → 𝑃𝑋)
56 simplr3 1214 . . . . . . . . . . . . 13 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛))) → ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))
57 eleq2 2878 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑃𝑥𝑃𝑦))
58 fveq2 6645 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑗 → (𝑔𝑘) = (𝑔𝑗))
5958sseq1d 3946 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑗 → ((𝑔𝑘) ⊆ 𝑥 ↔ (𝑔𝑗) ⊆ 𝑥))
6059cbvrexvw 3397 . . . . . . . . . . . . . . . 16 (∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥 ↔ ∃𝑗 ∈ ℕ (𝑔𝑗) ⊆ 𝑥)
61 sseq2 3941 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ((𝑔𝑗) ⊆ 𝑥 ↔ (𝑔𝑗) ⊆ 𝑦))
6261rexbidv 3256 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (∃𝑗 ∈ ℕ (𝑔𝑗) ⊆ 𝑥 ↔ ∃𝑗 ∈ ℕ (𝑔𝑗) ⊆ 𝑦))
6360, 62syl5bb 286 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥 ↔ ∃𝑗 ∈ ℕ (𝑔𝑗) ⊆ 𝑦))
6457, 63imbi12d 348 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → ((𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥) ↔ (𝑃𝑦 → ∃𝑗 ∈ ℕ (𝑔𝑗) ⊆ 𝑦)))
6564rspccva 3570 . . . . . . . . . . . . 13 ((∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥) ∧ 𝑦𝐽) → (𝑃𝑦 → ∃𝑗 ∈ ℕ (𝑔𝑗) ⊆ 𝑦))
6656, 65sylan 583 . . . . . . . . . . . 12 ((((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛))) ∧ 𝑦𝐽) → (𝑃𝑦 → ∃𝑗 ∈ ℕ (𝑔𝑗) ⊆ 𝑦))
67 simpr 488 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) → (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘))
6867ralimi 3128 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘))
699, 68syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘))
7069adantr 484 . . . . . . . . . . . . . . . . . . 19 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛)) ∧ (𝑦𝐽𝑗 ∈ ℕ))) → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘))
71 simprrr 781 . . . . . . . . . . . . . . . . . . 19 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛)) ∧ (𝑦𝐽𝑗 ∈ ℕ))) → 𝑗 ∈ ℕ)
72 fveq2 6645 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑗 → (𝑔𝑛) = (𝑔𝑗))
7372sseq1d 3946 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑗 → ((𝑔𝑛) ⊆ (𝑔𝑗) ↔ (𝑔𝑗) ⊆ (𝑔𝑗)))
7473imbi2d 344 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑗 → (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔𝑛) ⊆ (𝑔𝑗)) ↔ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔𝑗) ⊆ (𝑔𝑗))))
75 fveq2 6645 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑚 → (𝑔𝑛) = (𝑔𝑚))
7675sseq1d 3946 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑚 → ((𝑔𝑛) ⊆ (𝑔𝑗) ↔ (𝑔𝑚) ⊆ (𝑔𝑗)))
7776imbi2d 344 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑚 → (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔𝑛) ⊆ (𝑔𝑗)) ↔ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔𝑚) ⊆ (𝑔𝑗))))
78 fveq2 6645 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = (𝑚 + 1) → (𝑔𝑛) = (𝑔‘(𝑚 + 1)))
7978sseq1d 3946 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = (𝑚 + 1) → ((𝑔𝑛) ⊆ (𝑔𝑗) ↔ (𝑔‘(𝑚 + 1)) ⊆ (𝑔𝑗)))
8079imbi2d 344 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = (𝑚 + 1) → (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔𝑛) ⊆ (𝑔𝑗)) ↔ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔𝑗))))
81 ssid 3937 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔𝑗) ⊆ (𝑔𝑗)
82812a1i 12 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ ℤ → ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔𝑗) ⊆ (𝑔𝑗)))
83 eluznn 12308 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ ℕ ∧ 𝑚 ∈ (ℤ𝑗)) → 𝑚 ∈ ℕ)
84 fvoveq1 7158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 𝑚 → (𝑔‘(𝑘 + 1)) = (𝑔‘(𝑚 + 1)))
85 fveq2 6645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 𝑚 → (𝑔𝑘) = (𝑔𝑚))
8684, 85sseq12d 3948 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 = 𝑚 → ((𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘) ↔ (𝑔‘(𝑚 + 1)) ⊆ (𝑔𝑚)))
8786rspccva 3570 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘) ∧ 𝑚 ∈ ℕ) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔𝑚))
8883, 87sylan2 595 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘) ∧ (𝑗 ∈ ℕ ∧ 𝑚 ∈ (ℤ𝑗))) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔𝑚))
8988anassrs 471 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (ℤ𝑗)) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔𝑚))
90 sstr2 3922 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔‘(𝑚 + 1)) ⊆ (𝑔𝑚) → ((𝑔𝑚) ⊆ (𝑔𝑗) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔𝑗)))
9189, 90syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (ℤ𝑗)) → ((𝑔𝑚) ⊆ (𝑔𝑗) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔𝑗)))
9291expcom 417 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 ∈ (ℤ𝑗) → ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘) ∧ 𝑗 ∈ ℕ) → ((𝑔𝑚) ⊆ (𝑔𝑗) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔𝑗))))
9392a2d 29 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ (ℤ𝑗) → (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔𝑚) ⊆ (𝑔𝑗)) → ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔𝑗))))
9474, 77, 80, 77, 82, 93uzind4 12296 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ (ℤ𝑗) → ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔𝑚) ⊆ (𝑔𝑗)))
9594com12 32 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘) ∧ 𝑗 ∈ ℕ) → (𝑚 ∈ (ℤ𝑗) → (𝑔𝑚) ⊆ (𝑔𝑗)))
9695ralrimiv 3148 . . . . . . . . . . . . . . . . . . 19 ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘) ∧ 𝑗 ∈ ℕ) → ∀𝑚 ∈ (ℤ𝑗)(𝑔𝑚) ⊆ (𝑔𝑗))
9770, 71, 96syl2anc 587 . . . . . . . . . . . . . . . . . 18 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛)) ∧ (𝑦𝐽𝑗 ∈ ℕ))) → ∀𝑚 ∈ (ℤ𝑗)(𝑔𝑚) ⊆ (𝑔𝑗))
98 fveq2 6645 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑚 → (𝑓𝑛) = (𝑓𝑚))
9998, 75eleq12d 2884 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑚 → ((𝑓𝑛) ∈ (𝑔𝑛) ↔ (𝑓𝑚) ∈ (𝑔𝑚)))
100 simplr 768 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛)) ∧ (𝑦𝐽𝑗 ∈ ℕ)) → ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛))
101100ad2antlr 726 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛)) ∧ (𝑦𝐽𝑗 ∈ ℕ))) ∧ 𝑚 ∈ (ℤ𝑗)) → ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛))
10271, 83sylan 583 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛)) ∧ (𝑦𝐽𝑗 ∈ ℕ))) ∧ 𝑚 ∈ (ℤ𝑗)) → 𝑚 ∈ ℕ)
10399, 101, 102rspcdva 3573 . . . . . . . . . . . . . . . . . . 19 ((((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛)) ∧ (𝑦𝐽𝑗 ∈ ℕ))) ∧ 𝑚 ∈ (ℤ𝑗)) → (𝑓𝑚) ∈ (𝑔𝑚))
104103ralrimiva 3149 . . . . . . . . . . . . . . . . . 18 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛)) ∧ (𝑦𝐽𝑗 ∈ ℕ))) → ∀𝑚 ∈ (ℤ𝑗)(𝑓𝑚) ∈ (𝑔𝑚))
105 r19.26 3137 . . . . . . . . . . . . . . . . . 18 (∀𝑚 ∈ (ℤ𝑗)((𝑔𝑚) ⊆ (𝑔𝑗) ∧ (𝑓𝑚) ∈ (𝑔𝑚)) ↔ (∀𝑚 ∈ (ℤ𝑗)(𝑔𝑚) ⊆ (𝑔𝑗) ∧ ∀𝑚 ∈ (ℤ𝑗)(𝑓𝑚) ∈ (𝑔𝑚)))
10697, 104, 105sylanbrc 586 . . . . . . . . . . . . . . . . 17 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛)) ∧ (𝑦𝐽𝑗 ∈ ℕ))) → ∀𝑚 ∈ (ℤ𝑗)((𝑔𝑚) ⊆ (𝑔𝑗) ∧ (𝑓𝑚) ∈ (𝑔𝑚)))
107 ssel2 3910 . . . . . . . . . . . . . . . . . 18 (((𝑔𝑚) ⊆ (𝑔𝑗) ∧ (𝑓𝑚) ∈ (𝑔𝑚)) → (𝑓𝑚) ∈ (𝑔𝑗))
108107ralimi 3128 . . . . . . . . . . . . . . . . 17 (∀𝑚 ∈ (ℤ𝑗)((𝑔𝑚) ⊆ (𝑔𝑗) ∧ (𝑓𝑚) ∈ (𝑔𝑚)) → ∀𝑚 ∈ (ℤ𝑗)(𝑓𝑚) ∈ (𝑔𝑗))
109106, 108syl 17 . . . . . . . . . . . . . . . 16 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛)) ∧ (𝑦𝐽𝑗 ∈ ℕ))) → ∀𝑚 ∈ (ℤ𝑗)(𝑓𝑚) ∈ (𝑔𝑗))
110 ssel 3908 . . . . . . . . . . . . . . . . 17 ((𝑔𝑗) ⊆ 𝑦 → ((𝑓𝑚) ∈ (𝑔𝑗) → (𝑓𝑚) ∈ 𝑦))
111110ralimdv 3145 . . . . . . . . . . . . . . . 16 ((𝑔𝑗) ⊆ 𝑦 → (∀𝑚 ∈ (ℤ𝑗)(𝑓𝑚) ∈ (𝑔𝑗) → ∀𝑚 ∈ (ℤ𝑗)(𝑓𝑚) ∈ 𝑦))
112109, 111syl5com 31 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛)) ∧ (𝑦𝐽𝑗 ∈ ℕ))) → ((𝑔𝑗) ⊆ 𝑦 → ∀𝑚 ∈ (ℤ𝑗)(𝑓𝑚) ∈ 𝑦))
113112anassrs 471 . . . . . . . . . . . . . 14 ((((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛))) ∧ (𝑦𝐽𝑗 ∈ ℕ)) → ((𝑔𝑗) ⊆ 𝑦 → ∀𝑚 ∈ (ℤ𝑗)(𝑓𝑚) ∈ 𝑦))
114113anassrs 471 . . . . . . . . . . . . 13 (((((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛))) ∧ 𝑦𝐽) ∧ 𝑗 ∈ ℕ) → ((𝑔𝑗) ⊆ 𝑦 → ∀𝑚 ∈ (ℤ𝑗)(𝑓𝑚) ∈ 𝑦))
115114reximdva 3233 . . . . . . . . . . . 12 ((((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛))) ∧ 𝑦𝐽) → (∃𝑗 ∈ ℕ (𝑔𝑗) ⊆ 𝑦 → ∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ𝑗)(𝑓𝑚) ∈ 𝑦))
11666, 115syld 47 . . . . . . . . . . 11 ((((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛))) ∧ 𝑦𝐽) → (𝑃𝑦 → ∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ𝑗)(𝑓𝑚) ∈ 𝑦))
117116ralrimiva 3149 . . . . . . . . . 10 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛))) → ∀𝑦𝐽 (𝑃𝑦 → ∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ𝑗)(𝑓𝑚) ∈ 𝑦))
11836ad2antrr 725 . . . . . . . . . . . 12 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛))) → 𝐽 ∈ Top)
1193toptopon 21529 . . . . . . . . . . . 12 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
120118, 119sylib 221 . . . . . . . . . . 11 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛))) → 𝐽 ∈ (TopOn‘𝑋))
121 nnuz 12271 . . . . . . . . . . 11 ℕ = (ℤ‘1)
122 1zzd 12003 . . . . . . . . . . 11 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛))) → 1 ∈ ℤ)
123 simprl 770 . . . . . . . . . . . 12 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛))) → 𝑓:ℕ⟶𝑆)
12439ad2antrr 725 . . . . . . . . . . . 12 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛))) → 𝑆𝑋)
125123, 124fssd 6502 . . . . . . . . . . 11 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛))) → 𝑓:ℕ⟶𝑋)
126 eqidd 2799 . . . . . . . . . . 11 ((((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛))) ∧ 𝑚 ∈ ℕ) → (𝑓𝑚) = (𝑓𝑚))
127120, 121, 122, 125, 126lmbrf 21872 . . . . . . . . . 10 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛))) → (𝑓(⇝𝑡𝐽)𝑃 ↔ (𝑃𝑋 ∧ ∀𝑦𝐽 (𝑃𝑦 → ∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ𝑗)(𝑓𝑚) ∈ 𝑦))))
12855, 117, 127mpbir2and 712 . . . . . . . . 9 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛))) → 𝑓(⇝𝑡𝐽)𝑃)
129128expr 460 . . . . . . . 8 (((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) ∧ 𝑓:ℕ⟶𝑆) → (∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛) → 𝑓(⇝𝑡𝐽)𝑃))
130129imdistanda 575 . . . . . . 7 ((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) → ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛)) → (𝑓:ℕ⟶𝑆𝑓(⇝𝑡𝐽)𝑃)))
13154, 130syland 605 . . . . . 6 ((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) → ((𝑓:ℕ⟶( I ‘𝑆) ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛)) → (𝑓:ℕ⟶𝑆𝑓(⇝𝑡𝐽)𝑃)))
132131eximdv 1918 . . . . 5 ((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) → (∃𝑓(𝑓:ℕ⟶( I ‘𝑆) ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ (𝑔𝑛)) → ∃𝑓(𝑓:ℕ⟶𝑆𝑓(⇝𝑡𝐽)𝑃)))
13351, 132mpd 15 . . . 4 ((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔𝑘)) ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑥))) → ∃𝑓(𝑓:ℕ⟶𝑆𝑓(⇝𝑡𝐽)𝑃))
1348, 133exlimddv 1936 . . 3 (((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → ∃𝑓(𝑓:ℕ⟶𝑆𝑓(⇝𝑡𝐽)𝑃))
135134ex 416 . 2 ((𝐽 ∈ 1stω ∧ 𝑆𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) → ∃𝑓(𝑓:ℕ⟶𝑆𝑓(⇝𝑡𝐽)𝑃)))
1362ad2antrr 725 . . . . . 6 (((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ (𝑓:ℕ⟶𝑆𝑓(⇝𝑡𝐽)𝑃)) → 𝐽 ∈ Top)
137136, 119sylib 221 . . . . 5 (((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ (𝑓:ℕ⟶𝑆𝑓(⇝𝑡𝐽)𝑃)) → 𝐽 ∈ (TopOn‘𝑋))
138 1zzd 12003 . . . . 5 (((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ (𝑓:ℕ⟶𝑆𝑓(⇝𝑡𝐽)𝑃)) → 1 ∈ ℤ)
139 simprr 772 . . . . 5 (((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ (𝑓:ℕ⟶𝑆𝑓(⇝𝑡𝐽)𝑃)) → 𝑓(⇝𝑡𝐽)𝑃)
140 simprl 770 . . . . . 6 (((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ (𝑓:ℕ⟶𝑆𝑓(⇝𝑡𝐽)𝑃)) → 𝑓:ℕ⟶𝑆)
141140ffvelrnda 6828 . . . . 5 ((((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ (𝑓:ℕ⟶𝑆𝑓(⇝𝑡𝐽)𝑃)) ∧ 𝑘 ∈ ℕ) → (𝑓𝑘) ∈ 𝑆)
142 simplr 768 . . . . 5 (((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ (𝑓:ℕ⟶𝑆𝑓(⇝𝑡𝐽)𝑃)) → 𝑆𝑋)
143121, 137, 138, 139, 141, 142lmcls 21914 . . . 4 (((𝐽 ∈ 1stω ∧ 𝑆𝑋) ∧ (𝑓:ℕ⟶𝑆𝑓(⇝𝑡𝐽)𝑃)) → 𝑃 ∈ ((cls‘𝐽)‘𝑆))
144143ex 416 . . 3 ((𝐽 ∈ 1stω ∧ 𝑆𝑋) → ((𝑓:ℕ⟶𝑆𝑓(⇝𝑡𝐽)𝑃) → 𝑃 ∈ ((cls‘𝐽)‘𝑆)))
145144exlimdv 1934 . 2 ((𝐽 ∈ 1stω ∧ 𝑆𝑋) → (∃𝑓(𝑓:ℕ⟶𝑆𝑓(⇝𝑡𝐽)𝑃) → 𝑃 ∈ ((cls‘𝐽)‘𝑆)))
146135, 145impbid 215 1 ((𝐽 ∈ 1stω ∧ 𝑆𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∃𝑓(𝑓:ℕ⟶𝑆𝑓(⇝𝑡𝐽)𝑃)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  Vcvv 3441   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  ∪ cuni 4800   class class class wbr 5030   I cid 5424  ⟶wf 6320  ‘cfv 6324  (class class class)co 7135  1c1 10529   + caddc 10531  ℕcn 11627  ℤcz 11971  ℤ≥cuz 12233  Topctop 21505  TopOnctopon 21522  clsccl 21630  ⇝𝑡clm 21838  1stωc1stc 22049 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7443  ax-inf2 9090  ax-cc 9848  ax-cnex 10584  ax-resscn 10585  ax-1cn 10586  ax-icn 10587  ax-addcl 10588  ax-addrcl 10589  ax-mulcl 10590  ax-mulrcl 10591  ax-mulcom 10592  ax-addass 10593  ax-mulass 10594  ax-distr 10595  ax-i2m1 10596  ax-1ne0 10597  ax-1rid 10598  ax-rnegex 10599  ax-rrecex 10600  ax-cnre 10601  ax-pre-lttri 10602  ax-pre-lttrn 10603  ax-pre-ltadd 10604  ax-pre-mulgt0 10605 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-iin 4884  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7563  df-1st 7673  df-2nd 7674  df-wrecs 7932  df-recs 7993  df-rdg 8031  df-1o 8087  df-oadd 8091  df-er 8274  df-pm 8394  df-en 8495  df-dom 8496  df-sdom 8497  df-fin 8498  df-pnf 10668  df-mnf 10669  df-xr 10670  df-ltxr 10671  df-le 10672  df-sub 10863  df-neg 10864  df-nn 11628  df-n0 11888  df-z 11972  df-uz 12234  df-fz 12888  df-top 21506  df-topon 21523  df-cld 21631  df-ntr 21632  df-cls 21633  df-lm 21841  df-1stc 22051 This theorem is referenced by:  1stccnp  22074  hausmapdom  22112  1stckgen  22166  metelcls  23916
 Copyright terms: Public domain W3C validator