Metamath Proof Explorer

Theorem llyss

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

Ref Expression
Assertion llyss ⊢ A ⊆ B → Locally A ⊆ Locally B

Proof

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