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

Metamath Proof Explorer

Theorem is1stc2

Description: An equivalent way of saying "is a first-countable topology." (Contributed by Jeff Hankins, 22-Aug-2009) (Revised by Mario Carneiro, 21-Mar-2015)

Ref Expression
Hypothesis is1stc.1 
|- X = U. J
Assertion is1stc2 
|- ( J e. 1stc <-> ( J e. Top /\ A. x e. X E. y e. ~P J ( y ~<_ _om /\ A. z e. J ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) ) )

Proof

Step Hyp Ref Expression
1 is1stc.1 
 |-  X = U. J
2 1 is1stc 
 |-  ( J e. 1stc <-> ( J e. Top /\ A. x e. X E. y e. ~P J ( y ~<_ _om /\ A. z e. J ( x e. z -> x e. U. ( y i^i ~P z ) ) ) ) )
3 elin 
 |-  ( w e. ( y i^i ~P z ) <-> ( w e. y /\ w e. ~P z ) )
4 velpw 
 |-  ( w e. ~P z <-> w C_ z )
5 4 anbi2i 
 |-  ( ( w e. y /\ w e. ~P z ) <-> ( w e. y /\ w C_ z ) )
6 3 5 bitri 
 |-  ( w e. ( y i^i ~P z ) <-> ( w e. y /\ w C_ z ) )
7 6 anbi2i 
 |-  ( ( x e. w /\ w e. ( y i^i ~P z ) ) <-> ( x e. w /\ ( w e. y /\ w C_ z ) ) )
8 an12 
 |-  ( ( x e. w /\ ( w e. y /\ w C_ z ) ) <-> ( w e. y /\ ( x e. w /\ w C_ z ) ) )
9 7 8 bitri 
 |-  ( ( x e. w /\ w e. ( y i^i ~P z ) ) <-> ( w e. y /\ ( x e. w /\ w C_ z ) ) )
10 9 exbii 
 |-  ( E. w ( x e. w /\ w e. ( y i^i ~P z ) ) <-> E. w ( w e. y /\ ( x e. w /\ w C_ z ) ) )
11 eluni 
 |-  ( x e. U. ( y i^i ~P z ) <-> E. w ( x e. w /\ w e. ( y i^i ~P z ) ) )
12 df-rex 
 |-  ( E. w e. y ( x e. w /\ w C_ z ) <-> E. w ( w e. y /\ ( x e. w /\ w C_ z ) ) )
13 10 11 12 3bitr4i 
 |-  ( x e. U. ( y i^i ~P z ) <-> E. w e. y ( x e. w /\ w C_ z ) )
14 13 imbi2i 
 |-  ( ( x e. z -> x e. U. ( y i^i ~P z ) ) <-> ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) )
15 14 ralbii 
 |-  ( A. z e. J ( x e. z -> x e. U. ( y i^i ~P z ) ) <-> A. z e. J ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) )
16 15 anbi2i 
 |-  ( ( y ~<_ _om /\ A. z e. J ( x e. z -> x e. U. ( y i^i ~P z ) ) ) <-> ( y ~<_ _om /\ A. z e. J ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) )
17 16 rexbii 
 |-  ( E. y e. ~P J ( y ~<_ _om /\ A. z e. J ( x e. z -> x e. U. ( y i^i ~P z ) ) ) <-> E. y e. ~P J ( y ~<_ _om /\ A. z e. J ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) )
18 17 ralbii 
 |-  ( A. x e. X E. y e. ~P J ( y ~<_ _om /\ A. z e. J ( x e. z -> x e. U. ( y i^i ~P z ) ) ) <-> A. x e. X E. y e. ~P J ( y ~<_ _om /\ A. z e. J ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) )
19 18 anbi2i 
 |-  ( ( J e. Top /\ A. x e. X E. y e. ~P J ( y ~<_ _om /\ A. z e. J ( x e. z -> x e. U. ( y i^i ~P z ) ) ) ) <-> ( J e. Top /\ A. x e. X E. y e. ~P J ( y ~<_ _om /\ A. z e. J ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) ) )
20 2 19 bitri 
 |-  ( J e. 1stc <-> ( J e. Top /\ A. x e. X E. y e. ~P J ( y ~<_ _om /\ A. z e. J ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) ) )