| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > isperf3 | Structured version Visualization version GIF version | ||
| Description: A perfect space is a topology which has no open singletons. (Contributed by Mario Carneiro, 24-Dec-2016.) |
| Ref | Expression |
|---|---|
| lpfval.1 | ⊢ 𝑋 = ∪ 𝐽 |
| Ref | Expression |
|---|---|
| isperf3 | ⊢ (𝐽 ∈ Perf ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ¬ {𝑥} ∈ 𝐽)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lpfval.1 | . . 3 ⊢ 𝑋 = ∪ 𝐽 | |
| 2 | 1 | isperf2 23266 | . 2 ⊢ (𝐽 ∈ Perf ↔ (𝐽 ∈ Top ∧ 𝑋 ⊆ ((limPt‘𝐽)‘𝑋))) |
| 3 | dfss3 3928 | . . . 4 ⊢ (𝑋 ⊆ ((limPt‘𝐽)‘𝑋) ↔ ∀𝑥 ∈ 𝑋 𝑥 ∈ ((limPt‘𝐽)‘𝑋)) | |
| 4 | 1 | maxlp 23261 | . . . . . 6 ⊢ (𝐽 ∈ Top → (𝑥 ∈ ((limPt‘𝐽)‘𝑋) ↔ (𝑥 ∈ 𝑋 ∧ ¬ {𝑥} ∈ 𝐽))) |
| 5 | 4 | baibd 548 | . . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝑋) → (𝑥 ∈ ((limPt‘𝐽)‘𝑋) ↔ ¬ {𝑥} ∈ 𝐽)) |
| 6 | 5 | ralbidva 3186 | . . . 4 ⊢ (𝐽 ∈ Top → (∀𝑥 ∈ 𝑋 𝑥 ∈ ((limPt‘𝐽)‘𝑋) ↔ ∀𝑥 ∈ 𝑋 ¬ {𝑥} ∈ 𝐽)) |
| 7 | 3, 6 | bitrid 286 | . . 3 ⊢ (𝐽 ∈ Top → (𝑋 ⊆ ((limPt‘𝐽)‘𝑋) ↔ ∀𝑥 ∈ 𝑋 ¬ {𝑥} ∈ 𝐽)) |
| 8 | 7 | pm5.32i 584 | . 2 ⊢ ((𝐽 ∈ Top ∧ 𝑋 ⊆ ((limPt‘𝐽)‘𝑋)) ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ¬ {𝑥} ∈ 𝐽)) |
| 9 | 2, 8 | bitri 278 | 1 ⊢ (𝐽 ∈ Perf ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ¬ {𝑥} ∈ 𝐽)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ↔ wb 209 ∧ wa 400 = wceq 1563 ∈ wcel 2145 ∀wral 3079 ⊆ wss 3907 {csn 4585 ∪ cuni 4867 ‘cfv 6525 Topctop 23007 limPtclp 23248 Perfcperf 23249 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-rep 5231 ax-sep 5250 ax-nul 5260 ax-pow 5326 ax-pr 5394 ax-un 7722 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3080 df-rex 3090 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5105 df-opab 5167 df-mpt 5186 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-top 23008 df-cld 23133 df-ntr 23134 df-cls 23135 df-lp 23250 df-perf 23251 |
| This theorem is referenced by: perfi 23269 perfopn 23299 t1connperf 23550 |
| Copyright terms: Public domain | W3C validator |