This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝑢 ∩ 𝐵 ) ) ∈ 𝐴 ) ) )