Theorem nllyss

Description: The "n-locally" predicate respects inclusion. (Contributed by Mario Carneiro, 2-Mar-2015)

	Ref	Expression
Assertion	nllyss	⊢ ( 𝐴 ⊆ 𝐵 → 𝑛-Locally 𝐴 ⊆ 𝑛-Locally 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ssel	⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 → ( 𝑗 ↾t 𝑢 ) ∈ 𝐵 ) )
2	1	reximdv	⊢ ( 𝐴 ⊆ 𝐵 → ( ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 → ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐵 ) )
3	2	ralimdv	⊢ ( 𝐴 ⊆ 𝐵 → ( ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 → ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐵 ) )
4	3	ralimdv	⊢ ( 𝐴 ⊆ 𝐵 → ( ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 → ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐵 ) )
5	4	anim2d	⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑗 ∈ Top ∧ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ) → ( 𝑗 ∈ Top ∧ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐵 ) ) )
6		isnlly	⊢ ( 𝑗 ∈ 𝑛-Locally 𝐴 ↔ ( 𝑗 ∈ Top ∧ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ) )
7		isnlly	⊢ ( 𝑗 ∈ 𝑛-Locally 𝐵 ↔ ( 𝑗 ∈ Top ∧ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐵 ) )
8	5 6 7	3imtr4g	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑗 ∈ 𝑛-Locally 𝐴 → 𝑗 ∈ 𝑛-Locally 𝐵 ) )
9	8	ssrdv	⊢ ( 𝐴 ⊆ 𝐵 → 𝑛-Locally 𝐴 ⊆ 𝑛-Locally 𝐵 )