Step | Hyp | Ref
| Expression |
1 | | pibt2.x |
. . . 4
⊢ 𝑋 = ∪
𝐽 |
2 | | pibt2.19 |
. . . 4
⊢ 𝐶 = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥((∪
𝑥 = ∪ 𝑦
∧ 𝑦 ≼ ω)
→ ∃𝑧 ∈
(𝒫 𝑦 ∩
Fin)∪ 𝑥 = ∪ 𝑧)} |
3 | 1, 2 | pibp19 37134 |
. . 3
⊢ (𝐽 ∈ 𝐶 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))) |
4 | 3 | simplbi 496 |
. 2
⊢ (𝐽 ∈ 𝐶 → 𝐽 ∈ Top) |
5 | | eldif 3956 |
. . . . 5
⊢ (𝑏 ∈ (𝒫 𝑋 ∖ Fin) ↔ (𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin)) |
6 | | velpw 4602 |
. . . . . . 7
⊢ (𝑏 ∈ 𝒫 𝑋 ↔ 𝑏 ⊆ 𝑋) |
7 | 6 | anbi1i 622 |
. . . . . 6
⊢ ((𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin) ↔ (𝑏 ⊆ 𝑋 ∧ ¬ 𝑏 ∈ Fin)) |
8 | | vex 3466 |
. . . . . . . . . 10
⊢ 𝑏 ∈ V |
9 | | infinf 10600 |
. . . . . . . . . 10
⊢ (𝑏 ∈ V → (¬ 𝑏 ∈ Fin ↔ ω
≼ 𝑏)) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . . 9
⊢ (¬
𝑏 ∈ Fin ↔ ω
≼ 𝑏) |
11 | 8 | infcntss 9357 |
. . . . . . . . 9
⊢ (ω
≼ 𝑏 →
∃𝑎(𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω)) |
12 | 10, 11 | sylbi 216 |
. . . . . . . 8
⊢ (¬
𝑏 ∈ Fin →
∃𝑎(𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω)) |
13 | 12 | ad2antll 727 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝐶 ∧ (𝑏 ⊆ 𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑎(𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω)) |
14 | | sstr 3987 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) → 𝑎 ⊆ 𝑋) |
15 | 14 | ancoms 457 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏) → 𝑎 ⊆ 𝑋) |
16 | | simplr 767 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → 𝑎 ≈ ω) |
17 | | simpll 765 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω)) |
18 | | 0ss 4394 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ∅
⊆ 𝑎 |
19 | | sseq1 4004 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((limPt‘𝐽)‘𝑎) = ∅ → (((limPt‘𝐽)‘𝑎) ⊆ 𝑎 ↔ ∅ ⊆ 𝑎)) |
20 | 18, 19 | mpbiri 257 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((limPt‘𝐽)‘𝑎) = ∅ → ((limPt‘𝐽)‘𝑎) ⊆ 𝑎) |
21 | 20 | adantl 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑎) |
22 | 1 | cldlp 23142 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) → (𝑎 ∈ (Clsd‘𝐽) ↔ ((limPt‘𝐽)‘𝑎) ⊆ 𝑎)) |
23 | 22 | adantr 479 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (𝑎 ∈ (Clsd‘𝐽) ↔ ((limPt‘𝐽)‘𝑎) ⊆ 𝑎)) |
24 | 21, 23 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽)) |
25 | 4, 24 | sylanl1 678 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽)) |
26 | 25 | adantllr 717 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽)) |
27 | | simpr 483 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ((limPt‘𝐽)‘𝑎) = ∅) |
28 | 1 | cldss 23021 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 ∈ (Clsd‘𝐽) → 𝑎 ⊆ 𝑋) |
29 | 1 | nlpineqsn 37128 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∀𝑝 ∈ 𝑎 ∃𝑛 ∈ 𝐽 (𝑝 ∈ 𝑛 ∧ (𝑛 ∩ 𝑎) = {𝑝})) |
30 | | simpr 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑝 ∈ 𝑛 ∧ (𝑛 ∩ 𝑎) = {𝑝}) → (𝑛 ∩ 𝑎) = {𝑝}) |
31 | 30 | reximi 3074 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∃𝑛 ∈
𝐽 (𝑝 ∈ 𝑛 ∧ (𝑛 ∩ 𝑎) = {𝑝}) → ∃𝑛 ∈ 𝐽 (𝑛 ∩ 𝑎) = {𝑝}) |
32 | 31 | ralimi 3073 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(∀𝑝 ∈
𝑎 ∃𝑛 ∈ 𝐽 (𝑝 ∈ 𝑛 ∧ (𝑛 ∩ 𝑎) = {𝑝}) → ∀𝑝 ∈ 𝑎 ∃𝑛 ∈ 𝐽 (𝑛 ∩ 𝑎) = {𝑝}) |
33 | | vex 3466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑎 ∈ V |
34 | | ineq1 4203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 = (𝑓‘𝑝) → (𝑛 ∩ 𝑎) = ((𝑓‘𝑝) ∩ 𝑎)) |
35 | 34 | eqeq1d 2728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 = (𝑓‘𝑝) → ((𝑛 ∩ 𝑎) = {𝑝} ↔ ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) |
36 | 33, 35 | ac6s 10518 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(∀𝑝 ∈
𝑎 ∃𝑛 ∈ 𝐽 (𝑛 ∩ 𝑎) = {𝑝} → ∃𝑓(𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) |
37 | | fvineqsnf1 37130 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → 𝑓:𝑎–1-1→𝐽) |
38 | | simpr 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) |
39 | 37, 38 | jca 510 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) |
40 | 39 | eximi 1830 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(∃𝑓(𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) |
41 | 29, 32, 36, 40 | 4syl 19 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) |
42 | 28, 41 | syl3an2 1161 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) |
43 | 4, 42 | syl3an1 1160 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐽 ∈ 𝐶 ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) |
44 | 43 | 3adant1r 1174 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) |
45 | | simpr 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎–1-1→𝐽) → 𝑓:𝑎–1-1→𝐽) |
46 | | vsnid 4660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ 𝑝 ∈ {𝑝} |
47 | | eleq2 2815 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → (𝑝 ∈ ((𝑓‘𝑝) ∩ 𝑎) ↔ 𝑝 ∈ {𝑝})) |
48 | 46, 47 | mpbiri 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → 𝑝 ∈ ((𝑓‘𝑝) ∩ 𝑎)) |
49 | 48 | elin1d 4196 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → 𝑝 ∈ (𝑓‘𝑝)) |
50 | 49 | ralimi 3073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(∀𝑝 ∈
𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → ∀𝑝 ∈ 𝑎 𝑝 ∈ (𝑓‘𝑝)) |
51 | | ralssiun 37127 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(∀𝑝 ∈
𝑎 𝑝 ∈ (𝑓‘𝑝) → 𝑎 ⊆ ∪
𝑝 ∈ 𝑎 (𝑓‘𝑝)) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(∀𝑝 ∈
𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → 𝑎 ⊆ ∪
𝑝 ∈ 𝑎 (𝑓‘𝑝)) |
53 | 52 | adantl 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → 𝑎 ⊆ ∪
𝑝 ∈ 𝑎 (𝑓‘𝑝)) |
54 | | f1fn 6791 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑓:𝑎–1-1→𝐽 → 𝑓 Fn 𝑎) |
55 | | fniunfv 7254 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑓 Fn 𝑎 → ∪
𝑝 ∈ 𝑎 (𝑓‘𝑝) = ∪ ran 𝑓) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑓:𝑎–1-1→𝐽 → ∪
𝑝 ∈ 𝑎 (𝑓‘𝑝) = ∪ ran 𝑓) |
57 | 56 | adantr 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∪
𝑝 ∈ 𝑎 (𝑓‘𝑝) = ∪ ran 𝑓) |
58 | 53, 57 | sseqtrd 4019 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → 𝑎 ⊆ ∪ ran
𝑓) |
59 | 1 | cldopn 23023 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑎 ∈ (Clsd‘𝐽) → (𝑋 ∖ 𝑎) ∈ 𝐽) |
60 | 59 | ad2antll 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → (𝑋 ∖ 𝑎) ∈ 𝐽) |
61 | 60 | anim1i 613 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ⊆ ∪ ran
𝑓) → ((𝑋 ∖ 𝑎) ∈ 𝐽 ∧ 𝑎 ⊆ ∪ ran
𝑓)) |
62 | 61 | ancomd 460 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ⊆ ∪ ran
𝑓) → (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽)) |
63 | 28 | ad2antll 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → 𝑎 ⊆ 𝑋) |
64 | 63 | anim1i 613 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ⊆ ∪ ran
𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽)) → (𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran
𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽))) |
65 | | unisng 4925 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑋 ∖ 𝑎) ∈ 𝐽 → ∪ {(𝑋 ∖ 𝑎)} = (𝑋 ∖ 𝑎)) |
66 | 65 | eqcomd 2732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑋 ∖ 𝑎) ∈ 𝐽 → (𝑋 ∖ 𝑎) = ∪ {(𝑋 ∖ 𝑎)}) |
67 | | eqimss 4037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑋 ∖ 𝑎) = ∪ {(𝑋 ∖ 𝑎)} → (𝑋 ∖ 𝑎) ⊆ ∪
{(𝑋 ∖ 𝑎)}) |
68 | | ssun4 4173 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑋 ∖ 𝑎) ⊆ ∪
{(𝑋 ∖ 𝑎)} → (𝑋 ∖ 𝑎) ⊆ (∪ ran
𝑓 ∪ ∪ {(𝑋
∖ 𝑎)})) |
69 | | uniun 4930 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) = (∪ ran 𝑓 ∪ ∪ {(𝑋
∖ 𝑎)}) |
70 | 68, 69 | sseqtrrdi 4030 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑋 ∖ 𝑎) ⊆ ∪
{(𝑋 ∖ 𝑎)} → (𝑋 ∖ 𝑎) ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
71 | 66, 67, 70 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑋 ∖ 𝑎) ∈ 𝐽 → (𝑋 ∖ 𝑎) ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
72 | | ssun3 4172 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑎 ⊆ ∪ ran 𝑓 → 𝑎 ⊆ (∪ ran
𝑓 ∪ ∪ {(𝑋
∖ 𝑎)})) |
73 | 72, 69 | sseqtrrdi 4030 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑎 ⊆ ∪ ran 𝑓 → 𝑎 ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
74 | | uncom 4150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝑎 ∪ (𝑋 ∖ 𝑎)) = ((𝑋 ∖ 𝑎) ∪ 𝑎) |
75 | | undif1 4470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝑋 ∖ 𝑎) ∪ 𝑎) = (𝑋 ∪ 𝑎) |
76 | 74, 75 | eqtri 2754 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝑎 ∪ (𝑋 ∖ 𝑎)) = (𝑋 ∪ 𝑎) |
77 | | ssequn2 4181 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝑎 ⊆ 𝑋 ↔ (𝑋 ∪ 𝑎) = 𝑋) |
78 | 77 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝑎 ⊆ 𝑋 → (𝑋 ∪ 𝑎) = 𝑋) |
79 | 76, 78 | eqtrid 2778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝑎 ⊆ 𝑋 → (𝑎 ∪ (𝑋 ∖ 𝑎)) = 𝑋) |
80 | 79 | adantr 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}))) → (𝑎 ∪ (𝑋 ∖ 𝑎)) = 𝑋) |
81 | | unss12 4180 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑎 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)})) → (𝑎 ∪ (𝑋 ∖ 𝑎)) ⊆ (∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∪ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}))) |
82 | | unidm 4149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∪ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)})) = ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}) |
83 | 81, 82 | sseqtrdi 4029 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑎 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)})) → (𝑎 ∪ (𝑋 ∖ 𝑎)) ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
84 | 83 | adantl 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}))) → (𝑎 ∪ (𝑋 ∖ 𝑎)) ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
85 | 80, 84 | eqsstrrd 4018 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}))) → 𝑋 ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
86 | 73, 85 | sylanr1 680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran
𝑓 ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}))) → 𝑋 ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
87 | 71, 86 | sylanr2 681 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran
𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽)) → 𝑋 ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
88 | 87 | adantl 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran
𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽))) → 𝑋 ⊆ ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
89 | | f1f 6790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑓:𝑎–1-1→𝐽 → 𝑓:𝑎⟶𝐽) |
90 | | frn 6727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑓:𝑎⟶𝐽 → ran 𝑓 ⊆ 𝐽) |
91 | 89, 90 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑓:𝑎–1-1→𝐽 → ran 𝑓 ⊆ 𝐽) |
92 | 1 | topopn 22896 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽) |
93 | 1 | difopn 23026 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑋 ∈ 𝐽 ∧ 𝑎 ∈ (Clsd‘𝐽)) → (𝑋 ∖ 𝑎) ∈ 𝐽) |
94 | 92, 93 | sylan 578 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) → (𝑋 ∖ 𝑎) ∈ 𝐽) |
95 | 94 | snssd 4808 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) → {(𝑋 ∖ 𝑎)} ⊆ 𝐽) |
96 | | unss12 4180 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((ran
𝑓 ⊆ 𝐽 ∧ {(𝑋 ∖ 𝑎)} ⊆ 𝐽) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ (𝐽 ∪ 𝐽)) |
97 | | unidm 4149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝐽 ∪ 𝐽) = 𝐽 |
98 | 96, 97 | sseqtrdi 4029 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((ran
𝑓 ⊆ 𝐽 ∧ {(𝑋 ∖ 𝑎)} ⊆ 𝐽) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽) |
99 | 91, 95, 98 | syl2an 594 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽) |
100 | | uniss 4913 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽 → ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ ∪
𝐽) |
101 | 100, 1 | sseqtrrdi 4030 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽 → ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝑋) |
102 | 99, 101 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝑋) |
103 | 102 | adantr 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran
𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽))) → ∪ (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝑋) |
104 | 88, 103 | eqssd 3996 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran
𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽))) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
105 | 64, 104 | syldan 589 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ⊆ ∪ ran
𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽)) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
106 | 62, 105 | syldan 589 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ⊆ ∪ ran
𝑓) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
107 | 58, 106 | sylan2 591 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
108 | 107 | ancom1s 651 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎–1-1→𝐽) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
109 | 108 | ex 411 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎–1-1→𝐽) → ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))) |
110 | 45, 109 | mpand 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎–1-1→𝐽) → (∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))) |
111 | 110 | impr 453 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
112 | 111 | adantlrr 719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
113 | 4, 112 | sylanl1 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
114 | | vex 3466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 𝑓 ∈ V |
115 | | f1f1orn 6846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑓:𝑎–1-1→𝐽 → 𝑓:𝑎–1-1-onto→ran
𝑓) |
116 | | f1oen3g 8989 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑓 ∈ V ∧ 𝑓:𝑎–1-1-onto→ran
𝑓) → 𝑎 ≈ ran 𝑓) |
117 | 114, 115,
116 | sylancr 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑓:𝑎–1-1→𝐽 → 𝑎 ≈ ran 𝑓) |
118 | | enen1 9147 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑎 ≈ ran 𝑓 → (𝑎 ≈ ω ↔ ran 𝑓 ≈
ω)) |
119 | | endom 9002 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (ran
𝑓 ≈ ω →
ran 𝑓 ≼
ω) |
120 | | snfi 9073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ {(𝑋 ∖ 𝑎)} ∈ Fin |
121 | | isfinite 9688 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ({(𝑋 ∖ 𝑎)} ∈ Fin ↔ {(𝑋 ∖ 𝑎)} ≺ ω) |
122 | 120, 121 | mpbi 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ {(𝑋 ∖ 𝑎)} ≺ ω |
123 | | sdomdom 9003 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ({(𝑋 ∖ 𝑎)} ≺ ω → {(𝑋 ∖ 𝑎)} ≼ ω) |
124 | 122, 123 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ {(𝑋 ∖ 𝑎)} ≼ ω |
125 | | unctb 10239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((ran
𝑓 ≼ ω ∧
{(𝑋 ∖ 𝑎)} ≼ ω) → (ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) |
126 | 119, 124,
125 | sylancl 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (ran
𝑓 ≈ ω →
(ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) |
127 | 118, 126 | biimtrdi 252 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑎 ≈ ran 𝑓 → (𝑎 ≈ ω → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω)) |
128 | 117, 127 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑓:𝑎–1-1→𝐽 → (𝑎 ≈ ω → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω)) |
129 | 128 | impcom 406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑎 ≈ ω ∧ 𝑓:𝑎–1-1→𝐽) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) |
130 | 129 | adantll 712 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω) ∧ 𝑓:𝑎–1-1→𝐽) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) |
131 | 130 | ad2ant2lr 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) |
132 | 99 | ancoms 457 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎–1-1→𝐽) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽) |
133 | 132 | adantrr 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽) |
134 | 133 | adantlrr 719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽) |
135 | 4, 134 | sylanl1 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽) |
136 | | elpw2g 5343 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝐽 ∈ 𝐶 → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽 ↔ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽)) |
137 | 136 | biimprd 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐽 ∈ 𝐶 → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽 → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽)) |
138 | 137 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽 → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽)) |
139 | 135, 138 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽) |
140 | 3 | simprbi 495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝐽 ∈ 𝐶 → ∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)) |
141 | | unieq 4916 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑠 = 𝑧 → ∪ 𝑠 = ∪
𝑧) |
142 | 141 | eqeq2d 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑠 = 𝑧 → (𝑋 = ∪ 𝑠 ↔ 𝑋 = ∪ 𝑧)) |
143 | 142 | cbvrexvw 3226 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(∃𝑠 ∈
(𝒫 𝑦 ∩
Fin)𝑋 = ∪ 𝑠
↔ ∃𝑧 ∈
(𝒫 𝑦 ∩
Fin)𝑋 = ∪ 𝑧) |
144 | 143 | imbi2i 335 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑋 = ∪
𝑦 ∧ 𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠) ↔ ((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)) |
145 | 144 | ralbii 3083 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(∀𝑦 ∈
𝒫 𝐽((𝑋 = ∪
𝑦 ∧ 𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠) ↔ ∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)) |
146 | 140, 145 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐽 ∈ 𝐶 → ∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠)) |
147 | | unieq 4916 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → ∪ 𝑦 = ∪
(ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
148 | 147 | eqeq2d 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑋 = ∪ 𝑦 ↔ 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))) |
149 | | breq1 5148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑦 ≼ ω ↔ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω)) |
150 | 148, 149 | anbi12d 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → ((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) ↔ (𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω))) |
151 | | pweq 4611 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → 𝒫 𝑦 = 𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
152 | 151 | ineq1d 4209 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝒫 𝑦 ∩ Fin) = (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)) |
153 | 152 | rexeqdv 3316 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠 ↔ ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠)) |
154 | 150, 153 | imbi12d 343 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠) ↔ ((𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠))) |
155 | 154 | rspccv 3604 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∀𝑦 ∈
𝒫 𝐽((𝑋 = ∪
𝑦 ∧ 𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠) → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠))) |
156 | 146, 155 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐽 ∈ 𝐶 → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠))) |
157 | 156 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠))) |
158 | 139, 157 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠)) |
159 | 113, 131,
158 | mp2and 697 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠) |
160 | | df-rex 3061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∃𝑠 ∈
(𝒫 (ran 𝑓 ∪
{(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠 ↔ ∃𝑠(𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠)) |
161 | | elinel1 4193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) → 𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
162 | | velpw 4602 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ↔ 𝑠 ⊆ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) |
163 | | ssdif 4136 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∖ {(𝑋 ∖ 𝑎)})) |
164 | | difun2 4475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((ran
𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∖ {(𝑋 ∖ 𝑎)}) = (ran 𝑓 ∖ {(𝑋 ∖ 𝑎)}) |
165 | 163, 164 | sseqtrdi 4029 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ (ran 𝑓 ∖ {(𝑋 ∖ 𝑎)})) |
166 | 165 | difss2d 4131 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓) |
167 | 162, 166 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓) |
168 | 161, 167 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓) |
169 | 168 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) → (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓)) |
170 | | sseq2 4005 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑋 = ∪
𝑠 → (𝑎 ⊆ 𝑋 ↔ 𝑎 ⊆ ∪ 𝑠)) |
171 | | uniexg 7743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝐽 ∈ Top → ∪ 𝐽
∈ V) |
172 | 1, 171 | eqeltrid 2830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝐽 ∈ Top → 𝑋 ∈ V) |
173 | | difexg 5326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝑋 ∈ V → (𝑋 ∖ 𝑎) ∈ V) |
174 | | unisng 4925 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑋 ∖ 𝑎) ∈ V → ∪ {(𝑋
∖ 𝑎)} = (𝑋 ∖ 𝑎)) |
175 | 172, 173,
174 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝐽 ∈ Top → ∪ {(𝑋
∖ 𝑎)} = (𝑋 ∖ 𝑎)) |
176 | 175 | ineq2d 4210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝐽 ∈ Top → (𝑎 ∩ ∪ {(𝑋
∖ 𝑎)}) = (𝑎 ∩ (𝑋 ∖ 𝑎))) |
177 | | disjdif 4466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑎 ∩ (𝑋 ∖ 𝑎)) = ∅ |
178 | 176, 177 | eqtrdi 2782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝐽 ∈ Top → (𝑎 ∩ ∪ {(𝑋
∖ 𝑎)}) =
∅) |
179 | | inunissunidif 37095 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑎 ∩ ∪ {(𝑋
∖ 𝑎)}) = ∅
→ (𝑎 ⊆ ∪ 𝑠
↔ 𝑎 ⊆ ∪ (𝑠
∖ {(𝑋 ∖ 𝑎)}))) |
180 | 178, 179 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝐽 ∈ Top → (𝑎 ⊆ ∪ 𝑠
↔ 𝑎 ⊆ ∪ (𝑠
∖ {(𝑋 ∖ 𝑎)}))) |
181 | 170, 180 | sylan9bbr 509 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪
𝑠) → (𝑎 ⊆ 𝑋 ↔ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) |
182 | 181 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪
𝑠) → (𝑎 ⊆ 𝑋 → 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) |
183 | 182 | impancom 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) → (𝑋 = ∪ 𝑠 → 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) |
184 | 169, 183 | anim12d 607 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)})))) |
185 | 4, 28, 184 | syl2an 594 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐽 ∈ 𝐶 ∧ 𝑎 ∈ (Clsd‘𝐽)) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)})))) |
186 | 185 | adantrr 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)})))) |
187 | 186 | anim2d 610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠)) → ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))))) |
188 | 117 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) → 𝑎 ≈ ran 𝑓) |
189 | | fvineqsneq 37132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝑓 Fn 𝑎 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) = ran 𝑓) |
190 | 54, 189 | sylanl1 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) = ran 𝑓) |
191 | | vex 3466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ 𝑠 ∈ V |
192 | | difss 4128 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ 𝑠 |
193 | | ssdomg 9023 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑠 ∈ V → ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ 𝑠 → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ≼ 𝑠)) |
194 | 191, 192,
193 | mp2 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ≼ 𝑠 |
195 | 190, 194 | eqbrtrrdi 5185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) → ran 𝑓 ≼ 𝑠) |
196 | | endomtr 9035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑎 ≈ ran 𝑓 ∧ ran 𝑓 ≼ 𝑠) → 𝑎 ≼ 𝑠) |
197 | 188, 195,
196 | syl2anc 582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) → 𝑎 ≼ 𝑠) |
198 | 187, 197 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠)) → 𝑎 ≼ 𝑠)) |
199 | 198 | expdimp 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → 𝑎 ≼ 𝑠)) |
200 | | elinel2 4194 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) → 𝑠 ∈ Fin) |
201 | 200 | adantr 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → 𝑠 ∈ Fin) |
202 | 201 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → 𝑠 ∈ Fin)) |
203 | 199, 202 | jcad 511 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → (𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin))) |
204 | 203 | eximdv 1913 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (∃𝑠(𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin))) |
205 | 160, 204 | biimtrid 241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠 → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin))) |
206 | 159, 205 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)) |
207 | 206 | ex 411 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin))) |
208 | 207 | exlimdv 1929 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin))) |
209 | 208 | anass1rs 653 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽)) → (∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin))) |
210 | 209 | 3adant3 1129 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin))) |
211 | 44, 210 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)) |
212 | 17, 26, 27, 211 | syl3anc 1368 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)) |
213 | 212 | anasss 465 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)) |
214 | | isfinite 9688 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 ∈ Fin ↔ 𝑠 ≺
ω) |
215 | | domsdomtr 9142 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ≼ 𝑠 ∧ 𝑠 ≺ ω) → 𝑎 ≺ ω) |
216 | 214, 215 | sylan2b 592 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin) → 𝑎 ≺ ω) |
217 | 216 | exlimiv 1926 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin) → 𝑎 ≺ ω) |
218 | | sdomnen 9004 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ≺ ω → ¬
𝑎 ≈
ω) |
219 | 213, 217,
218 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → ¬ 𝑎 ≈ ω) |
220 | 16, 219 | pm2.65da 815 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) → ¬ (𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) |
221 | | imnan 398 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ⊆ 𝑋 → ¬ ((limPt‘𝐽)‘𝑎) = ∅) ↔ ¬ (𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) |
222 | 220, 221 | sylibr 233 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) → (𝑎 ⊆ 𝑋 → ¬ ((limPt‘𝐽)‘𝑎) = ∅)) |
223 | 222 | imp 405 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → ¬ ((limPt‘𝐽)‘𝑎) = ∅) |
224 | | neq0 4345 |
. . . . . . . . . . . . . . 15
⊢ (¬
((limPt‘𝐽)‘𝑎) = ∅ ↔ ∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎)) |
225 | 223, 224 | sylib 217 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → ∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎)) |
226 | 1 | lpss 23134 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋) |
227 | 4, 226 | sylan 578 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐽 ∈ 𝐶 ∧ 𝑎 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋) |
228 | 227 | adantlr 713 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋) |
229 | 228 | sseld 3977 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → 𝑠 ∈ 𝑋)) |
230 | 229 | ancrd 550 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → (𝑠 ∈ 𝑋 ∧ 𝑠 ∈ ((limPt‘𝐽)‘𝑎)))) |
231 | 230 | eximdv 1913 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → (∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠(𝑠 ∈ 𝑋 ∧ 𝑠 ∈ ((limPt‘𝐽)‘𝑎)))) |
232 | | df-rex 3061 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑠 ∈
𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎) ↔ ∃𝑠(𝑠 ∈ 𝑋 ∧ 𝑠 ∈ ((limPt‘𝐽)‘𝑎))) |
233 | 231, 232 | imbitrrdi 251 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → (∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎))) |
234 | 225, 233 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎)) |
235 | 15, 234 | sylan2 591 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎)) |
236 | 1 | lpss3 23136 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐽 ∈ Top ∧ 𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏)) |
237 | 236 | 3expb 1117 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ Top ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏)) |
238 | 4, 237 | sylan 578 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ 𝐶 ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏)) |
239 | 238 | adantlr 713 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏)) |
240 | 239 | sseld 3977 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → 𝑠 ∈ ((limPt‘𝐽)‘𝑏))) |
241 | 240 | reximdv 3160 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → (∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))) |
242 | 235, 241 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)) |
243 | 242 | an42s 659 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ 𝐶 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)) |
244 | 243 | ex 411 |
. . . . . . . . 9
⊢ ((𝐽 ∈ 𝐶 ∧ 𝑏 ⊆ 𝑋) → ((𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))) |
245 | 244 | exlimdv 1929 |
. . . . . . . 8
⊢ ((𝐽 ∈ 𝐶 ∧ 𝑏 ⊆ 𝑋) → (∃𝑎(𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))) |
246 | 245 | adantrr 715 |
. . . . . . 7
⊢ ((𝐽 ∈ 𝐶 ∧ (𝑏 ⊆ 𝑋 ∧ ¬ 𝑏 ∈ Fin)) → (∃𝑎(𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))) |
247 | 13, 246 | mpd 15 |
. . . . . 6
⊢ ((𝐽 ∈ 𝐶 ∧ (𝑏 ⊆ 𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)) |
248 | 7, 247 | sylan2b 592 |
. . . . 5
⊢ ((𝐽 ∈ 𝐶 ∧ (𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)) |
249 | 5, 248 | sylan2b 592 |
. . . 4
⊢ ((𝐽 ∈ 𝐶 ∧ 𝑏 ∈ (𝒫 𝑋 ∖ Fin)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)) |
250 | 249 | ralrimiva 3136 |
. . 3
⊢ (𝐽 ∈ 𝐶 → ∀𝑏 ∈ (𝒫 𝑋 ∖ Fin)∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)) |
251 | | simpr 483 |
. . . . . 6
⊢ ((𝑦 = 𝑏 ∧ 𝑧 = 𝑠) → 𝑧 = 𝑠) |
252 | | fveq2 6893 |
. . . . . . 7
⊢ (𝑦 = 𝑏 → ((limPt‘𝐽)‘𝑦) = ((limPt‘𝐽)‘𝑏)) |
253 | 252 | adantr 479 |
. . . . . 6
⊢ ((𝑦 = 𝑏 ∧ 𝑧 = 𝑠) → ((limPt‘𝐽)‘𝑦) = ((limPt‘𝐽)‘𝑏)) |
254 | 251, 253 | eleq12d 2820 |
. . . . 5
⊢ ((𝑦 = 𝑏 ∧ 𝑧 = 𝑠) → (𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ 𝑠 ∈ ((limPt‘𝐽)‘𝑏))) |
255 | 254 | cbvrexdva 3228 |
. . . 4
⊢ (𝑦 = 𝑏 → (∃𝑧 ∈ 𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))) |
256 | 255 | cbvralvw 3225 |
. . 3
⊢
(∀𝑦 ∈
(𝒫 𝑋 ∖
Fin)∃𝑧 ∈ 𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ ∀𝑏 ∈ (𝒫 𝑋 ∖ Fin)∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)) |
257 | 250, 256 | sylibr 233 |
. 2
⊢ (𝐽 ∈ 𝐶 → ∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧 ∈ 𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦)) |
258 | | pibt2.21 |
. . 3
⊢ 𝑊 = {𝑥 ∈ Top ∣ ∀𝑦 ∈ (𝒫 ∪ 𝑥
∖ Fin)∃𝑧 ∈
∪ 𝑥𝑧 ∈ ((limPt‘𝑥)‘𝑦)} |
259 | 1, 258 | pibp21 37135 |
. 2
⊢ (𝐽 ∈ 𝑊 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧 ∈ 𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦))) |
260 | 4, 257, 259 | sylanbrc 581 |
1
⊢ (𝐽 ∈ 𝐶 → 𝐽 ∈ 𝑊) |