Theorem topdifinffin

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 only if A is finite. (Contributed by ML, 17-Jul-2020)

	Ref	Expression
Hypothesis	topdifinf.t	⊢ 𝑇 = { 𝑥 ∈ 𝒫 𝐴 ∣ ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) }
Assertion	topdifinffin	⊢ ( 𝑇 ∈ ( TopOn ‘ 𝐴 ) → 𝐴 ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		topdifinf.t	⊢ 𝑇 = { 𝑥 ∈ 𝒫 𝐴 ∣ ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) }
2		difeq2	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ 𝑦 ) )
3	2	eleq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ↔ ( 𝐴 ∖ 𝑦 ) ∈ Fin ) )
4	3	notbid	⊢ ( 𝑥 = 𝑦 → ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ↔ ¬ ( 𝐴 ∖ 𝑦 ) ∈ Fin ) )
5		eqeq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = ∅ ↔ 𝑦 = ∅ ) )
6		eqeq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝐴 ↔ 𝑦 = 𝐴 ) )
7	5 6	orbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ↔ ( 𝑦 = ∅ ∨ 𝑦 = 𝐴 ) ) )
8	4 7	orbi12d	⊢ ( 𝑥 = 𝑦 → ( ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) ↔ ( ¬ ( 𝐴 ∖ 𝑦 ) ∈ Fin ∨ ( 𝑦 = ∅ ∨ 𝑦 = 𝐴 ) ) ) )
9	8	cbvrabv	⊢ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) } = { 𝑦 ∈ 𝒫 𝐴 ∣ ( ¬ ( 𝐴 ∖ 𝑦 ) ∈ Fin ∨ ( 𝑦 = ∅ ∨ 𝑦 = 𝐴 ) ) }
10	1 9	eqtri	⊢ 𝑇 = { 𝑦 ∈ 𝒫 𝐴 ∣ ( ¬ ( 𝐴 ∖ 𝑦 ) ∈ Fin ∨ ( 𝑦 = ∅ ∨ 𝑦 = 𝐴 ) ) }
11	10	topdifinffinlem	⊢ ( 𝑇 ∈ ( TopOn ‘ 𝐴 ) → 𝐴 ∈ Fin )