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

Metamath Proof Explorer

Definition df-lly

Detailed syntax breakdown