Description: The property of an n-locally A topological space. (Contributed by Mario Carneiro, 2-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | nllyi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isnlly | |
|
2 | 1 | simprbi | |
3 | pweq | |
|
4 | 3 | ineq2d | |
5 | 4 | rexeqdv | |
6 | 5 | raleqbi1dv | |
7 | 6 | rspccva | |
8 | 2 7 | sylan | |
9 | elin | |
|
10 | sneq | |
|
11 | 10 | fveq2d | |
12 | 11 | eleq2d | |
13 | velpw | |
|
14 | 13 | a1i | |
15 | 12 14 | anbi12d | |
16 | 9 15 | syl5bb | |
17 | 16 | anbi1d | |
18 | anass | |
|
19 | 17 18 | bitrdi | |
20 | 19 | rexbidv2 | |
21 | 20 | rspccva | |
22 | 8 21 | stoic3 | |