Metamath Proof Explorer


Theorem restlly

Description: If the property A passes to open subspaces, then a space which is A is also locally A . (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Hypotheses restlly.1 ( ( 𝜑 ∧ ( 𝑗𝐴𝑥𝑗 ) ) → ( 𝑗t 𝑥 ) ∈ 𝐴 )
restlly.2 ( 𝜑𝐴 ⊆ Top )
Assertion restlly ( 𝜑𝐴 ⊆ Locally 𝐴 )

Proof

Step Hyp Ref Expression
1 restlly.1 ( ( 𝜑 ∧ ( 𝑗𝐴𝑥𝑗 ) ) → ( 𝑗t 𝑥 ) ∈ 𝐴 )
2 restlly.2 ( 𝜑𝐴 ⊆ Top )
3 2 sselda ( ( 𝜑𝑗𝐴 ) → 𝑗 ∈ Top )
4 simprl ( ( ( 𝜑𝑗𝐴 ) ∧ ( 𝑥𝑗𝑦𝑥 ) ) → 𝑥𝑗 )
5 vex 𝑥 ∈ V
6 5 pwid 𝑥 ∈ 𝒫 𝑥
7 6 a1i ( ( ( 𝜑𝑗𝐴 ) ∧ ( 𝑥𝑗𝑦𝑥 ) ) → 𝑥 ∈ 𝒫 𝑥 )
8 4 7 elind ( ( ( 𝜑𝑗𝐴 ) ∧ ( 𝑥𝑗𝑦𝑥 ) ) → 𝑥 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) )
9 simprr ( ( ( 𝜑𝑗𝐴 ) ∧ ( 𝑥𝑗𝑦𝑥 ) ) → 𝑦𝑥 )
10 1 anassrs ( ( ( 𝜑𝑗𝐴 ) ∧ 𝑥𝑗 ) → ( 𝑗t 𝑥 ) ∈ 𝐴 )
11 10 adantrr ( ( ( 𝜑𝑗𝐴 ) ∧ ( 𝑥𝑗𝑦𝑥 ) ) → ( 𝑗t 𝑥 ) ∈ 𝐴 )
12 elequ2 ( 𝑢 = 𝑥 → ( 𝑦𝑢𝑦𝑥 ) )
13 oveq2 ( 𝑢 = 𝑥 → ( 𝑗t 𝑢 ) = ( 𝑗t 𝑥 ) )
14 13 eleq1d ( 𝑢 = 𝑥 → ( ( 𝑗t 𝑢 ) ∈ 𝐴 ↔ ( 𝑗t 𝑥 ) ∈ 𝐴 ) )
15 12 14 anbi12d ( 𝑢 = 𝑥 → ( ( 𝑦𝑢 ∧ ( 𝑗t 𝑢 ) ∈ 𝐴 ) ↔ ( 𝑦𝑥 ∧ ( 𝑗t 𝑥 ) ∈ 𝐴 ) ) )
16 15 rspcev ( ( 𝑥 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ∧ ( 𝑦𝑥 ∧ ( 𝑗t 𝑥 ) ∈ 𝐴 ) ) → ∃ 𝑢 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ( 𝑦𝑢 ∧ ( 𝑗t 𝑢 ) ∈ 𝐴 ) )
17 8 9 11 16 syl12anc ( ( ( 𝜑𝑗𝐴 ) ∧ ( 𝑥𝑗𝑦𝑥 ) ) → ∃ 𝑢 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ( 𝑦𝑢 ∧ ( 𝑗t 𝑢 ) ∈ 𝐴 ) )
18 17 ralrimivva ( ( 𝜑𝑗𝐴 ) → ∀ 𝑥𝑗𝑦𝑥𝑢 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ( 𝑦𝑢 ∧ ( 𝑗t 𝑢 ) ∈ 𝐴 ) )
19 islly ( 𝑗 ∈ Locally 𝐴 ↔ ( 𝑗 ∈ Top ∧ ∀ 𝑥𝑗𝑦𝑥𝑢 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ( 𝑦𝑢 ∧ ( 𝑗t 𝑢 ) ∈ 𝐴 ) ) )
20 3 18 19 sylanbrc ( ( 𝜑𝑗𝐴 ) → 𝑗 ∈ Locally 𝐴 )
21 20 ex ( 𝜑 → ( 𝑗𝐴𝑗 ∈ Locally 𝐴 ) )
22 21 ssrdv ( 𝜑𝐴 ⊆ Locally 𝐴 )