Metamath Proof Explorer


Theorem islly

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

Ref Expression
Assertion islly JLocally A JTopxJyxuJ𝒫xyuJ𝑡uA

Proof

Step Hyp Ref Expression
1 ineq1 j=Jj𝒫x=J𝒫x
2 oveq1 j=Jj𝑡u=J𝑡u
3 2 eleq1d j=Jj𝑡uAJ𝑡uA
4 3 anbi2d j=Jyuj𝑡uAyuJ𝑡uA
5 1 4 rexeqbidv j=Juj𝒫xyuj𝑡uAuJ𝒫xyuJ𝑡uA
6 5 ralbidv j=Jyxuj𝒫xyuj𝑡uAyxuJ𝒫xyuJ𝑡uA
7 6 raleqbi1dv j=Jxjyxuj𝒫xyuj𝑡uAxJyxuJ𝒫xyuJ𝑡uA
8 df-lly Locally A = jTop|xjyxuj𝒫xyuj𝑡uA
9 7 8 elrab2 JLocally A JTopxJyxuJ𝒫xyuJ𝑡uA