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 Locally A U J P U u J u U P u J 𝑡 u A

Proof

Step Hyp Ref Expression
1 islly J Locally A J Top x J y x u J 𝒫 x y u J 𝑡 u A
2 1 simprbi J Locally A x J y x u J 𝒫 x y u J 𝑡 u A
3 pweq x = U 𝒫 x = 𝒫 U
4 3 ineq2d x = U J 𝒫 x = J 𝒫 U
5 4 rexeqdv x = U u J 𝒫 x y u J 𝑡 u A u J 𝒫 U y u J 𝑡 u A
6 5 raleqbi1dv x = U y x u J 𝒫 x y u J 𝑡 u A y U u J 𝒫 U y u J 𝑡 u A
7 6 rspccva x J y x u J 𝒫 x y u J 𝑡 u A U J y U u J 𝒫 U y u J 𝑡 u A
8 2 7 sylan J Locally A U J y U u J 𝒫 U y u J 𝑡 u A
9 eleq1 y = P y u P u
10 9 anbi1d y = P y u J 𝑡 u A P u J 𝑡 u A
11 10 anbi2d y = P u J 𝒫 U y u J 𝑡 u A u J 𝒫 U P u J 𝑡 u A
12 anass u J u U P u J 𝑡 u A u J u U P u J 𝑡 u A
13 elin u J 𝒫 U u J u 𝒫 U
14 velpw u 𝒫 U u U
15 14 anbi2i u J u 𝒫 U u J u U
16 13 15 bitri u J 𝒫 U u J u U
17 16 anbi1i u J 𝒫 U P u J 𝑡 u A u J u U P u J 𝑡 u A
18 3anass u U P u J 𝑡 u A u U P u J 𝑡 u A
19 18 anbi2i u J u U P u J 𝑡 u A u J u U P u J 𝑡 u A
20 12 17 19 3bitr4i u J 𝒫 U P u J 𝑡 u A u J u U P u J 𝑡 u A
21 11 20 bitrdi y = P u J 𝒫 U y u J 𝑡 u A u J u U P u J 𝑡 u A
22 21 rexbidv2 y = P u J 𝒫 U y u J 𝑡 u A u J u U P u J 𝑡 u A
23 22 rspccva y U u J 𝒫 U y u J 𝑡 u A P U u J u U P u J 𝑡 u A
24 8 23 stoic3 J Locally A U J P U u J u U P u J 𝑡 u A