Step | Hyp | Ref
| Expression |
1 | | pibt2.x |
. . . 4
⊢ 𝑋 = ∪
𝐽 |
2 | | pibt2.19 |
. . . 4
⊢ 𝐶 = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥((∪
𝑥 = ∪ 𝑦
∧ 𝑦 ≼ ω)
→ ∃𝑧 ∈
(𝒫 𝑦 ∩
Fin)∪ 𝑥 = ∪ 𝑧)} |
3 | 1, 2 | pibp19 35322 |
. . 3
⊢ (𝐽 ∈ 𝐶 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))) |
4 | 3 | simplbi 501 |
. 2
⊢ (𝐽 ∈ 𝐶 → 𝐽 ∈ Top) |
5 | | eldif 3876 |
. . . . 5
⊢ (𝑏 ∈ (𝒫 𝑋 ∖ Fin) ↔ (𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin)) |
6 | | velpw 4518 |
. . . . . . 7
⊢ (𝑏 ∈ 𝒫 𝑋 ↔ 𝑏 ⊆ 𝑋) |
7 | 6 | anbi1i 627 |
. . . . . 6
⊢ ((𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin) ↔ (𝑏 ⊆ 𝑋 ∧ ¬ 𝑏 ∈ Fin)) |
8 | | vex 3412 |
. . . . . . . . . 10
⊢ 𝑏 ∈ V |
9 | | infinf 10180 |
. . . . . . . . . 10
⊢ (𝑏 ∈ V → (¬ 𝑏 ∈ Fin ↔ ω
≼ 𝑏)) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . . 9
⊢ (¬
𝑏 ∈ Fin ↔ ω
≼ 𝑏) |
11 | 8 | infcntss 8945 |
. . . . . . . . 9
⊢ (ω
≼ 𝑏 →
∃𝑎(𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω)) |
12 | 10, 11 | sylbi 220 |
. . . . . . . 8
⊢ (¬
𝑏 ∈ Fin →
∃𝑎(𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω)) |
13 | 12 | ad2antll 729 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝐶 ∧ (𝑏 ⊆ 𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑎(𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω)) |
14 | | sstr 3909 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) → 𝑎 ⊆ 𝑋) |
15 | 14 | ancoms 462 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏) → 𝑎 ⊆ 𝑋) |
16 | | simplr 769 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → 𝑎 ≈ ω) |
17 | | simpll 767 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω)) |
18 | | 0ss 4311 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ∅
⊆ 𝑎 |
19 | | sseq1 3926 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((limPt‘𝐽)‘𝑎) = ∅ → (((limPt‘𝐽)‘𝑎) ⊆ 𝑎 ↔ ∅ ⊆ 𝑎)) |
20 | 18, 19 | mpbiri 261 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((limPt‘𝐽)‘𝑎) = ∅ → ((limPt‘𝐽)‘𝑎) ⊆ 𝑎) |
21 | 20 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑎) |
22 | 1 | cldlp 22047 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) → (𝑎 ∈ (Clsd‘𝐽) ↔ ((limPt‘𝐽)‘𝑎) ⊆ 𝑎)) |
23 | 22 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (𝑎 ∈ (Clsd‘𝐽) ↔ ((limPt‘𝐽)‘𝑎) ⊆ 𝑎)) |
24 | 21, 23 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽)) |
25 | 4, 24 | sylanl1 680 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽)) |
26 | 25 | adantllr 719 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽)) |
27 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ((limPt‘𝐽)‘𝑎) = ∅) |
28 | 1 | cldss 21926 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 ∈ (Clsd‘𝐽) → 𝑎 ⊆ 𝑋) |
29 | 1 | nlpineqsn 35316 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∀𝑝 ∈ 𝑎 ∃𝑛 ∈ 𝐽 (𝑝 ∈ 𝑛 ∧ (𝑛 ∩ 𝑎) = {𝑝})) |
30 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑝 ∈ 𝑛 ∧ (𝑛 ∩ 𝑎) = {𝑝}) → (𝑛 ∩ 𝑎) = {𝑝}) |
31 | 30 | reximi 3166 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∃𝑛 ∈
𝐽 (𝑝 ∈ 𝑛 ∧ (𝑛 ∩ 𝑎) = {𝑝}) → ∃𝑛 ∈ 𝐽 (𝑛 ∩ 𝑎) = {𝑝}) |
32 | 31 | ralimi 3083 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∀𝑝 ∈
𝑎 ∃𝑛 ∈ 𝐽 (𝑝 ∈ 𝑛 ∧ (𝑛 ∩ 𝑎) = {𝑝}) → ∀𝑝 ∈ 𝑎 ∃𝑛 ∈ 𝐽 (𝑛 ∩ 𝑎) = {𝑝}) |
33 | | vex 3412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 𝑎 ∈ V |
34 | | ineq1 4120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑛 = (𝑓‘𝑝) → (𝑛 ∩ 𝑎) = ((𝑓‘𝑝) ∩ 𝑎)) |
35 | 34 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 = (𝑓‘𝑝) → ((𝑛 ∩ 𝑎) = {𝑝} ↔ ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) |
36 | 33, 35 | ac6s 10098 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∀𝑝 ∈
𝑎 ∃𝑛 ∈ 𝐽 (𝑛 ∩ 𝑎) = {𝑝} → ∃𝑓(𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) |
37 | 29, 32, 36 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) |
38 | | fvineqsnf1 35318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → 𝑓:𝑎–1-1→𝐽) |
39 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) |
40 | 38, 39 | jca 515 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) |
41 | 40 | eximi 1842 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(∃𝑓(𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) |
42 | 37, 41 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) |
43 | 28, 42 | syl3an2 1166 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) |
44 | 4, 43 | syl3an1 1165 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐽 ∈ 𝐶 ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) |
45 | 44 | 3adant1r 1179 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) |
46 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎–1-1→𝐽) → 𝑓:𝑎–1-1→𝐽) |
47 | | vsnid 4578 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ 𝑝 ∈ {𝑝} |
48 | | eleq2 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → (𝑝 ∈ ((𝑓‘𝑝) ∩ 𝑎) ↔ 𝑝 ∈ {𝑝})) |
49 | 47, 48 | mpbiri 261 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → 𝑝 ∈ ((𝑓‘𝑝) ∩ 𝑎)) |
50 | 49 | elin1d 4112 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → 𝑝 ∈ (𝑓‘𝑝)) |
51 | 50 | ralimi 3083 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(∀𝑝 ∈
𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → ∀𝑝 ∈ 𝑎 𝑝 ∈ (𝑓‘𝑝)) |
52 | | ralssiun 35315 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(∀𝑝 ∈
𝑎 𝑝 ∈ (𝑓‘𝑝) → 𝑎 ⊆ ∪
𝑝 ∈ 𝑎 (𝑓‘𝑝)) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(∀𝑝 ∈
𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → 𝑎 ⊆ ∪
𝑝 ∈ 𝑎 (𝑓‘𝑝)) |
54 | 53 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → 𝑎 ⊆ ∪
𝑝 ∈ 𝑎 (𝑓‘𝑝)) |
55 | | f1fn 6616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑓:𝑎–1-1→𝐽 → 𝑓 Fn 𝑎) |
56 | | fniunfv 7060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑓 Fn 𝑎 → ∪
𝑝 ∈ 𝑎 (𝑓‘𝑝) = ∪ ran 𝑓) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑓:𝑎–1-1→𝐽 → ∪
𝑝 ∈ 𝑎 (𝑓‘𝑝) = ∪ ran 𝑓) |
58 | 57 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∪
𝑝 ∈ 𝑎 (𝑓‘𝑝) = ∪ ran 𝑓) |
59 | 54, 58 | sseqtrd 3941 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → 𝑎 ⊆ ∪ ran
𝑓) |
60 | 1 | cldopn 21928 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑎 ∈ (Clsd‘𝐽) → (𝑋 ∖ 𝑎) ∈ 𝐽) |
61 | 60 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → (𝑋 ∖ 𝑎) ∈ 𝐽) |
62 | 61 | anim1i 618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ⊆ ∪ ran
𝑓) → ((𝑋 ∖ 𝑎) ∈ 𝐽 ∧ 𝑎 ⊆ ∪ ran
𝑓)) |
63 | 62 | ancomd 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ⊆ ∪ ran
𝑓) → (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽)) |
64 | 28 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → 𝑎 ⊆ 𝑋) |
65 | 64 | anim1i 618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ⊆ ∪ ran
𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽)) → (𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran
𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽))) |
66 | | unisng 4840 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑋 ∖ 𝑎) ∈ 𝐽 → ∪ {(𝑋 ∖ 𝑎)} = (𝑋 ∖ 𝑎)) |
67 | 66 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑋 ∖ 𝑎) ∈ 𝐽 → (𝑋 ∖ 𝑎) = ∪ {(𝑋 ∖ 𝑎)}) |
68 | | eqimss 3957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑋 ∖ 𝑎) = ∪ {(𝑋 ∖ 𝑎)} → (𝑋 ∖ 𝑎) ⊆ ∪
{(𝑋 ∖ 𝑎)}) |
69 | | ssun4 4089 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑋 ∖ 𝑎) ⊆ ∪
{(𝑋 ∖ 𝑎)} → (𝑋 ∖ 𝑎) ⊆ (∪ ran
𝑓 ∪ ∪ {(𝑋
∖ 𝑎)})) |
70 | | uniun 4844 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) = (∪ ran 𝑓 ∪ ∪ {(𝑋
∖ 𝑎)}) |
71 | 69, 70 | sseqtrrdi 3952 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑋 ∖ 𝑎) ⊆ ∪
{(𝑋 ∖ 𝑎)} → (𝑋 ∖ 𝑎) ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
72 | 67, 68, 71 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑋 ∖ 𝑎) ∈ 𝐽 → (𝑋 ∖ 𝑎) ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
73 | | ssun3 4088 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑎 ⊆ ∪ ran 𝑓 → 𝑎 ⊆ (∪ ran
𝑓 ∪ ∪ {(𝑋
∖ 𝑎)})) |
74 | 73, 70 | sseqtrrdi 3952 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑎 ⊆ ∪ ran 𝑓 → 𝑎 ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
75 | | uncom 4067 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝑎 ∪ (𝑋 ∖ 𝑎)) = ((𝑋 ∖ 𝑎) ∪ 𝑎) |
76 | | undif1 4390 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝑋 ∖ 𝑎) ∪ 𝑎) = (𝑋 ∪ 𝑎) |
77 | 75, 76 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝑎 ∪ (𝑋 ∖ 𝑎)) = (𝑋 ∪ 𝑎) |
78 | | ssequn2 4097 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝑎 ⊆ 𝑋 ↔ (𝑋 ∪ 𝑎) = 𝑋) |
79 | 78 | biimpi 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝑎 ⊆ 𝑋 → (𝑋 ∪ 𝑎) = 𝑋) |
80 | 77, 79 | syl5eq 2790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝑎 ⊆ 𝑋 → (𝑎 ∪ (𝑋 ∖ 𝑎)) = 𝑋) |
81 | 80 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}))) → (𝑎 ∪ (𝑋 ∖ 𝑎)) = 𝑋) |
82 | | unss12 4096 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑎 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)})) → (𝑎 ∪ (𝑋 ∖ 𝑎)) ⊆ (∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∪ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}))) |
83 | | unidm 4066 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∪ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)})) = ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}) |
84 | 82, 83 | sseqtrdi 3951 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑎 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)})) → (𝑎 ∪ (𝑋 ∖ 𝑎)) ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
85 | 84 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}))) → (𝑎 ∪ (𝑋 ∖ 𝑎)) ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
86 | 81, 85 | eqsstrrd 3940 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}))) → 𝑋 ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
87 | 74, 86 | sylanr1 682 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran
𝑓 ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}))) → 𝑋 ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
88 | 72, 87 | sylanr2 683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran
𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽)) → 𝑋 ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
89 | 88 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran
𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽))) → 𝑋 ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
90 | | f1f 6615 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑓:𝑎–1-1→𝐽 → 𝑓:𝑎⟶𝐽) |
91 | | frn 6552 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑓:𝑎⟶𝐽 → ran 𝑓 ⊆ 𝐽) |
92 | 90, 91 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑓:𝑎–1-1→𝐽 → ran 𝑓 ⊆ 𝐽) |
93 | 1 | topopn 21803 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽) |
94 | 1 | difopn 21931 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑋 ∈ 𝐽 ∧ 𝑎 ∈ (Clsd‘𝐽)) → (𝑋 ∖ 𝑎) ∈ 𝐽) |
95 | 93, 94 | sylan 583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) → (𝑋 ∖ 𝑎) ∈ 𝐽) |
96 | 95 | snssd 4722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) → {(𝑋 ∖ 𝑎)} ⊆ 𝐽) |
97 | | unss12 4096 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((ran
𝑓 ⊆ 𝐽 ∧ {(𝑋 ∖ 𝑎)} ⊆ 𝐽) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ (𝐽 ∪ 𝐽)) |
98 | | unidm 4066 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝐽 ∪ 𝐽) = 𝐽 |
99 | 97, 98 | sseqtrdi 3951 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((ran
𝑓 ⊆ 𝐽 ∧ {(𝑋 ∖ 𝑎)} ⊆ 𝐽) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽) |
100 | 92, 96, 99 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽) |
101 | | uniss 4827 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽 → ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ ∪
𝐽) |
102 | 101, 1 | sseqtrrdi 3952 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽 → ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝑋) |
103 | 100, 102 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝑋) |
104 | 103 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran
𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽))) → ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝑋) |
105 | 89, 104 | eqssd 3918 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran
𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽))) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
106 | 65, 105 | syldan 594 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ⊆ ∪ ran
𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽)) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
107 | 63, 106 | syldan 594 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ⊆ ∪ ran
𝑓) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
108 | 59, 107 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
109 | 108 | ancom1s 653 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎–1-1→𝐽) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
110 | 109 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎–1-1→𝐽) → ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))) |
111 | 46, 110 | mpand 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎–1-1→𝐽) → (∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))) |
112 | 111 | impr 458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
113 | 112 | adantlrr 721 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
114 | 4, 113 | sylanl1 680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
115 | | vex 3412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 𝑓 ∈ V |
116 | | f1f1orn 6672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑓:𝑎–1-1→𝐽 → 𝑓:𝑎–1-1-onto→ran
𝑓) |
117 | | f1oen3g 8644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑓 ∈ V ∧ 𝑓:𝑎–1-1-onto→ran
𝑓) → 𝑎 ≈ ran 𝑓) |
118 | 115, 116,
117 | sylancr 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑓:𝑎–1-1→𝐽 → 𝑎 ≈ ran 𝑓) |
119 | | enen1 8786 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑎 ≈ ran 𝑓 → (𝑎 ≈ ω ↔ ran 𝑓 ≈
ω)) |
120 | | endom 8655 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (ran
𝑓 ≈ ω →
ran 𝑓 ≼
ω) |
121 | | snfi 8721 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ {(𝑋 ∖ 𝑎)} ∈ Fin |
122 | | isfinite 9267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ({(𝑋 ∖ 𝑎)} ∈ Fin ↔ {(𝑋 ∖ 𝑎)} ≺ ω) |
123 | 121, 122 | mpbi 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ {(𝑋 ∖ 𝑎)} ≺ ω |
124 | | sdomdom 8656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ({(𝑋 ∖ 𝑎)} ≺ ω → {(𝑋 ∖ 𝑎)} ≼ ω) |
125 | 123, 124 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ {(𝑋 ∖ 𝑎)} ≼ ω |
126 | | unctb 9819 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((ran
𝑓 ≼ ω ∧
{(𝑋 ∖ 𝑎)} ≼ ω) → (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) |
127 | 120, 125,
126 | sylancl 589 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (ran
𝑓 ≈ ω →
(ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) |
128 | 119, 127 | syl6bi 256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑎 ≈ ran 𝑓 → (𝑎 ≈ ω → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω)) |
129 | 118, 128 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑓:𝑎–1-1→𝐽 → (𝑎 ≈ ω → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω)) |
130 | 129 | impcom 411 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑎 ≈ ω ∧ 𝑓:𝑎–1-1→𝐽) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) |
131 | 130 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω) ∧ 𝑓:𝑎–1-1→𝐽) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) |
132 | 131 | ad2ant2lr 748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) |
133 | 100 | ancoms 462 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎–1-1→𝐽) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽) |
134 | 133 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽) |
135 | 134 | adantlrr 721 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽) |
136 | 4, 135 | sylanl1 680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽) |
137 | | elpw2g 5237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝐽 ∈ 𝐶 → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽 ↔ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽)) |
138 | 137 | biimprd 251 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐽 ∈ 𝐶 → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽 → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽)) |
139 | 138 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽 → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽)) |
140 | 136, 139 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽) |
141 | 3 | simprbi 500 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝐽 ∈ 𝐶 → ∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)) |
142 | | unieq 4830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑠 = 𝑧 → ∪ 𝑠 = ∪
𝑧) |
143 | 142 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑠 = 𝑧 → (𝑋 = ∪ 𝑠 ↔ 𝑋 = ∪ 𝑧)) |
144 | 143 | cbvrexvw 3359 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(∃𝑠 ∈
(𝒫 𝑦 ∩
Fin)𝑋 = ∪ 𝑠
↔ ∃𝑧 ∈
(𝒫 𝑦 ∩
Fin)𝑋 = ∪ 𝑧) |
145 | 144 | imbi2i 339 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑋 = ∪
𝑦 ∧ 𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠) ↔ ((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)) |
146 | 145 | ralbii 3088 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(∀𝑦 ∈
𝒫 𝐽((𝑋 = ∪
𝑦 ∧ 𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠) ↔ ∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)) |
147 | 141, 146 | sylibr 237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐽 ∈ 𝐶 → ∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠)) |
148 | | unieq 4830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → ∪ 𝑦 = ∪
(ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
149 | 148 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑋 = ∪ 𝑦 ↔ 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))) |
150 | | breq1 5056 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑦 ≼ ω ↔ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω)) |
151 | 149, 150 | anbi12d 634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → ((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) ↔ (𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω))) |
152 | | pweq 4529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → 𝒫 𝑦 = 𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
153 | 152 | ineq1d 4126 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝒫 𝑦 ∩ Fin) = (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)) |
154 | 153 | rexeqdv 3326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠 ↔ ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠)) |
155 | 151, 154 | imbi12d 348 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠) ↔ ((𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠))) |
156 | 155 | rspccv 3534 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∀𝑦 ∈
𝒫 𝐽((𝑋 = ∪
𝑦 ∧ 𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠) → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠))) |
157 | 147, 156 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐽 ∈ 𝐶 → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠))) |
158 | 157 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠))) |
159 | 140, 158 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠)) |
160 | 114, 132,
159 | mp2and 699 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠) |
161 | | df-rex 3067 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∃𝑠 ∈
(𝒫 (ran 𝑓 ∪
{(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠 ↔ ∃𝑠(𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠)) |
162 | | elinel1 4109 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) → 𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
163 | | velpw 4518 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ↔ 𝑠 ⊆ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
164 | | ssdif 4054 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∖ {(𝑋 ∖ 𝑎)})) |
165 | | difun2 4395 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∖ {(𝑋 ∖ 𝑎)}) = (ran 𝑓 ∖ {(𝑋 ∖ 𝑎)}) |
166 | 164, 165 | sseqtrdi 3951 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ (ran 𝑓 ∖ {(𝑋 ∖ 𝑎)})) |
167 | 166 | difss2d 4049 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓) |
168 | 163, 167 | sylbi 220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓) |
169 | 162, 168 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓) |
170 | 169 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) → (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓)) |
171 | | sseq2 3927 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑋 = ∪
𝑠 → (𝑎 ⊆ 𝑋 ↔ 𝑎 ⊆ ∪ 𝑠)) |
172 | | uniexg 7528 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝐽 ∈ Top → ∪ 𝐽
∈ V) |
173 | 1, 172 | eqeltrid 2842 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝐽 ∈ Top → 𝑋 ∈ V) |
174 | | difexg 5220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝑋 ∈ V → (𝑋 ∖ 𝑎) ∈ V) |
175 | | unisng 4840 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑋 ∖ 𝑎) ∈ V → ∪ {(𝑋
∖ 𝑎)} = (𝑋 ∖ 𝑎)) |
176 | 173, 174,
175 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝐽 ∈ Top → ∪ {(𝑋
∖ 𝑎)} = (𝑋 ∖ 𝑎)) |
177 | 176 | ineq2d 4127 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝐽 ∈ Top → (𝑎 ∩ ∪ {(𝑋
∖ 𝑎)}) = (𝑎 ∩ (𝑋 ∖ 𝑎))) |
178 | | disjdif 4386 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑎 ∩ (𝑋 ∖ 𝑎)) = ∅ |
179 | 177, 178 | eqtrdi 2794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝐽 ∈ Top → (𝑎 ∩ ∪ {(𝑋
∖ 𝑎)}) =
∅) |
180 | | inunissunidif 35283 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑎 ∩ ∪ {(𝑋
∖ 𝑎)}) = ∅
→ (𝑎 ⊆ ∪ 𝑠
↔ 𝑎 ⊆ ∪ (𝑠
∖ {(𝑋 ∖ 𝑎)}))) |
181 | 179, 180 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝐽 ∈ Top → (𝑎 ⊆ ∪ 𝑠
↔ 𝑎 ⊆ ∪ (𝑠
∖ {(𝑋 ∖ 𝑎)}))) |
182 | 171, 181 | sylan9bbr 514 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪
𝑠) → (𝑎 ⊆ 𝑋 ↔ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) |
183 | 182 | biimpd 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪
𝑠) → (𝑎 ⊆ 𝑋 → 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) |
184 | 183 | impancom 455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) → (𝑋 = ∪ 𝑠 → 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) |
185 | 170, 184 | anim12d 612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)})))) |
186 | 4, 28, 185 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐽 ∈ 𝐶 ∧ 𝑎 ∈ (Clsd‘𝐽)) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)})))) |
187 | 186 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)})))) |
188 | 187 | anim2d 615 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠)) → ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))))) |
189 | 118 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) → 𝑎 ≈ ran 𝑓) |
190 | | fvineqsneq 35320 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝑓 Fn 𝑎 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) = ran 𝑓) |
191 | 55, 190 | sylanl1 680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) = ran 𝑓) |
192 | | vex 3412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ 𝑠 ∈ V |
193 | | difss 4046 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ 𝑠 |
194 | | ssdomg 8674 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑠 ∈ V → ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ 𝑠 → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ≼ 𝑠)) |
195 | 192, 193,
194 | mp2 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ≼ 𝑠 |
196 | 191, 195 | eqbrtrrdi 5093 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) → ran 𝑓 ≼ 𝑠) |
197 | | endomtr 8686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑎 ≈ ran 𝑓 ∧ ran 𝑓 ≼ 𝑠) → 𝑎 ≼ 𝑠) |
198 | 189, 196,
197 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) → 𝑎 ≼ 𝑠) |
199 | 188, 198 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠)) → 𝑎 ≼ 𝑠)) |
200 | 199 | expdimp 456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → 𝑎 ≼ 𝑠)) |
201 | | elinel2 4110 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) → 𝑠 ∈ Fin) |
202 | 201 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → 𝑠 ∈ Fin) |
203 | 202 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → 𝑠 ∈ Fin)) |
204 | 200, 203 | jcad 516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → (𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin))) |
205 | 204 | eximdv 1925 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (∃𝑠(𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin))) |
206 | 161, 205 | syl5bi 245 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠 → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin))) |
207 | 160, 206 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)) |
208 | 207 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin))) |
209 | 208 | exlimdv 1941 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin))) |
210 | 209 | anass1rs 655 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽)) → (∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin))) |
211 | 210 | 3adant3 1134 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin))) |
212 | 45, 211 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)) |
213 | 17, 26, 27, 212 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)) |
214 | 213 | anasss 470 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)) |
215 | | isfinite 9267 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 ∈ Fin ↔ 𝑠 ≺
ω) |
216 | | domsdomtr 8781 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ≼ 𝑠 ∧ 𝑠 ≺ ω) → 𝑎 ≺ ω) |
217 | 215, 216 | sylan2b 597 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin) → 𝑎 ≺ ω) |
218 | 217 | exlimiv 1938 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin) → 𝑎 ≺ ω) |
219 | | sdomnen 8657 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ≺ ω → ¬
𝑎 ≈
ω) |
220 | 214, 218,
219 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → ¬ 𝑎 ≈ ω) |
221 | 16, 220 | pm2.65da 817 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) → ¬ (𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) |
222 | | imnan 403 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ⊆ 𝑋 → ¬ ((limPt‘𝐽)‘𝑎) = ∅) ↔ ¬ (𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) |
223 | 221, 222 | sylibr 237 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) → (𝑎 ⊆ 𝑋 → ¬ ((limPt‘𝐽)‘𝑎) = ∅)) |
224 | 223 | imp 410 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → ¬ ((limPt‘𝐽)‘𝑎) = ∅) |
225 | | neq0 4260 |
. . . . . . . . . . . . . . 15
⊢ (¬
((limPt‘𝐽)‘𝑎) = ∅ ↔ ∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎)) |
226 | 224, 225 | sylib 221 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → ∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎)) |
227 | 1 | lpss 22039 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋) |
228 | 4, 227 | sylan 583 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐽 ∈ 𝐶 ∧ 𝑎 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋) |
229 | 228 | adantlr 715 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋) |
230 | 229 | sseld 3900 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → 𝑠 ∈ 𝑋)) |
231 | 230 | ancrd 555 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → (𝑠 ∈ 𝑋 ∧ 𝑠 ∈ ((limPt‘𝐽)‘𝑎)))) |
232 | 231 | eximdv 1925 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → (∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠(𝑠 ∈ 𝑋 ∧ 𝑠 ∈ ((limPt‘𝐽)‘𝑎)))) |
233 | | df-rex 3067 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑠 ∈
𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎) ↔ ∃𝑠(𝑠 ∈ 𝑋 ∧ 𝑠 ∈ ((limPt‘𝐽)‘𝑎))) |
234 | 232, 233 | syl6ibr 255 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → (∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎))) |
235 | 226, 234 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎)) |
236 | 15, 235 | sylan2 596 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎)) |
237 | 1 | lpss3 22041 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐽 ∈ Top ∧ 𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏)) |
238 | 237 | 3expb 1122 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ Top ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏)) |
239 | 4, 238 | sylan 583 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ 𝐶 ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏)) |
240 | 239 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏)) |
241 | 240 | sseld 3900 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → 𝑠 ∈ ((limPt‘𝐽)‘𝑏))) |
242 | 241 | reximdv 3192 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → (∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))) |
243 | 236, 242 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)) |
244 | 243 | an42s 661 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)) |
245 | 244 | ex 416 |
. . . . . . . . 9
⊢ ((𝐽 ∈ 𝐶 ∧ 𝑏 ⊆ 𝑋) → ((𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))) |
246 | 245 | exlimdv 1941 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝐶 ∧ 𝑏 ⊆ 𝑋) → (∃𝑎(𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))) |
247 | 246 | adantrr 717 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝐶 ∧ (𝑏 ⊆ 𝑋 ∧ ¬ 𝑏 ∈ Fin)) → (∃𝑎(𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))) |
248 | 13, 247 | mpd 15 |
. . . . . 6
⊢ ((𝐽 ∈ 𝐶 ∧ (𝑏 ⊆ 𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)) |
249 | 7, 248 | sylan2b 597 |
. . . . 5
⊢ ((𝐽 ∈ 𝐶 ∧ (𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)) |
250 | 5, 249 | sylan2b 597 |
. . . 4
⊢ ((𝐽 ∈ 𝐶 ∧ 𝑏 ∈ (𝒫 𝑋 ∖ Fin)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)) |
251 | 250 | ralrimiva 3105 |
. . 3
⊢ (𝐽 ∈ 𝐶 → ∀𝑏 ∈ (𝒫 𝑋 ∖ Fin)∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)) |
252 | | simpr 488 |
. . . . . 6
⊢ ((𝑦 = 𝑏 ∧ 𝑧 = 𝑠) → 𝑧 = 𝑠) |
253 | | fveq2 6717 |
. . . . . . 7
⊢ (𝑦 = 𝑏 → ((limPt‘𝐽)‘𝑦) = ((limPt‘𝐽)‘𝑏)) |
254 | 253 | adantr 484 |
. . . . . 6
⊢ ((𝑦 = 𝑏 ∧ 𝑧 = 𝑠) → ((limPt‘𝐽)‘𝑦) = ((limPt‘𝐽)‘𝑏)) |
255 | 252, 254 | eleq12d 2832 |
. . . . 5
⊢ ((𝑦 = 𝑏 ∧ 𝑧 = 𝑠) → (𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ 𝑠 ∈ ((limPt‘𝐽)‘𝑏))) |
256 | 255 | cbvrexdva 3370 |
. . . 4
⊢ (𝑦 = 𝑏 → (∃𝑧 ∈ 𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))) |
257 | 256 | cbvralvw 3358 |
. . 3
⊢
(∀𝑦 ∈
(𝒫 𝑋 ∖
Fin)∃𝑧 ∈ 𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ ∀𝑏 ∈ (𝒫 𝑋 ∖ Fin)∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)) |
258 | 251, 257 | sylibr 237 |
. 2
⊢ (𝐽 ∈ 𝐶 → ∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧 ∈ 𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦)) |
259 | | pibt2.21 |
. . 3
⊢ 𝑊 = {𝑥 ∈ Top ∣ ∀𝑦 ∈ (𝒫 ∪ 𝑥
∖ Fin)∃𝑧 ∈
∪ 𝑥𝑧 ∈ ((limPt‘𝑥)‘𝑦)} |
260 | 1, 259 | pibp21 35323 |
. 2
⊢ (𝐽 ∈ 𝑊 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧 ∈ 𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦))) |
261 | 4, 258, 260 | sylanbrc 586 |
1
⊢ (𝐽 ∈ 𝐶 → 𝐽 ∈ 𝑊) |