Description: Part of Exercise 3 of Munkres p. 83. The topology of all subsets x of A such that the complement of x in A is infinite, or x is the empty set, or x is all of A , is a topology if and only if A is finite, in which case it is the trivial topology. (Contributed by ML, 17-Jul-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | topdifinf.t | ⊢ 𝑇 = { 𝑥 ∈ 𝒫 𝐴 ∣ ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) } | |
| Assertion | topdifinf | ⊢ ( ( 𝑇 ∈ ( TopOn ‘ 𝐴 ) ↔ 𝐴 ∈ Fin ) ∧ ( 𝑇 ∈ ( TopOn ‘ 𝐴 ) → 𝑇 = { ∅ , 𝐴 } ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | topdifinf.t | ⊢ 𝑇 = { 𝑥 ∈ 𝒫 𝐴 ∣ ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) } | |
| 2 | 1 | topdifinffin | ⊢ ( 𝑇 ∈ ( TopOn ‘ 𝐴 ) → 𝐴 ∈ Fin ) |
| 3 | 1 | topdifinfindis | ⊢ ( 𝐴 ∈ Fin → 𝑇 = { ∅ , 𝐴 } ) |
| 4 | indistopon | ⊢ ( 𝐴 ∈ Fin → { ∅ , 𝐴 } ∈ ( TopOn ‘ 𝐴 ) ) | |
| 5 | 3 4 | eqeltrd | ⊢ ( 𝐴 ∈ Fin → 𝑇 ∈ ( TopOn ‘ 𝐴 ) ) |
| 6 | 2 5 | impbii | ⊢ ( 𝑇 ∈ ( TopOn ‘ 𝐴 ) ↔ 𝐴 ∈ Fin ) |
| 7 | 2 3 | syl | ⊢ ( 𝑇 ∈ ( TopOn ‘ 𝐴 ) → 𝑇 = { ∅ , 𝐴 } ) |
| 8 | 6 7 | pm3.2i | ⊢ ( ( 𝑇 ∈ ( TopOn ‘ 𝐴 ) ↔ 𝐴 ∈ Fin ) ∧ ( 𝑇 ∈ ( TopOn ‘ 𝐴 ) → 𝑇 = { ∅ , 𝐴 } ) ) |