This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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