Theorem llyi

Description: The property of a locally A topological space. (Contributed by Mario Carneiro, 2-Mar-2015)

	Ref	Expression
Assertion	llyi	|- ( ( J e. Locally A /\ U e. J /\ P e. U ) -> E. u e. J ( u C_ U /\ P e. u /\ ( J |`t u ) e. A ) )

Proof

Step	Hyp	Ref	Expression
1		islly	|- ( J e. 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 ) ) )
2	1	simprbi	|- ( J e. Locally A -> A. x e. J A. y e. x E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) e. A ) )
3		pweq	|- ( x = U -> ~P x = ~P U )
4	3	ineq2d	|- ( x = U -> ( J i^i ~P x ) = ( J i^i ~P U ) )
5	4	rexeqdv	|- ( x = U -> ( E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) e. A ) <-> E. u e. ( J i^i ~P U ) ( y e. u /\ ( J |`t u ) e. A ) ) )
6	5	raleqbi1dv	|- ( x = U -> ( A. y e. x E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) e. A ) <-> A. y e. U E. u e. ( J i^i ~P U ) ( y e. u /\ ( J |`t u ) e. A ) ) )
7	6	rspccva	|- ( ( A. x e. J A. y e. x E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) e. A ) /\ U e. J ) -> A. y e. U E. u e. ( J i^i ~P U ) ( y e. u /\ ( J |`t u ) e. A ) )
8	2 7	sylan	|- ( ( J e. Locally A /\ U e. J ) -> A. y e. U E. u e. ( J i^i ~P U ) ( y e. u /\ ( J |`t u ) e. A ) )
9		eleq1	|- ( y = P -> ( y e. u <-> P e. u ) )
10	9	anbi1d	|- ( y = P -> ( ( y e. u /\ ( J |`t u ) e. A ) <-> ( P e. u /\ ( J |`t u ) e. A ) ) )
11	10	anbi2d	|- ( y = P -> ( ( u e. ( J i^i ~P U ) /\ ( y e. u /\ ( J |`t u ) e. A ) ) <-> ( u e. ( J i^i ~P U ) /\ ( P e. u /\ ( J |`t u ) e. A ) ) ) )
12		anass	|- ( ( ( u e. J /\ u C_ U ) /\ ( P e. u /\ ( J |`t u ) e. A ) ) <-> ( u e. J /\ ( u C_ U /\ ( P e. u /\ ( J |`t u ) e. A ) ) ) )
13		elin	|- ( u e. ( J i^i ~P U ) <-> ( u e. J /\ u e. ~P U ) )
14		velpw	|- ( u e. ~P U <-> u C_ U )
15	14	anbi2i	|- ( ( u e. J /\ u e. ~P U ) <-> ( u e. J /\ u C_ U ) )
16	13 15	bitri	|- ( u e. ( J i^i ~P U ) <-> ( u e. J /\ u C_ U ) )
17	16	anbi1i	|- ( ( u e. ( J i^i ~P U ) /\ ( P e. u /\ ( J |`t u ) e. A ) ) <-> ( ( u e. J /\ u C_ U ) /\ ( P e. u /\ ( J |`t u ) e. A ) ) )
18		3anass	|- ( ( u C_ U /\ P e. u /\ ( J |`t u ) e. A ) <-> ( u C_ U /\ ( P e. u /\ ( J |`t u ) e. A ) ) )
19	18	anbi2i	|- ( ( u e. J /\ ( u C_ U /\ P e. u /\ ( J |`t u ) e. A ) ) <-> ( u e. J /\ ( u C_ U /\ ( P e. u /\ ( J |`t u ) e. A ) ) ) )
20	12 17 19	3bitr4i	|- ( ( u e. ( J i^i ~P U ) /\ ( P e. u /\ ( J |`t u ) e. A ) ) <-> ( u e. J /\ ( u C_ U /\ P e. u /\ ( J |`t u ) e. A ) ) )
21	11 20	bitrdi	|- ( y = P -> ( ( u e. ( J i^i ~P U ) /\ ( y e. u /\ ( J |`t u ) e. A ) ) <-> ( u e. J /\ ( u C_ U /\ P e. u /\ ( J |`t u ) e. A ) ) ) )
22	21	rexbidv2	|- ( y = P -> ( E. u e. ( J i^i ~P U ) ( y e. u /\ ( J |`t u ) e. A ) <-> E. u e. J ( u C_ U /\ P e. u /\ ( J |`t u ) e. A ) ) )
23	22	rspccva	|- ( ( A. y e. U E. u e. ( J i^i ~P U ) ( y e. u /\ ( J |`t u ) e. A ) /\ P e. U ) -> E. u e. J ( u C_ U /\ P e. u /\ ( J |`t u ) e. A ) )
24	8 23	stoic3	|- ( ( J e. Locally A /\ U e. J /\ P e. U ) -> E. u e. J ( u C_ U /\ P e. u /\ ( J |`t u ) e. A ) )