Step | Hyp | Ref
| Expression |
1 | | llytop 21085 |
. . . 4
⊢ (𝑗 ∈ Locally
1st𝜔 → 𝑗 ∈ Top) |
2 | | simprr 792 |
. . . . . . . . 9
⊢ ((((𝑗 ∈ Locally
1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) →
(𝑗 ↾t
𝑢) ∈
1st𝜔) |
3 | | simprl 790 |
. . . . . . . . . 10
⊢ ((((𝑗 ∈ Locally
1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) →
𝑥 ∈ 𝑢) |
4 | 1 | ad3antrrr 762 |
. . . . . . . . . . 11
⊢ ((((𝑗 ∈ Locally
1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) →
𝑗 ∈
Top) |
5 | | elssuni 4403 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ 𝑗 → 𝑢 ⊆ ∪ 𝑗) |
6 | 5 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ ((((𝑗 ∈ Locally
1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) →
𝑢 ⊆ ∪ 𝑗) |
7 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ ∪ 𝑗 =
∪ 𝑗 |
8 | 7 | restuni 20776 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ Top ∧ 𝑢 ⊆ ∪ 𝑗)
→ 𝑢 = ∪ (𝑗
↾t 𝑢)) |
9 | 4, 6, 8 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((((𝑗 ∈ Locally
1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) →
𝑢 = ∪ (𝑗
↾t 𝑢)) |
10 | 3, 9 | eleqtrd 2690 |
. . . . . . . . 9
⊢ ((((𝑗 ∈ Locally
1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) →
𝑥 ∈ ∪ (𝑗
↾t 𝑢)) |
11 | | eqid 2610 |
. . . . . . . . . 10
⊢ ∪ (𝑗
↾t 𝑢) =
∪ (𝑗 ↾t 𝑢) |
12 | 11 | 1stcclb 21057 |
. . . . . . . . 9
⊢ (((𝑗 ↾t 𝑢) ∈ 1st𝜔
∧ 𝑥 ∈ ∪ (𝑗
↾t 𝑢))
→ ∃𝑡 ∈
𝒫 (𝑗
↾t 𝑢)(𝑡 ≼ ω ∧ ∀𝑣 ∈ (𝑗 ↾t 𝑢)(𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣)))) |
13 | 2, 10, 12 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝑗 ∈ Locally
1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) →
∃𝑡 ∈ 𝒫
(𝑗 ↾t
𝑢)(𝑡 ≼ ω ∧ ∀𝑣 ∈ (𝑗 ↾t 𝑢)(𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣)))) |
14 | | elpwi 4117 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢) → 𝑡 ⊆ (𝑗 ↾t 𝑢)) |
15 | 14 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢)) → 𝑡 ⊆ (𝑗 ↾t 𝑢)) |
16 | 15 | sselda 3568 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢)) ∧ 𝑛 ∈ 𝑡) → 𝑛 ∈ (𝑗 ↾t 𝑢)) |
17 | 4 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢)) → 𝑗 ∈ Top) |
18 | | simpllr 795 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢)) → 𝑢 ∈ 𝑗) |
19 | | restopn2 20791 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ Top ∧ 𝑢 ∈ 𝑗) → (𝑛 ∈ (𝑗 ↾t 𝑢) ↔ (𝑛 ∈ 𝑗 ∧ 𝑛 ⊆ 𝑢))) |
20 | 17, 18, 19 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢)) → (𝑛 ∈ (𝑗 ↾t 𝑢) ↔ (𝑛 ∈ 𝑗 ∧ 𝑛 ⊆ 𝑢))) |
21 | 20 | simplbda 652 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢)) ∧ 𝑛 ∈ (𝑗 ↾t 𝑢)) → 𝑛 ⊆ 𝑢) |
22 | 16, 21 | syldan 486 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢)) ∧ 𝑛 ∈ 𝑡) → 𝑛 ⊆ 𝑢) |
23 | | df-ss 3554 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ⊆ 𝑢 ↔ (𝑛 ∩ 𝑢) = 𝑛) |
24 | 22, 23 | sylib 207 |
. . . . . . . . . . . . . 14
⊢
((((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢)) ∧ 𝑛 ∈ 𝑡) → (𝑛 ∩ 𝑢) = 𝑛) |
25 | 20 | simprbda 651 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢)) ∧ 𝑛 ∈ (𝑗 ↾t 𝑢)) → 𝑛 ∈ 𝑗) |
26 | 16, 25 | syldan 486 |
. . . . . . . . . . . . . 14
⊢
((((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢)) ∧ 𝑛 ∈ 𝑡) → 𝑛 ∈ 𝑗) |
27 | 24, 26 | eqeltrd 2688 |
. . . . . . . . . . . . 13
⊢
((((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢)) ∧ 𝑛 ∈ 𝑡) → (𝑛 ∩ 𝑢) ∈ 𝑗) |
28 | | ineq1 3769 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑛 → (𝑎 ∩ 𝑢) = (𝑛 ∩ 𝑢)) |
29 | 28 | cbvmptv 4678 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢)) = (𝑛 ∈ 𝑡 ↦ (𝑛 ∩ 𝑢)) |
30 | 27, 29 | fmptd 6292 |
. . . . . . . . . . . 12
⊢
(((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢)) → (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢)):𝑡⟶𝑗) |
31 | | frn 5966 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢)):𝑡⟶𝑗 → ran (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢)) ⊆ 𝑗) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . 11
⊢
(((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢)) → ran (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢)) ⊆ 𝑗) |
33 | 32 | adantrr 749 |
. . . . . . . . . 10
⊢
(((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
(𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢) ∧ (𝑡 ≼ ω ∧ ∀𝑣 ∈ (𝑗 ↾t 𝑢)(𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣))))) → ran (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢)) ⊆ 𝑗) |
34 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑗 ∈ V |
35 | 34 | elpw2 4755 |
. . . . . . . . . 10
⊢ (ran
(𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢)) ∈ 𝒫 𝑗 ↔ ran (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢)) ⊆ 𝑗) |
36 | 33, 35 | sylibr 223 |
. . . . . . . . 9
⊢
(((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
(𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢) ∧ (𝑡 ≼ ω ∧ ∀𝑣 ∈ (𝑗 ↾t 𝑢)(𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣))))) → ran (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢)) ∈ 𝒫 𝑗) |
37 | | simprrl 800 |
. . . . . . . . . 10
⊢
(((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
(𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢) ∧ (𝑡 ≼ ω ∧ ∀𝑣 ∈ (𝑗 ↾t 𝑢)(𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣))))) → 𝑡 ≼ ω) |
38 | | 1stcrestlem 21065 |
. . . . . . . . . 10
⊢ (𝑡 ≼ ω → ran
(𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢)) ≼ ω) |
39 | 37, 38 | syl 17 |
. . . . . . . . 9
⊢
(((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
(𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢) ∧ (𝑡 ≼ ω ∧ ∀𝑣 ∈ (𝑗 ↾t 𝑢)(𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣))))) → ran (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢)) ≼ ω) |
40 | 4 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢
((((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
(𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢) ∧ (𝑡 ≼ ω ∧ ∀𝑣 ∈ (𝑗 ↾t 𝑢)(𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣))))) ∧ (𝑧 ∈ 𝑗 ∧ 𝑥 ∈ 𝑧)) → 𝑗 ∈ Top) |
41 | | simpllr 795 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
(𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢) ∧ (𝑡 ≼ ω ∧ ∀𝑣 ∈ (𝑗 ↾t 𝑢)(𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣))))) → 𝑢 ∈ 𝑗) |
42 | 41 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
((((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
(𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢) ∧ (𝑡 ≼ ω ∧ ∀𝑣 ∈ (𝑗 ↾t 𝑢)(𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣))))) ∧ (𝑧 ∈ 𝑗 ∧ 𝑥 ∈ 𝑧)) → 𝑢 ∈ 𝑗) |
43 | | simprl 790 |
. . . . . . . . . . . . . 14
⊢
((((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
(𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢) ∧ (𝑡 ≼ ω ∧ ∀𝑣 ∈ (𝑗 ↾t 𝑢)(𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣))))) ∧ (𝑧 ∈ 𝑗 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ∈ 𝑗) |
44 | | elrestr 15912 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ Top ∧ 𝑢 ∈ 𝑗 ∧ 𝑧 ∈ 𝑗) → (𝑧 ∩ 𝑢) ∈ (𝑗 ↾t 𝑢)) |
45 | 40, 42, 43, 44 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢
((((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
(𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢) ∧ (𝑡 ≼ ω ∧ ∀𝑣 ∈ (𝑗 ↾t 𝑢)(𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣))))) ∧ (𝑧 ∈ 𝑗 ∧ 𝑥 ∈ 𝑧)) → (𝑧 ∩ 𝑢) ∈ (𝑗 ↾t 𝑢)) |
46 | | simprrr 801 |
. . . . . . . . . . . . . 14
⊢
(((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
(𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢) ∧ (𝑡 ≼ ω ∧ ∀𝑣 ∈ (𝑗 ↾t 𝑢)(𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣))))) → ∀𝑣 ∈ (𝑗 ↾t 𝑢)(𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣))) |
47 | 46 | adantr 480 |
. . . . . . . . . . . . 13
⊢
((((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
(𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢) ∧ (𝑡 ≼ ω ∧ ∀𝑣 ∈ (𝑗 ↾t 𝑢)(𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣))))) ∧ (𝑧 ∈ 𝑗 ∧ 𝑥 ∈ 𝑧)) → ∀𝑣 ∈ (𝑗 ↾t 𝑢)(𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣))) |
48 | | simprr 792 |
. . . . . . . . . . . . . 14
⊢
((((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
(𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢) ∧ (𝑡 ≼ ω ∧ ∀𝑣 ∈ (𝑗 ↾t 𝑢)(𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣))))) ∧ (𝑧 ∈ 𝑗 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ 𝑧) |
49 | 3 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢
((((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
(𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢) ∧ (𝑡 ≼ ω ∧ ∀𝑣 ∈ (𝑗 ↾t 𝑢)(𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣))))) ∧ (𝑧 ∈ 𝑗 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ 𝑢) |
50 | 48, 49 | elind 3760 |
. . . . . . . . . . . . 13
⊢
((((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
(𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢) ∧ (𝑡 ≼ ω ∧ ∀𝑣 ∈ (𝑗 ↾t 𝑢)(𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣))))) ∧ (𝑧 ∈ 𝑗 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ (𝑧 ∩ 𝑢)) |
51 | | eleq2 2677 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = (𝑧 ∩ 𝑢) → (𝑥 ∈ 𝑣 ↔ 𝑥 ∈ (𝑧 ∩ 𝑢))) |
52 | | sseq2 3590 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = (𝑧 ∩ 𝑢) → (𝑛 ⊆ 𝑣 ↔ 𝑛 ⊆ (𝑧 ∩ 𝑢))) |
53 | 52 | anbi2d 736 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = (𝑧 ∩ 𝑢) → ((𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣) ↔ (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ (𝑧 ∩ 𝑢)))) |
54 | 53 | rexbidv 3034 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = (𝑧 ∩ 𝑢) → (∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣) ↔ ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ (𝑧 ∩ 𝑢)))) |
55 | 51, 54 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = (𝑧 ∩ 𝑢) → ((𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣)) ↔ (𝑥 ∈ (𝑧 ∩ 𝑢) → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ (𝑧 ∩ 𝑢))))) |
56 | 55 | rspcv 3278 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∩ 𝑢) ∈ (𝑗 ↾t 𝑢) → (∀𝑣 ∈ (𝑗 ↾t 𝑢)(𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣)) → (𝑥 ∈ (𝑧 ∩ 𝑢) → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ (𝑧 ∩ 𝑢))))) |
57 | 45, 47, 50, 56 | syl3c 64 |
. . . . . . . . . . . 12
⊢
((((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
(𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢) ∧ (𝑡 ≼ ω ∧ ∀𝑣 ∈ (𝑗 ↾t 𝑢)(𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣))))) ∧ (𝑧 ∈ 𝑗 ∧ 𝑥 ∈ 𝑧)) → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ (𝑧 ∩ 𝑢))) |
58 | 3 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢)) ∧ 𝑛 ∈ 𝑡) → 𝑥 ∈ 𝑢) |
59 | | elin 3758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (𝑛 ∩ 𝑢) ↔ (𝑥 ∈ 𝑛 ∧ 𝑥 ∈ 𝑢)) |
60 | 59 | simplbi2com 655 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝑢 → (𝑥 ∈ 𝑛 → 𝑥 ∈ (𝑛 ∩ 𝑢))) |
61 | 58, 60 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢)) ∧ 𝑛 ∈ 𝑡) → (𝑥 ∈ 𝑛 → 𝑥 ∈ (𝑛 ∩ 𝑢))) |
62 | 22 | biantrud 527 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢)) ∧ 𝑛 ∈ 𝑡) → (𝑛 ⊆ 𝑧 ↔ (𝑛 ⊆ 𝑧 ∧ 𝑛 ⊆ 𝑢))) |
63 | | ssin 3797 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ⊆ 𝑧 ∧ 𝑛 ⊆ 𝑢) ↔ 𝑛 ⊆ (𝑧 ∩ 𝑢)) |
64 | 62, 63 | syl6bb 275 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢)) ∧ 𝑛 ∈ 𝑡) → (𝑛 ⊆ 𝑧 ↔ 𝑛 ⊆ (𝑧 ∩ 𝑢))) |
65 | | ssinss1 3803 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ⊆ 𝑧 → (𝑛 ∩ 𝑢) ⊆ 𝑧) |
66 | 64, 65 | syl6bir 243 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢)) ∧ 𝑛 ∈ 𝑡) → (𝑛 ⊆ (𝑧 ∩ 𝑢) → (𝑛 ∩ 𝑢) ⊆ 𝑧)) |
67 | 61, 66 | anim12d 584 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢)) ∧ 𝑛 ∈ 𝑡) → ((𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ (𝑧 ∩ 𝑢)) → (𝑥 ∈ (𝑛 ∩ 𝑢) ∧ (𝑛 ∩ 𝑢) ⊆ 𝑧))) |
68 | 67 | reximdva 3000 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢)) → (∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ (𝑧 ∩ 𝑢)) → ∃𝑛 ∈ 𝑡 (𝑥 ∈ (𝑛 ∩ 𝑢) ∧ (𝑛 ∩ 𝑢) ⊆ 𝑧))) |
69 | | vex 3176 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑛 ∈ V |
70 | 69 | inex1 4727 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∩ 𝑢) ∈ V |
71 | 70 | rgenw 2908 |
. . . . . . . . . . . . . . . 16
⊢
∀𝑛 ∈
𝑡 (𝑛 ∩ 𝑢) ∈ V |
72 | | eleq2 2677 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = (𝑛 ∩ 𝑢) → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ (𝑛 ∩ 𝑢))) |
73 | | sseq1 3589 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = (𝑛 ∩ 𝑢) → (𝑤 ⊆ 𝑧 ↔ (𝑛 ∩ 𝑢) ⊆ 𝑧)) |
74 | 72, 73 | anbi12d 743 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = (𝑛 ∩ 𝑢) → ((𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ (𝑥 ∈ (𝑛 ∩ 𝑢) ∧ (𝑛 ∩ 𝑢) ⊆ 𝑧))) |
75 | 29, 74 | rexrnmpt 6277 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑛 ∈
𝑡 (𝑛 ∩ 𝑢) ∈ V → (∃𝑤 ∈ ran (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢))(𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑛 ∈ 𝑡 (𝑥 ∈ (𝑛 ∩ 𝑢) ∧ (𝑛 ∩ 𝑢) ⊆ 𝑧))) |
76 | 71, 75 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑤 ∈ ran
(𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢))(𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑛 ∈ 𝑡 (𝑥 ∈ (𝑛 ∩ 𝑢) ∧ (𝑛 ∩ 𝑢) ⊆ 𝑧)) |
77 | 68, 76 | syl6ibr 241 |
. . . . . . . . . . . . . 14
⊢
(((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢)) → (∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ (𝑧 ∩ 𝑢)) → ∃𝑤 ∈ ran (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢))(𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
78 | 77 | adantrr 749 |
. . . . . . . . . . . . 13
⊢
(((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
(𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢) ∧ (𝑡 ≼ ω ∧ ∀𝑣 ∈ (𝑗 ↾t 𝑢)(𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣))))) → (∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ (𝑧 ∩ 𝑢)) → ∃𝑤 ∈ ran (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢))(𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
79 | 78 | adantr 480 |
. . . . . . . . . . . 12
⊢
((((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
(𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢) ∧ (𝑡 ≼ ω ∧ ∀𝑣 ∈ (𝑗 ↾t 𝑢)(𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣))))) ∧ (𝑧 ∈ 𝑗 ∧ 𝑥 ∈ 𝑧)) → (∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ (𝑧 ∩ 𝑢)) → ∃𝑤 ∈ ran (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢))(𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
80 | 57, 79 | mpd 15 |
. . . . . . . . . . 11
⊢
((((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
(𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢) ∧ (𝑡 ≼ ω ∧ ∀𝑣 ∈ (𝑗 ↾t 𝑢)(𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣))))) ∧ (𝑧 ∈ 𝑗 ∧ 𝑥 ∈ 𝑧)) → ∃𝑤 ∈ ran (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢))(𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) |
81 | 80 | expr 641 |
. . . . . . . . . 10
⊢
((((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
(𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢) ∧ (𝑡 ≼ ω ∧ ∀𝑣 ∈ (𝑗 ↾t 𝑢)(𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣))))) ∧ 𝑧 ∈ 𝑗) → (𝑥 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢))(𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
82 | 81 | ralrimiva 2949 |
. . . . . . . . 9
⊢
(((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
(𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢) ∧ (𝑡 ≼ ω ∧ ∀𝑣 ∈ (𝑗 ↾t 𝑢)(𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣))))) → ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢))(𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
83 | | breq1 4586 |
. . . . . . . . . . 11
⊢ (𝑦 = ran (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢)) → (𝑦 ≼ ω ↔ ran (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢)) ≼ ω)) |
84 | | rexeq 3116 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ran (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢)) → (∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑤 ∈ ran (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢))(𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
85 | 84 | imbi2d 329 |
. . . . . . . . . . . 12
⊢ (𝑦 = ran (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢)) → ((𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ (𝑥 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢))(𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
86 | 85 | ralbidv 2969 |
. . . . . . . . . . 11
⊢ (𝑦 = ran (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢)) → (∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢))(𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
87 | 83, 86 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝑦 = ran (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢)) → ((𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ (ran (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢)) ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢))(𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
88 | 87 | rspcev 3282 |
. . . . . . . . 9
⊢ ((ran
(𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢)) ∈ 𝒫 𝑗 ∧ (ran (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢)) ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑎 ∈ 𝑡 ↦ (𝑎 ∩ 𝑢))(𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) → ∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
89 | 36, 39, 82, 88 | syl12anc 1316 |
. . . . . . . 8
⊢
(((((𝑗 ∈
Locally 1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) ∧
(𝑡 ∈ 𝒫 (𝑗 ↾t 𝑢) ∧ (𝑡 ≼ ω ∧ ∀𝑣 ∈ (𝑗 ↾t 𝑢)(𝑥 ∈ 𝑣 → ∃𝑛 ∈ 𝑡 (𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣))))) → ∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
90 | 13, 89 | rexlimddv 3017 |
. . . . . . 7
⊢ ((((𝑗 ∈ Locally
1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) →
∃𝑦 ∈ 𝒫
𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
91 | 90 | 3adantr1 1213 |
. . . . . 6
⊢ ((((𝑗 ∈ Locally
1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) ∧ 𝑢 ∈ 𝑗) ∧ (𝑢 ⊆ ∪ 𝑗 ∧ 𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 1st𝜔)) →
∃𝑦 ∈ 𝒫
𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
92 | | simpl 472 |
. . . . . . 7
⊢ ((𝑗 ∈ Locally
1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) → 𝑗 ∈ Locally
1st𝜔) |
93 | 1 | adantr 480 |
. . . . . . . 8
⊢ ((𝑗 ∈ Locally
1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) → 𝑗 ∈ Top) |
94 | 7 | topopn 20536 |
. . . . . . . 8
⊢ (𝑗 ∈ Top → ∪ 𝑗
∈ 𝑗) |
95 | 93, 94 | syl 17 |
. . . . . . 7
⊢ ((𝑗 ∈ Locally
1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) → ∪ 𝑗
∈ 𝑗) |
96 | | simpr 476 |
. . . . . . 7
⊢ ((𝑗 ∈ Locally
1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) → 𝑥 ∈ ∪ 𝑗) |
97 | | llyi 21087 |
. . . . . . 7
⊢ ((𝑗 ∈ Locally
1st𝜔 ∧ ∪ 𝑗 ∈ 𝑗 ∧ 𝑥 ∈ ∪ 𝑗) → ∃𝑢 ∈ 𝑗 (𝑢 ⊆ ∪ 𝑗 ∧ 𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈
1st𝜔)) |
98 | 92, 95, 96, 97 | syl3anc 1318 |
. . . . . 6
⊢ ((𝑗 ∈ Locally
1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) → ∃𝑢 ∈ 𝑗 (𝑢 ⊆ ∪ 𝑗 ∧ 𝑥 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈
1st𝜔)) |
99 | 91, 98 | r19.29a 3060 |
. . . . 5
⊢ ((𝑗 ∈ Locally
1st𝜔 ∧ 𝑥 ∈ ∪ 𝑗) → ∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
100 | 99 | ralrimiva 2949 |
. . . 4
⊢ (𝑗 ∈ Locally
1st𝜔 → ∀𝑥 ∈ ∪ 𝑗∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
101 | 7 | is1stc2 21055 |
. . . 4
⊢ (𝑗 ∈ 1st𝜔
↔ (𝑗 ∈ Top ∧
∀𝑥 ∈ ∪ 𝑗∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
102 | 1, 100, 101 | sylanbrc 695 |
. . 3
⊢ (𝑗 ∈ Locally
1st𝜔 → 𝑗 ∈
1st𝜔) |
103 | 102 | ssriv 3572 |
. 2
⊢ Locally
1st𝜔 ⊆ 1st𝜔 |
104 | | 1stcrest 21066 |
. . . . 5
⊢ ((𝑗 ∈ 1st𝜔
∧ 𝑥 ∈ 𝑗) → (𝑗 ↾t 𝑥) ∈
1st𝜔) |
105 | 104 | adantl 481 |
. . . 4
⊢
((⊤ ∧ (𝑗
∈ 1st𝜔 ∧ 𝑥 ∈ 𝑗)) → (𝑗 ↾t 𝑥) ∈
1st𝜔) |
106 | | 1stctop 21056 |
. . . . . 6
⊢ (𝑗 ∈ 1st𝜔
→ 𝑗 ∈
Top) |
107 | 106 | ssriv 3572 |
. . . . 5
⊢
1st𝜔 ⊆ Top |
108 | 107 | a1i 11 |
. . . 4
⊢ (⊤
→ 1st𝜔 ⊆ Top) |
109 | 105, 108 | restlly 21096 |
. . 3
⊢ (⊤
→ 1st𝜔 ⊆ Locally
1st𝜔) |
110 | 109 | trud 1484 |
. 2
⊢
1st𝜔 ⊆ Locally
1st𝜔 |
111 | 103, 110 | eqssi 3584 |
1
⊢ Locally
1st𝜔 = 1st𝜔 |