This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐴 )