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	|- ( ( ph /\ ( j e. A /\ x e. j ) ) -> ( j |`t x ) e. A )
	restlly.2	|- ( ph -> A C_ Top )
Assertion	restlly	|- ( ph -> A C_ Locally A )

Proof

Step	Hyp	Ref	Expression
1		restlly.1	|- ( ( ph /\ ( j e. A /\ x e. j ) ) -> ( j |`t x ) e. A )
2		restlly.2	|- ( ph -> A C_ Top )
3	2	sselda	|- ( ( ph /\ j e. A ) -> j e. Top )
4		simprl	|- ( ( ( ph /\ j e. A ) /\ ( x e. j /\ y e. x ) ) -> x e. j )
5		vex	|- x e. _V
6	5	pwid	|- x e. ~P x
7	6	a1i	|- ( ( ( ph /\ j e. A ) /\ ( x e. j /\ y e. x ) ) -> x e. ~P x )
8	4 7	elind	|- ( ( ( ph /\ j e. A ) /\ ( x e. j /\ y e. x ) ) -> x e. ( j i^i ~P x ) )
9		simprr	|- ( ( ( ph /\ j e. A ) /\ ( x e. j /\ y e. x ) ) -> y e. x )
10	1	anassrs	|- ( ( ( ph /\ j e. A ) /\ x e. j ) -> ( j |`t x ) e. A )
11	10	adantrr	|- ( ( ( ph /\ j e. A ) /\ ( x e. j /\ y e. x ) ) -> ( j |`t x ) e. A )
12		elequ2	|- ( u = x -> ( y e. u <-> y e. x ) )
13		oveq2	|- ( u = x -> ( j |`t u ) = ( j |`t x ) )
14	13	eleq1d	|- ( u = x -> ( ( j |`t u ) e. A <-> ( j |`t x ) e. A ) )
15	12 14	anbi12d	|- ( u = x -> ( ( y e. u /\ ( j |`t u ) e. A ) <-> ( y e. x /\ ( j |`t x ) e. A ) ) )
16	15	rspcev	|- ( ( x e. ( j i^i ~P x ) /\ ( y e. x /\ ( j |`t x ) e. A ) ) -> E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A ) )
17	8 9 11 16	syl12anc	|- ( ( ( ph /\ j e. A ) /\ ( x e. j /\ y e. x ) ) -> E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A ) )
18	17	ralrimivva	|- ( ( ph /\ j e. A ) -> A. x e. j A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A ) )
19		islly	|- ( j e. Locally A <-> ( j e. Top /\ A. x e. j A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A ) ) )
20	3 18 19	sylanbrc	|- ( ( ph /\ j e. A ) -> j e. Locally A )
21	20	ex	|- ( ph -> ( j e. A -> j e. Locally A ) )
22	21	ssrdv	|- ( ph -> A C_ Locally A )