Theorem fctop2

Description: The finite complement topology on a set A . Example 3 in Munkres p. 77. (This version of fctop requires the Axiom of Infinity.) (Contributed by FL, 20-Aug-2006)

	Ref	Expression
Assertion	fctop2	$$⊢A\in V\to \left\{x\in 𝒫A|\left(\left(A\setminus x\right)\prec \mathrm{\omega }\vee x=\varnothing \right)\right\}\in \mathrm{TopOn}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		isfinite	$$⊢A\setminus x\in \mathrm{Fin}\leftrightarrow \left(A\setminus x\right)\prec \mathrm{\omega }$$
2	1	orbi1i	$$⊢\left(A\setminus x\in \mathrm{Fin}\vee x=\varnothing \right)\leftrightarrow \left(\left(A\setminus x\right)\prec \mathrm{\omega }\vee x=\varnothing \right)$$
3	2	rabbii	$$⊢\left\{x\in 𝒫A|\left(A\setminus x\in \mathrm{Fin}\vee x=\varnothing \right)\right\}=\left\{x\in 𝒫A|\left(\left(A\setminus x\right)\prec \mathrm{\omega }\vee x=\varnothing \right)\right\}$$
4		fctop	$$⊢A\in V\to \left\{x\in 𝒫A|\left(A\setminus x\in \mathrm{Fin}\vee x=\varnothing \right)\right\}\in \mathrm{TopOn}\left(A\right)$$
5	3 4	eqeltrrid	$$⊢A\in V\to \left\{x\in 𝒫A|\left(\left(A\setminus x\right)\prec \mathrm{\omega }\vee x=\varnothing \right)\right\}\in \mathrm{TopOn}\left(A\right)$$