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

Metamath Proof Explorer

Theorem llyss

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

Ref Expression
Assertion llyss ( 𝐴 ⊆ 𝐵 → Locally 𝐴 ⊆ Locally 𝐵 )

Proof

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