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 e. V -> { x e. ~P A | ( ( A \ x ) ~< _om \/ x = (/) ) } e. ( TopOn ` A ) )

Proof

Step Hyp Ref Expression
1 isfinite
 |-  ( ( A \ x ) e. Fin <-> ( A \ x ) ~< _om )
2 1 orbi1i
 |-  ( ( ( A \ x ) e. Fin \/ x = (/) ) <-> ( ( A \ x ) ~< _om \/ x = (/) ) )
3 2 rabbii
 |-  { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } = { x e. ~P A | ( ( A \ x ) ~< _om \/ x = (/) ) }
4 fctop
 |-  ( A e. V -> { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } e. ( TopOn ` A ) )
5 3 4 eqeltrrid
 |-  ( A e. V -> { x e. ~P A | ( ( A \ x ) ~< _om \/ x = (/) ) } e. ( TopOn ` A ) )