Theorem 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	$$⊢\left(\phi \wedge \left(j\in A\wedge x\in j\right)\right)\to j{\upharpoonright }_{𝑡}x\in A$$
	restlly.2	$$⊢\phi \to A\subseteq \mathrm{Top}$$
Assertion	restlly

Proof

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