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

Metamath Proof Explorer

Theorem 1stcclb

Description: A property of points in a first-countable topology. (Contributed by Jeff Hankins, 22-Aug-2009)

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

Proof

Step Hyp Ref Expression
1 1stcclb.1 
 |-  X = U. J
2 1 is1stc2 
 |-  ( J e. 1stc <-> ( J e. Top /\ A. w e. X E. x e. ~P J ( x ~<_ _om /\ A. y e. J ( w e. y -> E. z e. x ( w e. z /\ z C_ y ) ) ) ) )
3 2 simprbi 
 |-  ( J e. 1stc -> A. w e. X E. x e. ~P J ( x ~<_ _om /\ A. y e. J ( w e. y -> E. z e. x ( w e. z /\ z C_ y ) ) ) )
4 eleq1 
 |-  ( w = A -> ( w e. y <-> A e. y ) )
5 eleq1 
 |-  ( w = A -> ( w e. z <-> A e. z ) )
6 5 anbi1d 
 |-  ( w = A -> ( ( w e. z /\ z C_ y ) <-> ( A e. z /\ z C_ y ) ) )
7 6 rexbidv 
 |-  ( w = A -> ( E. z e. x ( w e. z /\ z C_ y ) <-> E. z e. x ( A e. z /\ z C_ y ) ) )
8 4 7 imbi12d 
 |-  ( w = A -> ( ( w e. y -> E. z e. x ( w e. z /\ z C_ y ) ) <-> ( A e. y -> E. z e. x ( A e. z /\ z C_ y ) ) ) )
9 8 ralbidv 
 |-  ( w = A -> ( A. y e. J ( w e. y -> E. z e. x ( w e. z /\ z C_ y ) ) <-> A. y e. J ( A e. y -> E. z e. x ( A e. z /\ z C_ y ) ) ) )
10 9 anbi2d 
 |-  ( w = A -> ( ( x ~<_ _om /\ A. y e. J ( w e. y -> E. z e. x ( w e. z /\ z C_ y ) ) ) <-> ( x ~<_ _om /\ A. y e. J ( A e. y -> E. z e. x ( A e. z /\ z C_ y ) ) ) ) )
11 10 rexbidv 
 |-  ( w = A -> ( E. x e. ~P J ( x ~<_ _om /\ A. y e. J ( w e. y -> E. z e. x ( w e. z /\ z C_ y ) ) ) <-> E. x e. ~P J ( x ~<_ _om /\ A. y e. J ( A e. y -> E. z e. x ( A e. z /\ z C_ y ) ) ) ) )
12 11 rspcv 
 |-  ( A e. X -> ( A. w e. X E. x e. ~P J ( x ~<_ _om /\ A. y e. J ( w e. y -> E. z e. x ( w e. z /\ z C_ y ) ) ) -> E. x e. ~P J ( x ~<_ _om /\ A. y e. J ( A e. y -> E. z e. x ( A e. z /\ z C_ y ) ) ) ) )
13 3 12 mpan9 
 |-  ( ( J e. 1stc /\ A e. X ) -> E. x e. ~P J ( x ~<_ _om /\ A. y e. J ( A e. y -> E. z e. x ( A e. z /\ z C_ y ) ) ) )