Theorem subislly

Description: The property of a subspace being locally A . (Contributed by Mario Carneiro, 10-Mar-2015)

	Ref	Expression
Assertion	subislly	⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐽 ↾t 𝐵 ) ∈ Locally 𝐴 ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ∃ 𝑢 ∈ 𝐽 ( ( 𝑢 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t ( 𝑢 ∩ 𝐵 ) ) ∈ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		resttop	⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐵 ) ∈ Top )
2		islly	⊢ ( ( 𝐽 ↾t 𝐵 ) ∈ Locally 𝐴 ↔ ( ( 𝐽 ↾t 𝐵 ) ∈ Top ∧ ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐵 ) ∀ 𝑦 ∈ 𝑧 ∃ 𝑤 ∈ ( ( 𝐽 ↾t 𝐵 ) ∩ 𝒫 𝑧 ) ( 𝑦 ∈ 𝑤 ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑤 ) ∈ 𝐴 ) ) )
3	2	baib	⊢ ( ( 𝐽 ↾t 𝐵 ) ∈ Top → ( ( 𝐽 ↾t 𝐵 ) ∈ Locally 𝐴 ↔ ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐵 ) ∀ 𝑦 ∈ 𝑧 ∃ 𝑤 ∈ ( ( 𝐽 ↾t 𝐵 ) ∩ 𝒫 𝑧 ) ( 𝑦 ∈ 𝑤 ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑤 ) ∈ 𝐴 ) ) )
4	1 3	syl	⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐽 ↾t 𝐵 ) ∈ Locally 𝐴 ↔ ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐵 ) ∀ 𝑦 ∈ 𝑧 ∃ 𝑤 ∈ ( ( 𝐽 ↾t 𝐵 ) ∩ 𝒫 𝑧 ) ( 𝑦 ∈ 𝑤 ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑤 ) ∈ 𝐴 ) ) )
5		vex	⊢ 𝑥 ∈ V
6	5	inex1	⊢ ( 𝑥 ∩ 𝐵 ) ∈ V
7	6	a1i	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑥 ∩ 𝐵 ) ∈ V )
8		elrest	⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) → ( 𝑧 ∈ ( 𝐽 ↾t 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐽 𝑧 = ( 𝑥 ∩ 𝐵 ) ) )
9		simpr	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) → 𝑧 = ( 𝑥 ∩ 𝐵 ) )
10	9	raleqdv	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) → ( ∀ 𝑦 ∈ 𝑧 ∃ 𝑤 ∈ ( ( 𝐽 ↾t 𝐵 ) ∩ 𝒫 𝑧 ) ( 𝑦 ∈ 𝑤 ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑤 ) ∈ 𝐴 ) ↔ ∀ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ∃ 𝑤 ∈ ( ( 𝐽 ↾t 𝐵 ) ∩ 𝒫 𝑧 ) ( 𝑦 ∈ 𝑤 ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑤 ) ∈ 𝐴 ) ) )
11		rexin	⊢ ( ∃ 𝑤 ∈ ( ( 𝐽 ↾t 𝐵 ) ∩ 𝒫 𝑧 ) ( 𝑦 ∈ 𝑤 ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑤 ) ∈ 𝐴 ) ↔ ∃ 𝑤 ∈ ( 𝐽 ↾t 𝐵 ) ( 𝑤 ∈ 𝒫 𝑧 ∧ ( 𝑦 ∈ 𝑤 ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑤 ) ∈ 𝐴 ) ) )
12		vex	⊢ 𝑢 ∈ V
13	12	inex1	⊢ ( 𝑢 ∩ 𝐵 ) ∈ V
14	13	a1i	⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐽 ) → ( 𝑢 ∩ 𝐵 ) ∈ V )
15		elrest	⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) → ( 𝑤 ∈ ( 𝐽 ↾t 𝐵 ) ↔ ∃ 𝑢 ∈ 𝐽 𝑤 = ( 𝑢 ∩ 𝐵 ) ) )
16	15	ad2antrr	⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) → ( 𝑤 ∈ ( 𝐽 ↾t 𝐵 ) ↔ ∃ 𝑢 ∈ 𝐽 𝑤 = ( 𝑢 ∩ 𝐵 ) ) )
17		3anass	⊢ ( ( 𝑤 ∈ 𝒫 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑤 ) ∈ 𝐴 ) ↔ ( 𝑤 ∈ 𝒫 𝑧 ∧ ( 𝑦 ∈ 𝑤 ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑤 ) ∈ 𝐴 ) ) )
18		simpr	⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑤 = ( 𝑢 ∩ 𝐵 ) ) → 𝑤 = ( 𝑢 ∩ 𝐵 ) )
19		simpllr	⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑤 = ( 𝑢 ∩ 𝐵 ) ) → 𝑧 = ( 𝑥 ∩ 𝐵 ) )
20	18 19	sseq12d	⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑤 = ( 𝑢 ∩ 𝐵 ) ) → ( 𝑤 ⊆ 𝑧 ↔ ( 𝑢 ∩ 𝐵 ) ⊆ ( 𝑥 ∩ 𝐵 ) ) )
21		velpw	⊢ ( 𝑤 ∈ 𝒫 𝑧 ↔ 𝑤 ⊆ 𝑧 )
22		inss2	⊢ ( 𝑢 ∩ 𝐵 ) ⊆ 𝐵
23	22	biantru	⊢ ( ( 𝑢 ∩ 𝐵 ) ⊆ 𝑥 ↔ ( ( 𝑢 ∩ 𝐵 ) ⊆ 𝑥 ∧ ( 𝑢 ∩ 𝐵 ) ⊆ 𝐵 ) )
24		ssin	⊢ ( ( ( 𝑢 ∩ 𝐵 ) ⊆ 𝑥 ∧ ( 𝑢 ∩ 𝐵 ) ⊆ 𝐵 ) ↔ ( 𝑢 ∩ 𝐵 ) ⊆ ( 𝑥 ∩ 𝐵 ) )
25	23 24	bitri	⊢ ( ( 𝑢 ∩ 𝐵 ) ⊆ 𝑥 ↔ ( 𝑢 ∩ 𝐵 ) ⊆ ( 𝑥 ∩ 𝐵 ) )
26	20 21 25	3bitr4g	⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑤 = ( 𝑢 ∩ 𝐵 ) ) → ( 𝑤 ∈ 𝒫 𝑧 ↔ ( 𝑢 ∩ 𝐵 ) ⊆ 𝑥 ) )
27	18	eleq2d	⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑤 = ( 𝑢 ∩ 𝐵 ) ) → ( 𝑦 ∈ 𝑤 ↔ 𝑦 ∈ ( 𝑢 ∩ 𝐵 ) ) )
28		simplr	⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑤 = ( 𝑢 ∩ 𝐵 ) ) → 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) )
29	28	elin2d	⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑤 = ( 𝑢 ∩ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
30	29	biantrud	⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑤 = ( 𝑢 ∩ 𝐵 ) ) → ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝑢 ∧ 𝑦 ∈ 𝐵 ) ) )
31		elin	⊢ ( 𝑦 ∈ ( 𝑢 ∩ 𝐵 ) ↔ ( 𝑦 ∈ 𝑢 ∧ 𝑦 ∈ 𝐵 ) )
32	30 31	bitr4di	⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑤 = ( 𝑢 ∩ 𝐵 ) ) → ( 𝑦 ∈ 𝑢 ↔ 𝑦 ∈ ( 𝑢 ∩ 𝐵 ) ) )
33	27 32	bitr4d	⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑤 = ( 𝑢 ∩ 𝐵 ) ) → ( 𝑦 ∈ 𝑤 ↔ 𝑦 ∈ 𝑢 ) )
34	18	oveq2d	⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑤 = ( 𝑢 ∩ 𝐵 ) ) → ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑤 ) = ( ( 𝐽 ↾t 𝐵 ) ↾t ( 𝑢 ∩ 𝐵 ) ) )
35		simp-4l	⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑤 = ( 𝑢 ∩ 𝐵 ) ) → 𝐽 ∈ Top )
36	22	a1i	⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑤 = ( 𝑢 ∩ 𝐵 ) ) → ( 𝑢 ∩ 𝐵 ) ⊆ 𝐵 )
37		simplr	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) → 𝐵 ∈ 𝑉 )
38	37	ad2antrr	⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑤 = ( 𝑢 ∩ 𝐵 ) ) → 𝐵 ∈ 𝑉 )
39		restabs	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑢 ∩ 𝐵 ) ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐽 ↾t 𝐵 ) ↾t ( 𝑢 ∩ 𝐵 ) ) = ( 𝐽 ↾t ( 𝑢 ∩ 𝐵 ) ) )
40	35 36 38 39	syl3anc	⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑤 = ( 𝑢 ∩ 𝐵 ) ) → ( ( 𝐽 ↾t 𝐵 ) ↾t ( 𝑢 ∩ 𝐵 ) ) = ( 𝐽 ↾t ( 𝑢 ∩ 𝐵 ) ) )
41	34 40	eqtrd	⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑤 = ( 𝑢 ∩ 𝐵 ) ) → ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑤 ) = ( 𝐽 ↾t ( 𝑢 ∩ 𝐵 ) ) )
42	41	eleq1d	⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑤 = ( 𝑢 ∩ 𝐵 ) ) → ( ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑤 ) ∈ 𝐴 ↔ ( 𝐽 ↾t ( 𝑢 ∩ 𝐵 ) ) ∈ 𝐴 ) )
43	26 33 42	3anbi123d	⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑤 = ( 𝑢 ∩ 𝐵 ) ) → ( ( 𝑤 ∈ 𝒫 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑤 ) ∈ 𝐴 ) ↔ ( ( 𝑢 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t ( 𝑢 ∩ 𝐵 ) ) ∈ 𝐴 ) ) )
44	17 43	bitr3id	⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑤 = ( 𝑢 ∩ 𝐵 ) ) → ( ( 𝑤 ∈ 𝒫 𝑧 ∧ ( 𝑦 ∈ 𝑤 ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑤 ) ∈ 𝐴 ) ) ↔ ( ( 𝑢 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t ( 𝑢 ∩ 𝐵 ) ) ∈ 𝐴 ) ) )
45	14 16 44	rexxfr2d	⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) → ( ∃ 𝑤 ∈ ( 𝐽 ↾t 𝐵 ) ( 𝑤 ∈ 𝒫 𝑧 ∧ ( 𝑦 ∈ 𝑤 ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑤 ) ∈ 𝐴 ) ) ↔ ∃ 𝑢 ∈ 𝐽 ( ( 𝑢 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t ( 𝑢 ∩ 𝐵 ) ) ∈ 𝐴 ) ) )
46	11 45	bitrid	⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) → ( ∃ 𝑤 ∈ ( ( 𝐽 ↾t 𝐵 ) ∩ 𝒫 𝑧 ) ( 𝑦 ∈ 𝑤 ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑤 ) ∈ 𝐴 ) ↔ ∃ 𝑢 ∈ 𝐽 ( ( 𝑢 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t ( 𝑢 ∩ 𝐵 ) ) ∈ 𝐴 ) ) )
47	46	ralbidva	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) → ( ∀ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ∃ 𝑤 ∈ ( ( 𝐽 ↾t 𝐵 ) ∩ 𝒫 𝑧 ) ( 𝑦 ∈ 𝑤 ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑤 ) ∈ 𝐴 ) ↔ ∀ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ∃ 𝑢 ∈ 𝐽 ( ( 𝑢 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t ( 𝑢 ∩ 𝐵 ) ) ∈ 𝐴 ) ) )
48	10 47	bitrd	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑧 = ( 𝑥 ∩ 𝐵 ) ) → ( ∀ 𝑦 ∈ 𝑧 ∃ 𝑤 ∈ ( ( 𝐽 ↾t 𝐵 ) ∩ 𝒫 𝑧 ) ( 𝑦 ∈ 𝑤 ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑤 ) ∈ 𝐴 ) ↔ ∀ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ∃ 𝑢 ∈ 𝐽 ( ( 𝑢 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t ( 𝑢 ∩ 𝐵 ) ) ∈ 𝐴 ) ) )
49	7 8 48	ralxfr2d	⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) → ( ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐵 ) ∀ 𝑦 ∈ 𝑧 ∃ 𝑤 ∈ ( ( 𝐽 ↾t 𝐵 ) ∩ 𝒫 𝑧 ) ( 𝑦 ∈ 𝑤 ∧ ( ( 𝐽 ↾t 𝐵 ) ↾t 𝑤 ) ∈ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ∃ 𝑢 ∈ 𝐽 ( ( 𝑢 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t ( 𝑢 ∩ 𝐵 ) ) ∈ 𝐴 ) ) )
50	4 49	bitrd	⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐽 ↾t 𝐵 ) ∈ Locally 𝐴 ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ∃ 𝑢 ∈ 𝐽 ( ( 𝑢 ∩ 𝐵 ) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t ( 𝑢 ∩ 𝐵 ) ) ∈ 𝐴 ) ) )