restlly

Description: If the property A passes to open subspaces, then a space which is A is also locally A . (Contributed by Mario Carneiro, 2-Mar-2015)

	Ref	Expression
Hypotheses	restlly.1	$⊢ (φ \land (j \in A \land x \in j)) \to j ↾_{𝑡} x \in A$
	restlly.2	$⊢ φ \to A \subseteq Top$
Assertion	restlly	$⊢ φ \to A \subseteq LocallyA$

Proof

Step	Hyp	Ref	Expression
1		restlly.1	$⊢ (φ \land (j \in A \land x \in j)) \to j ↾_{𝑡} x \in A$
2		restlly.2	$⊢ φ \to A \subseteq Top$
3	2	sselda	$⊢ (φ \land j \in A) \to j \in Top$
4		simprl	$⊢ ((φ \land j \in A) \land (x \in j \land y \in x)) \to x \in j$
5		vex	$⊢ x \in V$
6	5	pwid	$⊢ x \in 𝒫 x$
7	6	a1i	$⊢ ((φ \land j \in A) \land (x \in j \land y \in x)) \to x \in 𝒫 x$
8	4 7	elind	$⊢ ((φ \land j \in A) \land (x \in j \land y \in x)) \to x \in (j \cap 𝒫 x)$
9		simprr	$⊢ ((φ \land j \in A) \land (x \in j \land y \in x)) \to y \in x$
10	1	anassrs	$⊢ ((φ \land j \in A) \land x \in j) \to j ↾_{𝑡} x \in A$
11	10	adantrr	$⊢ ((φ \land j \in A) \land (x \in j \land y \in x)) \to j ↾_{𝑡} x \in A$
12		elequ2	$⊢ u = x \to (y \in u \leftrightarrow y \in x)$
13		oveq2	$⊢ u = x \to j ↾_{𝑡} u = j ↾_{𝑡} x$
14	13	eleq1d	$⊢ u = x \to (j ↾_{𝑡} u \in A \leftrightarrow j ↾_{𝑡} x \in A)$
15	12 14	anbi12d	$⊢ u = x \to ((y \in u \land j ↾_{𝑡} u \in A) \leftrightarrow (y \in x \land j ↾_{𝑡} x \in A))$
16	15	rspcev	$⊢ (x \in (j \cap 𝒫 x) \land (y \in x \land j ↾_{𝑡} x \in A)) \to \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in A)$
17	8 9 11 16	syl12anc	$⊢ ((φ \land j \in A) \land (x \in j \land y \in x)) \to \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in A)$
18	17	ralrimivva	$⊢ (φ \land j \in A) \to \forall x \in j \forall y \in x \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in A)$
19		islly	$⊢ j \in LocallyA\leftrightarrow(j \in Top \land \forall x \in j)$
20	3 18 19	sylanbrc	$⊢ (φ \land j \in A) \to j \in LocallyA$
21	20	ex	$⊢ φ \to (j \in A \to j \in LocallyA)$
22	21	ssrdv	$⊢ φ \to A \subseteq LocallyA$

Metamath Proof Explorer

Theorem restlly

Proof