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