Step | Hyp | Ref
| Expression |
1 | | simpll 786 |
. . . . 5
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝐽 ∈
1st𝜔) |
2 | | 1stctop 21056 |
. . . . . . 7
⊢ (𝐽 ∈ 1st𝜔
→ 𝐽 ∈
Top) |
3 | | 1stcelcls.1 |
. . . . . . . 8
⊢ 𝑋 = ∪
𝐽 |
4 | 3 | clsss3 20673 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋) |
5 | 2, 4 | sylan 487 |
. . . . . 6
⊢ ((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋) |
6 | 5 | sselda 3568 |
. . . . 5
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑃 ∈ 𝑋) |
7 | 3 | 1stcfb 21058 |
. . . . 5
⊢ ((𝐽 ∈ 1st𝜔
∧ 𝑃 ∈ 𝑋) → ∃𝑔(𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) |
8 | 1, 6, 7 | syl2anc 691 |
. . . 4
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → ∃𝑔(𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) |
9 | | simpr1 1060 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → 𝑔:ℕ⟶𝐽) |
10 | 9 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → (𝑔‘𝑛) ∈ 𝐽) |
11 | 3 | elcls2 20688 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅)))) |
12 | 2, 11 | sylan 487 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅)))) |
13 | 12 | simplbda 652 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅)) |
14 | 13 | ad2antrr 758 |
. . . . . . . . . 10
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅)) |
15 | | simpr2 1061 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘))) |
16 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) → 𝑃 ∈ (𝑔‘𝑘)) |
17 | 16 | ralimi 2936 |
. . . . . . . . . . . 12
⊢
(∀𝑘 ∈
ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) → ∀𝑘 ∈ ℕ 𝑃 ∈ (𝑔‘𝑘)) |
18 | 15, 17 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∀𝑘 ∈ ℕ 𝑃 ∈ (𝑔‘𝑘)) |
19 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → (𝑔‘𝑘) = (𝑔‘𝑛)) |
20 | 19 | eleq2d 2673 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → (𝑃 ∈ (𝑔‘𝑘) ↔ 𝑃 ∈ (𝑔‘𝑛))) |
21 | 20 | rspccva 3281 |
. . . . . . . . . . 11
⊢
((∀𝑘 ∈
ℕ 𝑃 ∈ (𝑔‘𝑘) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ (𝑔‘𝑛)) |
22 | 18, 21 | sylan 487 |
. . . . . . . . . 10
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ (𝑔‘𝑛)) |
23 | | eleq2 2677 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑔‘𝑛) → (𝑃 ∈ 𝑦 ↔ 𝑃 ∈ (𝑔‘𝑛))) |
24 | | ineq1 3769 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑔‘𝑛) → (𝑦 ∩ 𝑆) = ((𝑔‘𝑛) ∩ 𝑆)) |
25 | 24 | neeq1d 2841 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑔‘𝑛) → ((𝑦 ∩ 𝑆) ≠ ∅ ↔ ((𝑔‘𝑛) ∩ 𝑆) ≠ ∅)) |
26 | 23, 25 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑔‘𝑛) → ((𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅) ↔ (𝑃 ∈ (𝑔‘𝑛) → ((𝑔‘𝑛) ∩ 𝑆) ≠ ∅))) |
27 | 26 | rspcv 3278 |
. . . . . . . . . 10
⊢ ((𝑔‘𝑛) ∈ 𝐽 → (∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅) → (𝑃 ∈ (𝑔‘𝑛) → ((𝑔‘𝑛) ∩ 𝑆) ≠ ∅))) |
28 | 10, 14, 22, 27 | syl3c 64 |
. . . . . . . . 9
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ((𝑔‘𝑛) ∩ 𝑆) ≠ ∅) |
29 | | elin 3758 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((𝑔‘𝑛) ∩ 𝑆) ↔ (𝑥 ∈ (𝑔‘𝑛) ∧ 𝑥 ∈ 𝑆)) |
30 | | ancom 465 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝑔‘𝑛) ∧ 𝑥 ∈ 𝑆) ↔ (𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑔‘𝑛))) |
31 | 29, 30 | bitri 263 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ((𝑔‘𝑛) ∩ 𝑆) ↔ (𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑔‘𝑛))) |
32 | 31 | exbii 1764 |
. . . . . . . . . 10
⊢
(∃𝑥 𝑥 ∈ ((𝑔‘𝑛) ∩ 𝑆) ↔ ∃𝑥(𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑔‘𝑛))) |
33 | | n0 3890 |
. . . . . . . . . 10
⊢ (((𝑔‘𝑛) ∩ 𝑆) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ ((𝑔‘𝑛) ∩ 𝑆)) |
34 | | df-rex 2902 |
. . . . . . . . . 10
⊢
(∃𝑥 ∈
𝑆 𝑥 ∈ (𝑔‘𝑛) ↔ ∃𝑥(𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝑔‘𝑛))) |
35 | 32, 33, 34 | 3bitr4i 291 |
. . . . . . . . 9
⊢ (((𝑔‘𝑛) ∩ 𝑆) ≠ ∅ ↔ ∃𝑥 ∈ 𝑆 𝑥 ∈ (𝑔‘𝑛)) |
36 | 28, 35 | sylib 207 |
. . . . . . . 8
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ∃𝑥 ∈ 𝑆 𝑥 ∈ (𝑔‘𝑛)) |
37 | 2 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝐽 ∈ Top) |
38 | 3 | topopn 20536 |
. . . . . . . . . . . . 13
⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑋 ∈ 𝐽) |
40 | | simplr 788 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ⊆ 𝑋) |
41 | 39, 40 | ssexd 4733 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ∈ V) |
42 | | fvi 6165 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ V → ( I
‘𝑆) = 𝑆) |
43 | 41, 42 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → ( I ‘𝑆) = 𝑆) |
44 | 43 | ad2antrr 758 |
. . . . . . . . 9
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ( I ‘𝑆) = 𝑆) |
45 | 44 | rexeqdv 3122 |
. . . . . . . 8
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → (∃𝑥 ∈ ( I ‘𝑆)𝑥 ∈ (𝑔‘𝑛) ↔ ∃𝑥 ∈ 𝑆 𝑥 ∈ (𝑔‘𝑛))) |
46 | 36, 45 | mpbird 246 |
. . . . . . 7
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑛 ∈ ℕ) → ∃𝑥 ∈ ( I ‘𝑆)𝑥 ∈ (𝑔‘𝑛)) |
47 | 46 | ralrimiva 2949 |
. . . . . 6
⊢ ((((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∀𝑛 ∈ ℕ ∃𝑥 ∈ ( I ‘𝑆)𝑥 ∈ (𝑔‘𝑛)) |
48 | | fvex 6113 |
. . . . . . 7
⊢ ( I
‘𝑆) ∈
V |
49 | | nnenom 12641 |
. . . . . . 7
⊢ ℕ
≈ ω |
50 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑥 = (𝑓‘𝑛) → (𝑥 ∈ (𝑔‘𝑛) ↔ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) |
51 | 48, 49, 50 | axcc4 9144 |
. . . . . 6
⊢
(∀𝑛 ∈
ℕ ∃𝑥 ∈ ( I
‘𝑆)𝑥 ∈ (𝑔‘𝑛) → ∃𝑓(𝑓:ℕ⟶( I ‘𝑆) ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) |
52 | 47, 51 | syl 17 |
. . . . 5
⊢ ((((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∃𝑓(𝑓:ℕ⟶( I ‘𝑆) ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) |
53 | 43 | feq3d 5945 |
. . . . . . . . 9
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → (𝑓:ℕ⟶( I ‘𝑆) ↔ 𝑓:ℕ⟶𝑆)) |
54 | 53 | biimpd 218 |
. . . . . . . 8
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → (𝑓:ℕ⟶( I ‘𝑆) → 𝑓:ℕ⟶𝑆)) |
55 | 54 | adantr 480 |
. . . . . . 7
⊢ ((((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → (𝑓:ℕ⟶( I ‘𝑆) → 𝑓:ℕ⟶𝑆)) |
56 | 6 | ad2antrr 758 |
. . . . . . . . . 10
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝑃 ∈ 𝑋) |
57 | | simplr3 1098 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥)) |
58 | | eleq2 2677 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝑃 ∈ 𝑥 ↔ 𝑃 ∈ 𝑦)) |
59 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑗 → (𝑔‘𝑘) = (𝑔‘𝑗)) |
60 | 59 | sseq1d 3595 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑗 → ((𝑔‘𝑘) ⊆ 𝑥 ↔ (𝑔‘𝑗) ⊆ 𝑥)) |
61 | 60 | cbvrexv 3148 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑘 ∈
ℕ (𝑔‘𝑘) ⊆ 𝑥 ↔ ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑥) |
62 | | sseq2 3590 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → ((𝑔‘𝑗) ⊆ 𝑥 ↔ (𝑔‘𝑗) ⊆ 𝑦)) |
63 | 62 | rexbidv 3034 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑥 ↔ ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦)) |
64 | 61, 63 | syl5bb 271 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥 ↔ ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦)) |
65 | 58, 64 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ((𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥) ↔ (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦))) |
66 | 65 | rspccva 3281 |
. . . . . . . . . . . . 13
⊢
((∀𝑥 ∈
𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥) ∧ 𝑦 ∈ 𝐽) → (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦)) |
67 | 57, 66 | sylan 487 |
. . . . . . . . . . . 12
⊢
((((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ 𝑦 ∈ 𝐽) → (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦)) |
68 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) → (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) |
69 | 68 | ralimi 2936 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑘 ∈
ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) |
70 | 15, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) |
71 | 70 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) |
72 | | simprrr 801 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → 𝑗 ∈ ℕ) |
73 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = 𝑗 → (𝑔‘𝑛) = (𝑔‘𝑗)) |
74 | 73 | sseq1d 3595 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑗 → ((𝑔‘𝑛) ⊆ (𝑔‘𝑗) ↔ (𝑔‘𝑗) ⊆ (𝑔‘𝑗))) |
75 | 74 | imbi2d 329 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑗 → (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑛) ⊆ (𝑔‘𝑗)) ↔ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑗) ⊆ (𝑔‘𝑗)))) |
76 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = 𝑚 → (𝑔‘𝑛) = (𝑔‘𝑚)) |
77 | 76 | sseq1d 3595 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑚 → ((𝑔‘𝑛) ⊆ (𝑔‘𝑗) ↔ (𝑔‘𝑚) ⊆ (𝑔‘𝑗))) |
78 | 77 | imbi2d 329 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑚 → (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑛) ⊆ (𝑔‘𝑗)) ↔ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑚) ⊆ (𝑔‘𝑗)))) |
79 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = (𝑚 + 1) → (𝑔‘𝑛) = (𝑔‘(𝑚 + 1))) |
80 | 79 | sseq1d 3595 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = (𝑚 + 1) → ((𝑔‘𝑛) ⊆ (𝑔‘𝑗) ↔ (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑗))) |
81 | 80 | imbi2d 329 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = (𝑚 + 1) → (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑛) ⊆ (𝑔‘𝑗)) ↔ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑗)))) |
82 | | ssid 3587 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑔‘𝑗) ⊆ (𝑔‘𝑗) |
83 | 82 | 2a1i 12 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈ ℤ →
((∀𝑘 ∈ ℕ
(𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑗) ⊆ (𝑔‘𝑗))) |
84 | | eluznn 11634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑗 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘𝑗)) → 𝑚 ∈ ℕ) |
85 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑘 = 𝑚 → (𝑘 + 1) = (𝑚 + 1)) |
86 | 85 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑘 = 𝑚 → (𝑔‘(𝑘 + 1)) = (𝑔‘(𝑚 + 1))) |
87 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑘 = 𝑚 → (𝑔‘𝑘) = (𝑔‘𝑚)) |
88 | 86, 87 | sseq12d 3597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑘 = 𝑚 → ((𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ↔ (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑚))) |
89 | 88 | rspccva 3281 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((∀𝑘 ∈
ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑚 ∈ ℕ) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑚)) |
90 | 84, 89 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((∀𝑘 ∈
ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ (𝑗 ∈ ℕ ∧ 𝑚 ∈ (ℤ≥‘𝑗))) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑚)) |
91 | 90 | anassrs 678 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((∀𝑘 ∈
ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑚)) |
92 | | sstr2 3575 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑚) → ((𝑔‘𝑚) ⊆ (𝑔‘𝑗) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑗))) |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((∀𝑘 ∈
ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → ((𝑔‘𝑚) ⊆ (𝑔‘𝑗) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑗))) |
94 | 93 | expcom 450 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 ∈
(ℤ≥‘𝑗) → ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → ((𝑔‘𝑚) ⊆ (𝑔‘𝑗) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑗)))) |
95 | 94 | a2d 29 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 ∈
(ℤ≥‘𝑗) → (((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑚) ⊆ (𝑔‘𝑗)) → ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘(𝑚 + 1)) ⊆ (𝑔‘𝑗)))) |
96 | 75, 78, 81, 78, 83, 95 | uzind4 11622 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈
(ℤ≥‘𝑗) → ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑔‘𝑚) ⊆ (𝑔‘𝑗))) |
97 | 96 | com12 32 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑘 ∈
ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → (𝑚 ∈ (ℤ≥‘𝑗) → (𝑔‘𝑚) ⊆ (𝑔‘𝑗))) |
98 | 97 | ralrimiv 2948 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑘 ∈
ℕ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘) ∧ 𝑗 ∈ ℕ) → ∀𝑚 ∈
(ℤ≥‘𝑗)(𝑔‘𝑚) ⊆ (𝑔‘𝑗)) |
99 | 71, 72, 98 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ∀𝑚 ∈
(ℤ≥‘𝑗)(𝑔‘𝑚) ⊆ (𝑔‘𝑗)) |
100 | 72, 84 | sylan 487 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → 𝑚 ∈ ℕ) |
101 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ)) → ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) |
102 | 101 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) |
103 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑚 → (𝑓‘𝑛) = (𝑓‘𝑚)) |
104 | 103, 76 | eleq12d 2682 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑚 → ((𝑓‘𝑛) ∈ (𝑔‘𝑛) ↔ (𝑓‘𝑚) ∈ (𝑔‘𝑚))) |
105 | 104 | rspcv 3278 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ ℕ →
(∀𝑛 ∈ ℕ
(𝑓‘𝑛) ∈ (𝑔‘𝑛) → (𝑓‘𝑚) ∈ (𝑔‘𝑚))) |
106 | 100, 102,
105 | sylc 63 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (𝑓‘𝑚) ∈ (𝑔‘𝑚)) |
107 | 106 | ralrimiva 2949 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ∀𝑚 ∈
(ℤ≥‘𝑗)(𝑓‘𝑚) ∈ (𝑔‘𝑚)) |
108 | | r19.26 3046 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑚 ∈
(ℤ≥‘𝑗)((𝑔‘𝑚) ⊆ (𝑔‘𝑗) ∧ (𝑓‘𝑚) ∈ (𝑔‘𝑚)) ↔ (∀𝑚 ∈ (ℤ≥‘𝑗)(𝑔‘𝑚) ⊆ (𝑔‘𝑗) ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ (𝑔‘𝑚))) |
109 | 99, 107, 108 | sylanbrc 695 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ∀𝑚 ∈
(ℤ≥‘𝑗)((𝑔‘𝑚) ⊆ (𝑔‘𝑗) ∧ (𝑓‘𝑚) ∈ (𝑔‘𝑚))) |
110 | | ssel2 3563 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑔‘𝑚) ⊆ (𝑔‘𝑗) ∧ (𝑓‘𝑚) ∈ (𝑔‘𝑚)) → (𝑓‘𝑚) ∈ (𝑔‘𝑗)) |
111 | 110 | ralimi 2936 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑚 ∈
(ℤ≥‘𝑗)((𝑔‘𝑚) ⊆ (𝑔‘𝑗) ∧ (𝑓‘𝑚) ∈ (𝑔‘𝑚)) → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ (𝑔‘𝑗)) |
112 | 109, 111 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ∀𝑚 ∈
(ℤ≥‘𝑗)(𝑓‘𝑚) ∈ (𝑔‘𝑗)) |
113 | | ssel 3562 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔‘𝑗) ⊆ 𝑦 → ((𝑓‘𝑚) ∈ (𝑔‘𝑗) → (𝑓‘𝑚) ∈ 𝑦)) |
114 | 113 | ralimdv 2946 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔‘𝑗) ⊆ 𝑦 → (∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ (𝑔‘𝑗) → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦)) |
115 | 112, 114 | syl5com 31 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ))) → ((𝑔‘𝑗) ⊆ 𝑦 → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦)) |
116 | 115 | anassrs 678 |
. . . . . . . . . . . . . 14
⊢
((((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑗 ∈ ℕ)) → ((𝑔‘𝑗) ⊆ 𝑦 → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦)) |
117 | 116 | anassrs 678 |
. . . . . . . . . . . . 13
⊢
(((((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ 𝑦 ∈ 𝐽) ∧ 𝑗 ∈ ℕ) → ((𝑔‘𝑗) ⊆ 𝑦 → ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦)) |
118 | 117 | reximdva 3000 |
. . . . . . . . . . . 12
⊢
((((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ 𝑦 ∈ 𝐽) → (∃𝑗 ∈ ℕ (𝑔‘𝑗) ⊆ 𝑦 → ∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦)) |
119 | 67, 118 | syld 46 |
. . . . . . . . . . 11
⊢
((((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ 𝑦 ∈ 𝐽) → (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦)) |
120 | 119 | ralrimiva 2949 |
. . . . . . . . . 10
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦)) |
121 | 37 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝐽 ∈ Top) |
122 | 3 | toptopon 20548 |
. . . . . . . . . . . 12
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
123 | 121, 122 | sylib 207 |
. . . . . . . . . . 11
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝐽 ∈ (TopOn‘𝑋)) |
124 | | nnuz 11599 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
125 | | 1zzd 11285 |
. . . . . . . . . . 11
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 1 ∈ ℤ) |
126 | | simprl 790 |
. . . . . . . . . . . 12
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝑓:ℕ⟶𝑆) |
127 | 40 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝑆 ⊆ 𝑋) |
128 | 126, 127 | fssd 5970 |
. . . . . . . . . . 11
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝑓:ℕ⟶𝑋) |
129 | | eqidd 2611 |
. . . . . . . . . . 11
⊢
((((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) ∧ 𝑚 ∈ ℕ) → (𝑓‘𝑚) = (𝑓‘𝑚)) |
130 | 123, 124,
125, 128, 129 | lmbrf 20874 |
. . . . . . . . . 10
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → (𝑓(⇝𝑡‘𝐽)𝑃 ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → ∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑗)(𝑓‘𝑚) ∈ 𝑦)))) |
131 | 56, 120, 130 | mpbir2and 959 |
. . . . . . . . 9
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ (𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛))) → 𝑓(⇝𝑡‘𝐽)𝑃) |
132 | 131 | expr 641 |
. . . . . . . 8
⊢
(((((𝐽 ∈
1st𝜔 ∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) ∧ 𝑓:ℕ⟶𝑆) → (∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛) → 𝑓(⇝𝑡‘𝐽)𝑃)) |
133 | 132 | imdistanda 725 |
. . . . . . 7
⊢ ((((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ((𝑓:ℕ⟶𝑆 ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) → (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃))) |
134 | 55, 133 | syland 497 |
. . . . . 6
⊢ ((((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ((𝑓:ℕ⟶( I ‘𝑆) ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) → (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃))) |
135 | 134 | eximdv 1833 |
. . . . 5
⊢ ((((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → (∃𝑓(𝑓:ℕ⟶( I ‘𝑆) ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ∈ (𝑔‘𝑛)) → ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃))) |
136 | 52, 135 | mpd 15 |
. . . 4
⊢ ((((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑔:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝑃 ∈ (𝑔‘𝑘) ∧ (𝑔‘(𝑘 + 1)) ⊆ (𝑔‘𝑘)) ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑥))) → ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) |
137 | 8, 136 | exlimddv 1850 |
. . 3
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) |
138 | 137 | ex 449 |
. 2
⊢ ((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) → ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃))) |
139 | 2 | ad2antrr 758 |
. . . . . 6
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝐽 ∈ Top) |
140 | 139, 122 | sylib 207 |
. . . . 5
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝐽 ∈ (TopOn‘𝑋)) |
141 | | 1zzd 11285 |
. . . . 5
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 1 ∈ ℤ) |
142 | | simprr 792 |
. . . . 5
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝑓(⇝𝑡‘𝐽)𝑃) |
143 | | simprl 790 |
. . . . . 6
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝑓:ℕ⟶𝑆) |
144 | 143 | ffvelrnda 6267 |
. . . . 5
⊢ ((((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) ∈ 𝑆) |
145 | | simplr 788 |
. . . . 5
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝑆 ⊆ 𝑋) |
146 | 124, 140,
141, 142, 144, 145 | lmcls 20916 |
. . . 4
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) ∧ (𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝑃 ∈ ((cls‘𝐽)‘𝑆)) |
147 | 146 | ex 449 |
. . 3
⊢ ((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) → ((𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → 𝑃 ∈ ((cls‘𝐽)‘𝑆))) |
148 | 147 | exlimdv 1848 |
. 2
⊢ ((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) → (∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → 𝑃 ∈ ((cls‘𝐽)‘𝑆))) |
149 | 138, 148 | impbid 201 |
1
⊢ ((𝐽 ∈ 1st𝜔
∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃))) |