Metamath Proof Explorer

Theorem islly2

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)

Ref Expression
Hypotheses restlly.1 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑥 ∈ 𝑗 ) ) → ( 𝑗 ↾t 𝑥 ) ∈ 𝐴 )
islly2.2 ⊢ 𝑋 = ∪ 𝐽
Assertion islly2 ( 𝜑 → ( 𝐽 ∈ Locally 𝐴 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝑋 ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 restlly.1 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑥 ∈ 𝑗 ) ) → ( 𝑗 ↾t 𝑥 ) ∈ 𝐴 )
2 islly2.2 ⊢ 𝑋 = ∪ 𝐽
3 llytop ⊢ ( 𝐽 ∈ Locally 𝐴 → 𝐽 ∈ Top )
4 3 adantl ⊢ ( ( 𝜑 ∧ 𝐽 ∈ Locally 𝐴 ) → 𝐽 ∈ Top )
5 simplr ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ Locally 𝐴 ) ∧ 𝑦 ∈ 𝑋 ) → 𝐽 ∈ Locally 𝐴 )
6 4 adantr ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ Locally 𝐴 ) ∧ 𝑦 ∈ 𝑋 ) → 𝐽 ∈ Top )
7 2 topopn ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
8 6 7 syl ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ Locally 𝐴 ) ∧ 𝑦 ∈ 𝑋 ) → 𝑋 ∈ 𝐽 )
9 simpr ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ Locally 𝐴 ) ∧ 𝑦 ∈ 𝑋 ) → 𝑦 ∈ 𝑋 )
10 llyi ⊢ ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑋 ∈ 𝐽 ∧ 𝑦 ∈ 𝑋 ) → ∃ 𝑢 ∈ 𝐽 ( 𝑢 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )
11 5 8 9 10 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ Locally 𝐴 ) ∧ 𝑦 ∈ 𝑋 ) → ∃ 𝑢 ∈ 𝐽 ( 𝑢 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )
12 3simpc ⊢ ( ( 𝑢 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) → ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )
13 12 reximi ⊢ ( ∃ 𝑢 ∈ 𝐽 ( 𝑢 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) → ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )
14 11 13 syl ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ Locally 𝐴 ) ∧ 𝑦 ∈ 𝑋 ) → ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )
15 14 ralrimiva ⊢ ( ( 𝜑 ∧ 𝐽 ∈ Locally 𝐴 ) → ∀ 𝑦 ∈ 𝑋 ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )
16 4 15 jca ⊢ ( ( 𝜑 ∧ 𝐽 ∈ Locally 𝐴 ) → ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝑋 ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) )
17 simprl ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝑋 ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → 𝐽 ∈ Top )
18 elssuni ⊢ ( 𝑧 ∈ 𝐽 → 𝑧 ⊆ ∪ 𝐽 )
19 18 2 sseqtrrdi ⊢ ( 𝑧 ∈ 𝐽 → 𝑧 ⊆ 𝑋 )
20 19 adantl ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑧 ∈ 𝐽 ) → 𝑧 ⊆ 𝑋 )
21 ssralv ⊢ ( 𝑧 ⊆ 𝑋 → ( ∀ 𝑦 ∈ 𝑋 ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) → ∀ 𝑦 ∈ 𝑧 ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) )
22 20 21 syl ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑧 ∈ 𝐽 ) → ( ∀ 𝑦 ∈ 𝑋 ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) → ∀ 𝑦 ∈ 𝑧 ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) )
23 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → 𝐽 ∈ Top )
24 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → 𝑧 ∈ 𝐽 )
25 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → 𝑢 ∈ 𝐽 )
26 inopn ⊢ ( ( 𝐽 ∈ Top ∧ 𝑧 ∈ 𝐽 ∧ 𝑢 ∈ 𝐽 ) → ( 𝑧 ∩ 𝑢 ) ∈ 𝐽 )
27 23 24 25 26 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → ( 𝑧 ∩ 𝑢 ) ∈ 𝐽 )
28 vex ⊢ 𝑧 ∈ V
29 inss1 ⊢ ( 𝑧 ∩ 𝑢 ) ⊆ 𝑧
30 28 29 elpwi2 ⊢ ( 𝑧 ∩ 𝑢 ) ∈ 𝒫 𝑧
31 30 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → ( 𝑧 ∩ 𝑢 ) ∈ 𝒫 𝑧 )
32 27 31 elind ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → ( 𝑧 ∩ 𝑢 ) ∈ ( 𝐽 ∩ 𝒫 𝑧 ) )
33 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → 𝑦 ∈ 𝑧 )
34 simprrl ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → 𝑦 ∈ 𝑢 )
35 33 34 elind ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → 𝑦 ∈ ( 𝑧 ∩ 𝑢 ) )
36 inss2 ⊢ ( 𝑧 ∩ 𝑢 ) ⊆ 𝑢
37 36 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → ( 𝑧 ∩ 𝑢 ) ⊆ 𝑢 )
38 restabs ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑧 ∩ 𝑢 ) ⊆ 𝑢 ∧ 𝑢 ∈ 𝐽 ) → ( ( 𝐽 ↾t 𝑢 ) ↾t ( 𝑧 ∩ 𝑢 ) ) = ( 𝐽 ↾t ( 𝑧 ∩ 𝑢 ) ) )
39 23 37 25 38 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → ( ( 𝐽 ↾t 𝑢 ) ↾t ( 𝑧 ∩ 𝑢 ) ) = ( 𝐽 ↾t ( 𝑧 ∩ 𝑢 ) ) )
40 oveq2 ⊢ ( 𝑥 = ( 𝑧 ∩ 𝑢 ) → ( ( 𝐽 ↾t 𝑢 ) ↾t 𝑥 ) = ( ( 𝐽 ↾t 𝑢 ) ↾t ( 𝑧 ∩ 𝑢 ) ) )
41 40 eleq1d ⊢ ( 𝑥 = ( 𝑧 ∩ 𝑢 ) → ( ( ( 𝐽 ↾t 𝑢 ) ↾t 𝑥 ) ∈ 𝐴 ↔ ( ( 𝐽 ↾t 𝑢 ) ↾t ( 𝑧 ∩ 𝑢 ) ) ∈ 𝐴 ) )
42 oveq1 ⊢ ( 𝑗 = ( 𝐽 ↾t 𝑢 ) → ( 𝑗 ↾t 𝑥 ) = ( ( 𝐽 ↾t 𝑢 ) ↾t 𝑥 ) )
43 42 eleq1d ⊢ ( 𝑗 = ( 𝐽 ↾t 𝑢 ) → ( ( 𝑗 ↾t 𝑥 ) ∈ 𝐴 ↔ ( ( 𝐽 ↾t 𝑢 ) ↾t 𝑥 ) ∈ 𝐴 ) )
44 43 raleqbi1dv ⊢ ( 𝑗 = ( 𝐽 ↾t 𝑢 ) → ( ∀ 𝑥 ∈ 𝑗 ( 𝑗 ↾t 𝑥 ) ∈ 𝐴 ↔ ∀ 𝑥 ∈ ( 𝐽 ↾t 𝑢 ) ( ( 𝐽 ↾t 𝑢 ) ↾t 𝑥 ) ∈ 𝐴 ) )
45 1 ralrimivva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝐴 ∀ 𝑥 ∈ 𝑗 ( 𝑗 ↾t 𝑥 ) ∈ 𝐴 )
46 45 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → ∀ 𝑗 ∈ 𝐴 ∀ 𝑥 ∈ 𝑗 ( 𝑗 ↾t 𝑥 ) ∈ 𝐴 )
47 simprrr ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 )
48 44 46 47 rspcdva ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → ∀ 𝑥 ∈ ( 𝐽 ↾t 𝑢 ) ( ( 𝐽 ↾t 𝑢 ) ↾t 𝑥 ) ∈ 𝐴 )
49 elrestr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝐽 ) → ( 𝑧 ∩ 𝑢 ) ∈ ( 𝐽 ↾t 𝑢 ) )
50 23 25 24 49 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → ( 𝑧 ∩ 𝑢 ) ∈ ( 𝐽 ↾t 𝑢 ) )
51 41 48 50 rspcdva ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → ( ( 𝐽 ↾t 𝑢 ) ↾t ( 𝑧 ∩ 𝑢 ) ) ∈ 𝐴 )
52 39 51 eqeltrrd ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → ( 𝐽 ↾t ( 𝑧 ∩ 𝑢 ) ) ∈ 𝐴 )
53 eleq2 ⊢ ( 𝑣 = ( 𝑧 ∩ 𝑢 ) → ( 𝑦 ∈ 𝑣 ↔ 𝑦 ∈ ( 𝑧 ∩ 𝑢 ) ) )
54 oveq2 ⊢ ( 𝑣 = ( 𝑧 ∩ 𝑢 ) → ( 𝐽 ↾t 𝑣 ) = ( 𝐽 ↾t ( 𝑧 ∩ 𝑢 ) ) )
55 54 eleq1d ⊢ ( 𝑣 = ( 𝑧 ∩ 𝑢 ) → ( ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ↔ ( 𝐽 ↾t ( 𝑧 ∩ 𝑢 ) ) ∈ 𝐴 ) )
56 53 55 anbi12d ⊢ ( 𝑣 = ( 𝑧 ∩ 𝑢 ) → ( ( 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) ↔ ( 𝑦 ∈ ( 𝑧 ∩ 𝑢 ) ∧ ( 𝐽 ↾t ( 𝑧 ∩ 𝑢 ) ) ∈ 𝐴 ) ) )
57 56 rspcev ⊢ ( ( ( 𝑧 ∩ 𝑢 ) ∈ ( 𝐽 ∩ 𝒫 𝑧 ) ∧ ( 𝑦 ∈ ( 𝑧 ∩ 𝑢 ) ∧ ( 𝐽 ↾t ( 𝑧 ∩ 𝑢 ) ) ∈ 𝐴 ) ) → ∃ 𝑣 ∈ ( 𝐽 ∩ 𝒫 𝑧 ) ( 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) )
58 32 35 52 57 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → ∃ 𝑣 ∈ ( 𝐽 ∩ 𝒫 𝑧 ) ( 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) )
59 58 rexlimdvaa ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → ( ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) → ∃ 𝑣 ∈ ( 𝐽 ∩ 𝒫 𝑧 ) ( 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) ) )
60 59 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑧 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑧 ) → ( ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) → ∃ 𝑣 ∈ ( 𝐽 ∩ 𝒫 𝑧 ) ( 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) ) )
61 60 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑧 ∈ 𝐽 ) → ( ∀ 𝑦 ∈ 𝑧 ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) → ∀ 𝑦 ∈ 𝑧 ∃ 𝑣 ∈ ( 𝐽 ∩ 𝒫 𝑧 ) ( 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) ) )
62 22 61 syld ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑧 ∈ 𝐽 ) → ( ∀ 𝑦 ∈ 𝑋 ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) → ∀ 𝑦 ∈ 𝑧 ∃ 𝑣 ∈ ( 𝐽 ∩ 𝒫 𝑧 ) ( 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) ) )
63 62 ralrimdva ⊢ ( ( 𝜑 ∧ 𝐽 ∈ Top ) → ( ∀ 𝑦 ∈ 𝑋 ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) → ∀ 𝑧 ∈ 𝐽 ∀ 𝑦 ∈ 𝑧 ∃ 𝑣 ∈ ( 𝐽 ∩ 𝒫 𝑧 ) ( 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) ) )
64 63 impr ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝑋 ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → ∀ 𝑧 ∈ 𝐽 ∀ 𝑦 ∈ 𝑧 ∃ 𝑣 ∈ ( 𝐽 ∩ 𝒫 𝑧 ) ( 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) )
65 islly ⊢ ( 𝐽 ∈ Locally 𝐴 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑧 ∈ 𝐽 ∀ 𝑦 ∈ 𝑧 ∃ 𝑣 ∈ ( 𝐽 ∩ 𝒫 𝑧 ) ( 𝑦 ∈ 𝑣 ∧ ( 𝐽 ↾t 𝑣 ) ∈ 𝐴 ) ) )
66 17 64 65 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝑋 ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → 𝐽 ∈ Locally 𝐴 )
67 16 66 impbida ⊢ ( 𝜑 → ( 𝐽 ∈ Locally 𝐴 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝑋 ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) )