Metamath Proof Explorer

Theorem llyss

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

		Ref	Expression
	Assertion	llyss	$⊢ A \subseteq B \to LocallyA\subseteqLocallyB$

Proof

Step	Hyp	Ref	Expression
1		ssel	$⊢ A \subseteq B \to (j ↾_{𝑡} u \in A \to j ↾_{𝑡} u \in B)$
2	1	anim2d	$⊢ A \subseteq B \to ((y \in u \land j ↾_{𝑡} u \in A) \to (y \in u \land j ↾_{𝑡} u \in B))$
3	2	reximdv	$⊢ A \subseteq B \to (\exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in A) \to \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in B))$
4	3	ralimdv	$⊢ A \subseteq B \to (\forall y \in x \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in A) \to \forall y \in x \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in B))$
5	4	ralimdv	$⊢ A \subseteq B \to (\forall x \in j \forall y \in x \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in A) \to \forall x \in j \forall y \in x \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in B))$
6	5	anim2d	$⊢ A \subseteq B \to ((j \in Top \land \forall x \in j \forall y \in x \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in A)) \to (j \in Top \land \forall x \in j \forall y \in x \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in B)))$
7		islly	$⊢ j \in LocallyA\leftrightarrow(j \in Top \land \forall x \in j \forall y \in x \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in A))$
8		islly	$⊢ j \in LocallyB\leftrightarrow(j \in Top \land \forall x \in j \forall y \in x \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in B))$
9	6 7 8	3imtr4g	$⊢ A \subseteq B \to (j \in LocallyA\toj \in LocallyB)$
10	9	ssrdv	$⊢ A \subseteq B \to LocallyA\subseteqLocallyB$