This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ V → x ∈ 𝒫 A | A ∖ x ≺ ω ∨ x = ∅ ∈ TopOn ⁡ A

Proof

Step Hyp Ref Expression
1 isfinite ⊢ A ∖ x ∈ Fin ↔ A ∖ x ≺ ω
2 1 orbi1i ⊢ A ∖ x ∈ Fin ∨ x = ∅ ↔ A ∖ x ≺ ω ∨ x = ∅
3 2 rabbii ⊢ x ∈ 𝒫 A | A ∖ x ∈ Fin ∨ x = ∅ = x ∈ 𝒫 A | A ∖ x ≺ ω ∨ x = ∅
4 fctop ⊢ A ∈ V → x ∈ 𝒫 A | A ∖ x ∈ Fin ∨ x = ∅ ∈ TopOn ⁡ A
5 3 4 eqeltrrid ⊢ A ∈ V → x ∈ 𝒫 A | A ∖ x ≺ ω ∨ x = ∅ ∈ TopOn ⁡ A