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

Proof

Step	Hyp	Ref	Expression
1		topdifinf.t	|- T = { x e. ~P A | ( -. ( A \ x ) e. Fin \/ ( x = (/) \/ x = A ) ) }
2		difeq2	|- ( x = y -> ( A \ x ) = ( A \ y ) )
3	2	eleq1d	|- ( x = y -> ( ( A \ x ) e. Fin <-> ( A \ y ) e. Fin ) )
4	3	notbid	|- ( x = y -> ( -. ( A \ x ) e. Fin <-> -. ( A \ y ) e. Fin ) )
5		eqeq1	|- ( x = y -> ( x = (/) <-> y = (/) ) )
6		eqeq1	|- ( x = y -> ( x = A <-> y = A ) )
7	5 6	orbi12d	|- ( x = y -> ( ( x = (/) \/ x = A ) <-> ( y = (/) \/ y = A ) ) )
8	4 7	orbi12d	|- ( x = y -> ( ( -. ( A \ x ) e. Fin \/ ( x = (/) \/ x = A ) ) <-> ( -. ( A \ y ) e. Fin \/ ( y = (/) \/ y = A ) ) ) )
9	8	cbvrabv	|- { x e. ~P A | ( -. ( A \ x ) e. Fin \/ ( x = (/) \/ x = A ) ) } = { y e. ~P A | ( -. ( A \ y ) e. Fin \/ ( y = (/) \/ y = A ) ) }
10	1 9	eqtri	|- T = { y e. ~P A | ( -. ( A \ y ) e. Fin \/ ( y = (/) \/ y = A ) ) }
11	10	topdifinffinlem	|- ( T e. ( TopOn ` A ) -> A e. Fin )