Metamath Proof Explorer

Theorem llynlly

Description: A locally A space is n-locally A : the "n-locally" predicate is the weaker notion. (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Assertion llynlly 
|- ( J e. Locally A -> J e. N-Locally A )

Proof

Step Hyp Ref Expression
1 llytop 
 |-  ( J e. Locally A -> J e. Top )
2 llyi 
 |-  ( ( J e. Locally A /\ x e. J /\ y e. x ) -> E. u e. J ( u C_ x /\ y e. u /\ ( J |`t u ) e. A ) )
3 simpl1 
 |-  ( ( ( J e. Locally A /\ x e. J /\ y e. x ) /\ ( u e. J /\ ( u C_ x /\ y e. u /\ ( J |`t u ) e. A ) ) ) -> J e. Locally A )
4 3 1 syl 
 |-  ( ( ( J e. Locally A /\ x e. J /\ y e. x ) /\ ( u e. J /\ ( u C_ x /\ y e. u /\ ( J |`t u ) e. A ) ) ) -> J e. Top )
5 simprl 
 |-  ( ( ( J e. Locally A /\ x e. J /\ y e. x ) /\ ( u e. J /\ ( u C_ x /\ y e. u /\ ( J |`t u ) e. A ) ) ) -> u e. J )
6 simprr2 
 |-  ( ( ( J e. Locally A /\ x e. J /\ y e. x ) /\ ( u e. J /\ ( u C_ x /\ y e. u /\ ( J |`t u ) e. A ) ) ) -> y e. u )
7 opnneip 
 |-  ( ( J e. Top /\ u e. J /\ y e. u ) -> u e. ( ( nei ` J ) ` { y } ) )
8 4 5 6 7 syl3anc 
 |-  ( ( ( J e. Locally A /\ x e. J /\ y e. x ) /\ ( u e. J /\ ( u C_ x /\ y e. u /\ ( J |`t u ) e. A ) ) ) -> u e. ( ( nei ` J ) ` { y } ) )
9 simprr1 
 |-  ( ( ( J e. Locally A /\ x e. J /\ y e. x ) /\ ( u e. J /\ ( u C_ x /\ y e. u /\ ( J |`t u ) e. A ) ) ) -> u C_ x )
10 velpw 
 |-  ( u e. ~P x <-> u C_ x )
11 9 10 sylibr 
 |-  ( ( ( J e. Locally A /\ x e. J /\ y e. x ) /\ ( u e. J /\ ( u C_ x /\ y e. u /\ ( J |`t u ) e. A ) ) ) -> u e. ~P x )
12 8 11 elind 
 |-  ( ( ( J e. Locally A /\ x e. J /\ y e. x ) /\ ( u e. J /\ ( u C_ x /\ y e. u /\ ( J |`t u ) e. A ) ) ) -> u e. ( ( ( nei ` J ) ` { y } ) i^i ~P x ) )
13 simprr3 
 |-  ( ( ( J e. Locally A /\ x e. J /\ y e. x ) /\ ( u e. J /\ ( u C_ x /\ y e. u /\ ( J |`t u ) e. A ) ) ) -> ( J |`t u ) e. A )
14 2 12 13 reximssdv 
 |-  ( ( J e. Locally A /\ x e. J /\ y e. x ) -> E. u e. ( ( ( nei ` J ) ` { y } ) i^i ~P x ) ( J |`t u ) e. A )
15 14 3expb 
 |-  ( ( J e. Locally A /\ ( x e. J /\ y e. x ) ) -> E. u e. ( ( ( nei ` J ) ` { y } ) i^i ~P x ) ( J |`t u ) e. A )
16 15 ralrimivva 
 |-  ( J e. Locally A -> A. x e. J A. y e. x E. u e. ( ( ( nei ` J ) ` { y } ) i^i ~P x ) ( J |`t u ) e. A )
17 isnlly 
 |-  ( J e. N-Locally A <-> ( J e. Top /\ A. x e. J A. y e. x E. u e. ( ( ( nei ` J ) ` { y } ) i^i ~P x ) ( J |`t u ) e. A ) )
18 1 16 17 sylanbrc 
 |-  ( J e. Locally A -> J e. N-Locally A )