Theorem topdifinf

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	|- T = { x e. ~P A | ( -. ( A \ x ) e. Fin \/ ( x = (/) \/ x = A ) ) }
Assertion	topdifinf	|- ( ( T e. ( TopOn ` A ) <-> A e. Fin ) /\ ( T e. ( TopOn ` A ) -> T = { (/) , A } ) )

Proof

Step	Hyp	Ref	Expression
1		topdifinf.t	|- T = { x e. ~P A | ( -. ( A \ x ) e. Fin \/ ( x = (/) \/ x = A ) ) }
2	1	topdifinffin	|- ( T e. ( TopOn ` A ) -> A e. Fin )
3	1	topdifinfindis	|- ( A e. Fin -> T = { (/) , A } )
4		indistopon	|- ( A e. Fin -> { (/) , A } e. ( TopOn ` A ) )
5	3 4	eqeltrd	|- ( A e. Fin -> T e. ( TopOn ` A ) )
6	2 5	impbii	|- ( T e. ( TopOn ` A ) <-> A e. Fin )
7	2 3	syl	|- ( T e. ( TopOn ` A ) -> T = { (/) , A } )
8	6 7	pm3.2i	|- ( ( T e. ( TopOn ` A ) <-> A e. Fin ) /\ ( T e. ( TopOn ` A ) -> T = { (/) , A } ) )