nllyss

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

		Ref	Expression
	Assertion	nllyss	$⊢ A \subseteq B \to N-LocallyA\subseteqN-LocallyB$

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

Metamath Proof Explorer