Theorem islly2 20576

Description: An alternative expression for J e. Locally A when A passes to open subspaces: A space is locally A if every point is contained in an open neighborhood with property A. (Contributed by Mario Carneiro, 2-Mar-2015.)

Hypotheses

Ref	Expression
restlly.1	|- ( ( ph /\ ( j e. A /\ x e. j ) ) -> ( j ↾t x ) e. A )
islly2.2	|- X = U. J

Assertion

Ref	Expression
islly2	|- ( ph -> ( J e. Locally A <-> ( J e. Top /\ A. y e. X E. u e. J ( y e. u /\ ( J ↾t u ) e. A ) ) ) )

Distinct variable groups:   u, j, x, y, A   j, J, u, x, y   ph, j, u, x, y   u, X, y

Allowed substitution hints:   X( x, j)

Proof of Theorem islly2

Dummy variables v z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		llytop 20564	. . . 4 |- ( J e. Locally A -> J e. Top )
2	1	adantl 473	. . 3 |- ( ( ph /\ J e. Locally A ) -> J e. Top )
3		simplr 770	. . . . . 6 |- ( ( ( ph /\ J e. Locally A ) /\ y e. X ) -> J e. Locally A )
4	2	adantr 472	. . . . . . 7 |- ( ( ( ph /\ J e. Locally A ) /\ y e. X ) -> J e. Top )
5		islly2.2	. . . . . . . 8 |- X = U. J
6	5	topopn 20013	. . . . . . 7 |- ( J e. Top -> X e. J )
7	4, 6	syl 17	. . . . . 6 |- ( ( ( ph /\ J e. Locally A ) /\ y e. X ) -> X e. J )
8		simpr 468	. . . . . 6 |- ( ( ( ph /\ J e. Locally A ) /\ y e. X ) -> y e. X )
9		llyi 20566	. . . . . 6 |- ( ( J e. Locally A /\ X e. J /\ y e. X ) -> E. u e. J ( u C_ X /\ y e. u /\ ( J ↾t u ) e. A ) )
10	3, 7, 8, 9	syl3anc 1292	. . . . 5 |- ( ( ( ph /\ J e. Locally A ) /\ y e. X ) -> E. u e. J ( u C_ X /\ y e. u /\ ( J ↾t u ) e. A ) )
11		3simpc 1029	. . . . . 6 |- ( ( u C_ X /\ y e. u /\ ( J ↾t u ) e. A ) -> ( y e. u /\ ( J ↾t u ) e. A ) )
12	11	reximi 2852	. . . . 5 |- ( E. u e. J ( u C_ X /\ y e. u /\ ( J ↾t u ) e. A ) -> E. u e. J ( y e. u /\ ( J ↾t u ) e. A ) )
13	10, 12	syl 17	. . . 4 |- ( ( ( ph /\ J e. Locally A ) /\ y e. X ) -> E. u e. J ( y e. u /\ ( J ↾t u ) e. A ) )
14	13	ralrimiva 2809	. . 3 |- ( ( ph /\ J e. Locally A ) -> A. y e. X E. u e. J ( y e. u /\ ( J ↾t u ) e. A ) )
15	2, 14	jca 541	. 2 |- ( ( ph /\ J e. Locally A ) -> ( J e. Top /\ A. y e. X E. u e. J ( y e. u /\ ( J ↾t u ) e. A ) ) )
16		simprl 772	. . 3 |- ( ( ph /\ ( J e. Top /\ A. y e. X E. u e. J ( y e. u /\ ( J ↾t u ) e. A ) ) ) -> J e. Top )
17		elssuni 4219	. . . . . . . . 9 |- ( z e. J -> z C_ U. J )
18	17, 5	syl6sseqr 3465	. . . . . . . 8 |- ( z e. J -> z C_ X )
19	18	adantl 473	. . . . . . 7 |- ( ( ( ph /\ J e. Top ) /\ z e. J ) -> z C_ X )
20		ssralv 3479	. . . . . . 7 |- ( z C_ X -> ( A. y e. X E. u e. J ( y e. u /\ ( J ↾t u ) e. A ) -> A. y e. z E. u e. J ( y e. u /\ ( J ↾t u ) e. A ) ) )
21	19, 20	syl 17	. . . . . 6 |- ( ( ( ph /\ J e. Top ) /\ z e. J ) -> ( A. y e. X E. u e. J ( y e. u /\ ( J ↾t u ) e. A ) -> A. y e. z E. u e. J ( y e. u /\ ( J ↾t u ) e. A ) ) )
22		simpllr 777	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J ↾t u ) e. A ) ) ) -> J e. Top )
23		simplrl 778	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J ↾t u ) e. A ) ) ) -> z e. J )
24		simprl 772	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J ↾t u ) e. A ) ) ) -> u e. J )
25		inopn 20006	. . . . . . . . . . . 12 |- ( ( J e. Top /\ z e. J /\ u e. J ) -> ( z i^i u ) e. J )
26	22, 23, 24, 25	syl3anc 1292	. . . . . . . . . . 11 |- ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J ↾t u ) e. A ) ) ) -> ( z i^i u ) e. J )
27		inss1 3643	. . . . . . . . . . . . 13 |- ( z i^i u ) C_ z
28		vex 3034	. . . . . . . . . . . . . 14 |- z e. _V
29	28	elpw2 4565	. . . . . . . . . . . . 13 |- ( ( z i^i u ) e. ~P z <-> ( z i^i u ) C_ z )
30	27, 29	mpbir 214	. . . . . . . . . . . 12 |- ( z i^i u ) e. ~P z
31	30	a1i 11	. . . . . . . . . . 11 |- ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J ↾t u ) e. A ) ) ) -> ( z i^i u ) e. ~P z )
32	26, 31	elind 3609	. . . . . . . . . 10 |- ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J ↾t u ) e. A ) ) ) -> ( z i^i u ) e. ( J i^i ~P z ) )
33		simplrr 779	. . . . . . . . . . 11 |- ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J ↾t u ) e. A ) ) ) -> y e. z )
34		simprrl 782	. . . . . . . . . . 11 |- ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J ↾t u ) e. A ) ) ) -> y e. u )
35	33, 34	elind 3609	. . . . . . . . . 10 |- ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J ↾t u ) e. A ) ) ) -> y e. ( z i^i u ) )
36		inss2 3644	. . . . . . . . . . . . 13 |- ( z i^i u ) C_ u
37	36	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J ↾t u ) e. A ) ) ) -> ( z i^i u ) C_ u )
38		restabs 20258	. . . . . . . . . . . 12 |- ( ( J e. Top /\ ( z i^i u ) C_ u /\ u e. J ) -> ( ( J ↾t u ) ↾t ( z i^i u ) ) = ( J ↾t ( z i^i u ) ) )
39	22, 37, 24, 38	syl3anc 1292	. . . . . . . . . . 11 |- ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J ↾t u ) e. A ) ) ) -> ( ( J ↾t u ) ↾t ( z i^i u ) ) = ( J ↾t ( z i^i u ) ) )
40		elrestr 15405	. . . . . . . . . . . . 13 |- ( ( J e. Top /\ u e. J /\ z e. J ) -> ( z i^i u ) e. ( J ↾t u ) )
41	22, 24, 23, 40	syl3anc 1292	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J ↾t u ) e. A ) ) ) -> ( z i^i u ) e. ( J ↾t u ) )
42		simprrr 783	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J ↾t u ) e. A ) ) ) -> ( J ↾t u ) e. A )
43		restlly.1	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( j e. A /\ x e. j ) ) -> ( j ↾t x ) e. A )
44	43	ralrimivva 2814	. . . . . . . . . . . . . 14 |- ( ph -> A. j e. A A. x e. j ( j ↾t x ) e. A )
45	44	ad3antrrr 744	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J ↾t u ) e. A ) ) ) -> A. j e. A A. x e. j ( j ↾t x ) e. A )
46		oveq1 6315	. . . . . . . . . . . . . . . 16 |- ( j = ( J ↾t u ) -> ( j ↾t x ) = ( ( J ↾t u ) ↾t x ) )
47	46	eleq1d 2533	. . . . . . . . . . . . . . 15 |- ( j = ( J ↾t u ) -> ( ( j ↾t x ) e. A <-> ( ( J ↾t u ) ↾t x ) e. A ) )
48	47	raleqbi1dv 2981	. . . . . . . . . . . . . 14 |- ( j = ( J ↾t u ) -> ( A. x e. j ( j ↾t x ) e. A <-> A. x e. ( J ↾t u ) ( ( J ↾t u ) ↾t x ) e. A ) )
49	48	rspcv 3132	. . . . . . . . . . . . 13 |- ( ( J ↾t u ) e. A -> ( A. j e. A A. x e. j ( j ↾t x ) e. A -> A. x e. ( J ↾t u ) ( ( J ↾t u ) ↾t x ) e. A ) )
50	42, 45, 49	sylc 61	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J ↾t u ) e. A ) ) ) -> A. x e. ( J ↾t u ) ( ( J ↾t u ) ↾t x ) e. A )
51		oveq2 6316	. . . . . . . . . . . . . 14 |- ( x = ( z i^i u ) -> ( ( J ↾t u ) ↾t x ) = ( ( J ↾t u ) ↾t ( z i^i u ) ) )
52	51	eleq1d 2533	. . . . . . . . . . . . 13 |- ( x = ( z i^i u ) -> ( ( ( J ↾t u ) ↾t x ) e. A <-> ( ( J ↾t u ) ↾t ( z i^i u ) ) e. A ) )
53	52	rspcv 3132	. . . . . . . . . . . 12 |- ( ( z i^i u ) e. ( J ↾t u ) -> ( A. x e. ( J ↾t u ) ( ( J ↾t u ) ↾t x ) e. A -> ( ( J ↾t u ) ↾t ( z i^i u ) ) e. A ) )
54	41, 50, 53	sylc 61	. . . . . . . . . . 11 |- ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J ↾t u ) e. A ) ) ) -> ( ( J ↾t u ) ↾t ( z i^i u ) ) e. A )
55	39, 54	eqeltrrd 2550	. . . . . . . . . 10 |- ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J ↾t u ) e. A ) ) ) -> ( J ↾t ( z i^i u ) ) e. A )
56		eleq2 2538	. . . . . . . . . . . 12 |- ( v = ( z i^i u ) -> ( y e. v <-> y e. ( z i^i u ) ) )
57		oveq2 6316	. . . . . . . . . . . . 13 |- ( v = ( z i^i u ) -> ( J ↾t v ) = ( J ↾t ( z i^i u ) ) )
58	57	eleq1d 2533	. . . . . . . . . . . 12 |- ( v = ( z i^i u ) -> ( ( J ↾t v ) e. A <-> ( J ↾t ( z i^i u ) ) e. A ) )
59	56, 58	anbi12d 725	. . . . . . . . . . 11 |- ( v = ( z i^i u ) -> ( ( y e. v /\ ( J ↾t v ) e. A ) <-> ( y e. ( z i^i u ) /\ ( J ↾t ( z i^i u ) ) e. A ) ) )
60	59	rspcev 3136	. . . . . . . . . 10 |- ( ( ( z i^i u ) e. ( J i^i ~P z ) /\ ( y e. ( z i^i u ) /\ ( J ↾t ( z i^i u ) ) e. A ) ) -> E. v e. ( J i^i ~P z ) ( y e. v /\ ( J ↾t v ) e. A ) )
61	32, 35, 55, 60	syl12anc 1290	. . . . . . . . 9 |- ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J ↾t u ) e. A ) ) ) -> E. v e. ( J i^i ~P z ) ( y e. v /\ ( J ↾t v ) e. A ) )
62	61	rexlimdvaa 2872	. . . . . . . 8 |- ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) -> ( E. u e. J ( y e. u /\ ( J ↾t u ) e. A ) -> E. v e. ( J i^i ~P z ) ( y e. v /\ ( J ↾t v ) e. A ) ) )
63	62	anassrs 660	. . . . . . 7 |- ( ( ( ( ph /\ J e. Top ) /\ z e. J ) /\ y e. z ) -> ( E. u e. J ( y e. u /\ ( J ↾t u ) e. A ) -> E. v e. ( J i^i ~P z ) ( y e. v /\ ( J ↾t v ) e. A ) ) )
64	63	ralimdva 2805	. . . . . 6 |- ( ( ( ph /\ J e. Top ) /\ z e. J ) -> ( A. y e. z E. u e. J ( y e. u /\ ( J ↾t u ) e. A ) -> A. y e. z E. v e. ( J i^i ~P z ) ( y e. v /\ ( J ↾t v ) e. A ) ) )
65	21, 64	syld 44	. . . . 5 |- ( ( ( ph /\ J e. Top ) /\ z e. J ) -> ( A. y e. X E. u e. J ( y e. u /\ ( J ↾t u ) e. A ) -> A. y e. z E. v e. ( J i^i ~P z ) ( y e. v /\ ( J ↾t v ) e. A ) ) )
66	65	ralrimdva 2812	. . . 4 |- ( ( ph /\ J e. Top ) -> ( A. y e. X E. u e. J ( y e. u /\ ( J ↾t u ) e. A ) -> A. z e. J A. y e. z E. v e. ( J i^i ~P z ) ( y e. v /\ ( J ↾t v ) e. A ) ) )
67	66	impr 631	. . 3 |- ( ( ph /\ ( J e. Top /\ A. y e. X E. u e. J ( y e. u /\ ( J ↾t u ) e. A ) ) ) -> A. z e. J A. y e. z E. v e. ( J i^i ~P z ) ( y e. v /\ ( J ↾t v ) e. A ) )
68		islly 20560	. . 3 |- ( J e. Locally A <-> ( J e. Top /\ A. z e. J A. y e. z E. v e. ( J i^i ~P z ) ( y e. v /\ ( J ↾t v ) e. A ) ) )
69	16, 67, 68	sylanbrc 677	. 2 |- ( ( ph /\ ( J e. Top /\ A. y e. X E. u e. J ( y e. u /\ ( J ↾t u ) e. A ) ) ) -> J e. Locally A )
70	15, 69	impbida 850	1 |- ( ph -> ( J e. Locally A <-> ( J e. Top /\ A. y e. X E. u e. J ( y e. u /\ ( J ↾t u ) e. A ) ) ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 376   /\ w3a 1007   = wceq 1452   e. wcel 1904   A.wral 2756   E.wrex 2757   i^i cin 3389   C_ wss 3390   ~Pcpw 3942   U.cuni 4190  (class class class)co 6308   ↾_t crest 15397   Topctop 19994  Locally clly 20556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pr 4639  ax-un 6602

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-rest 15399  df-top 19998  df-lly 20558

This theorem is referenced by: (None)