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