Definition df-lly 21269

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 sub-neighborhood that is A in the subspace topology. (Contributed by Mario Carneiro, 2-Mar-2015.)

Assertion

Ref	Expression
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 ) }

Distinct variable group:   u, j, x, y, A

Detailed syntax breakdown of Definition df-lly

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	clly 21267	. 2 class Locally A
3		vy	. . . . . . . 8 setvar y
4		vu	. . . . . . . 8 setvar u
5	3, 4	wel 1991	. . . . . . 7 wff y e. u
6		vj	. . . . . . . . . 10 setvar j
7	6	cv 1482	. . . . . . . . 9 class j
8	4	cv 1482	. . . . . . . . 9 class u
9		crest 16081	. . . . . . . . 9 class ↾t
10	7, 8, 9	co 6650	. . . . . . . 8 class ( j ↾t u )
11	10, 1	wcel 1990	. . . . . . 7 wff ( j ↾t u ) e. A
12	5, 11	wa 384	. . . . . 6 wff ( y e. u /\ ( j ↾t u ) e. A )
13		vx	. . . . . . . . 9 setvar x
14	13	cv 1482	. . . . . . . 8 class x
15	14	cpw 4158	. . . . . . 7 class ~P x
16	7, 15	cin 3573	. . . . . 6 class ( j i^i ~P x )
17	12, 4, 16	wrex 2913	. . . . 5 wff E. u e. ( j i^i ~P x ) ( y e. u /\ ( j ↾t u ) e. A )
18	17, 3, 14	wral 2912	. . . 4 wff A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j ↾t u ) e. A )
19	18, 13, 7	wral 2912	. . 3 wff A. x e. j A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j ↾t u ) e. A )
20		ctop 20698	. . 3 class Top
21	19, 6, 20	crab 2916	. 2 class { 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	2, 21	wceq 1483	1 wff 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 ) }

This definition is referenced by:  islly  21271  llyeq  21273