Metamath Proof Explorer


Theorem nllyi

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

Ref Expression
Assertion nllyi JN-Locally A UJ PU uneiJPuUJ𝑡uA

Proof

Step Hyp Ref Expression
1 isnlly JN-Locally A JTopxJyxuneiJy𝒫xJ𝑡uA
2 1 simprbi JN-Locally A xJyxuneiJy𝒫xJ𝑡uA
3 pweq x=U𝒫x=𝒫U
4 3 ineq2d x=UneiJy𝒫x=neiJy𝒫U
5 4 rexeqdv x=UuneiJy𝒫xJ𝑡uAuneiJy𝒫UJ𝑡uA
6 5 raleqbi1dv x=UyxuneiJy𝒫xJ𝑡uAyUuneiJy𝒫UJ𝑡uA
7 6 rspccva xJyxuneiJy𝒫xJ𝑡uAUJyUuneiJy𝒫UJ𝑡uA
8 2 7 sylan JN-Locally A UJ yUuneiJy𝒫UJ𝑡uA
9 elin uneiJy𝒫UuneiJyu𝒫U
10 sneq y=Py=P
11 10 fveq2d y=PneiJy=neiJP
12 11 eleq2d y=PuneiJyuneiJP
13 velpw u𝒫UuU
14 13 a1i y=Pu𝒫UuU
15 12 14 anbi12d y=PuneiJyu𝒫UuneiJPuU
16 9 15 syl5bb y=PuneiJy𝒫UuneiJPuU
17 16 anbi1d y=PuneiJy𝒫UJ𝑡uAuneiJPuUJ𝑡uA
18 anass uneiJPuUJ𝑡uAuneiJPuUJ𝑡uA
19 17 18 bitrdi y=PuneiJy𝒫UJ𝑡uAuneiJPuUJ𝑡uA
20 19 rexbidv2 y=PuneiJy𝒫UJ𝑡uAuneiJPuUJ𝑡uA
21 20 rspccva yUuneiJy𝒫UJ𝑡uAPUuneiJPuUJ𝑡uA
22 8 21 stoic3 JN-Locally A UJ PU uneiJPuUJ𝑡uA