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	⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ≺ ω ∨ 𝑥 = ∅ ) } ∈ ( TopOn ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		isfinite	⊢ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ↔ ( 𝐴 ∖ 𝑥 ) ≺ ω )
2	1	orbi1i	⊢ ( ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) ↔ ( ( 𝐴 ∖ 𝑥 ) ≺ ω ∨ 𝑥 = ∅ ) )
3	2	rabbii	⊢ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } = { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ≺ ω ∨ 𝑥 = ∅ ) }
4		fctop	⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ∈ ( TopOn ‘ 𝐴 ) )
5	3 4	eqeltrrid	⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ≺ ω ∨ 𝑥 = ∅ ) } ∈ ( TopOn ‘ 𝐴 ) )