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 ) ) ) )