Metamath Proof Explorer

Theorem nllyss

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

Ref Expression
Assertion nllyss ⊢ A ⊆ B → N-Locally A ⊆ N-Locally B

Proof

Step Hyp Ref Expression
1 ssel ⊢ A ⊆ B → j ↾ 𝑡 u ∈ A → j ↾ 𝑡 u ∈ B
2 1 reximdv ⊢ A ⊆ B → ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ A → ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ B
3 2 ralimdv ⊢ A ⊆ B → ∀ y ∈ x ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ A → ∀ y ∈ x ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ B
4 3 ralimdv ⊢ A ⊆ B → ∀ x ∈ j ∀ y ∈ x ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ A → ∀ x ∈ j ∀ y ∈ x ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ B
5 4 anim2d ⊢ A ⊆ B → j ∈ Top ∧ ∀ x ∈ j ∀ y ∈ x ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ A → j ∈ Top ∧ ∀ x ∈ j ∀ y ∈ x ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ B
6 isnlly ⊢ j ∈ N-Locally A ↔ j ∈ Top ∧ ∀ x ∈ j ∀ y ∈ x ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ A
7 isnlly ⊢ j ∈ N-Locally B ↔ j ∈ Top ∧ ∀ x ∈ j ∀ y ∈ x ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ B
8 5 6 7 3imtr4g ⊢ A ⊆ B → j ∈ N-Locally A → j ∈ N-Locally B
9 8 ssrdv ⊢ A ⊆ B → N-Locally A ⊆ N-Locally B