Definition df-lly

Description: Define a space that is locally A , where A is a topological property like "compact", "connected", or "path-connected". A topological space is locally A if every neighborhood of a point contains an open subneighborhood that is A in the subspace topology. (Contributed by Mario Carneiro, 2-Mar-2015)

	Ref	Expression
Assertion	df-lly	|- Locally A = { j e. Top | A. x e. j A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1	0	clly	|- Locally A
2		vj	|- j
3		ctop	|- Top
4		vx	|- x
5	2	cv	|- j
6		vy	|- y
7	4	cv	|- x
8		vu	|- u
9	7	cpw	|- ~P x
10	5 9	cin	|- ( j i^i ~P x )
11	6	cv	|- y
12	8	cv	|- u
13	11 12	wcel	|- y e. u
14		crest	|- |`t
15	5 12 14	co	|- ( j |`t u )
16	15 0	wcel	|- ( j |`t u ) e. A
17	13 16	wa	|- ( y e. u /\ ( j |`t u ) e. A )
18	17 8 10	wrex	|- E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A )
19	18 6 7	wral	|- A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A )
20	19 4 5	wral	|- A. x e. j A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A )
21	20 2 3	crab	|- { j e. Top | A. x e. j A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A ) }
22	1 21	wceq	|- Locally A = { j e. Top | A. x e. j A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A ) }