Metamath Proof Explorer

Theorem nllyidm

Description: Idempotence of the "n-locally" predicate, i.e. being "n-locally A " is a local property. (Use loclly to show N-Locally N-Locally A = N-Locally A .) (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Assertion nllyidm Locally 𝑛-Locally 𝐴 = 𝑛-Locally 𝐴

Proof

Step Hyp Ref Expression
1 llytop ⊢ ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 → 𝑗 ∈ Top )
2 llyi ⊢ ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑢 ∈ 𝑗 ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) )
3 simprr3 ⊢ ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) → ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 )
4 simprl ⊢ ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) → 𝑢 ∈ 𝑗 )
5 ssidd ⊢ ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) → 𝑢 ⊆ 𝑢 )
6 simpl1 ⊢ ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) → 𝑗 ∈ Locally 𝑛-Locally 𝐴 )
7 6 1 syl ⊢ ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) → 𝑗 ∈ Top )
8 restopn2 ⊢ ( ( 𝑗 ∈ Top ∧ 𝑢 ∈ 𝑗 ) → ( 𝑢 ∈ ( 𝑗 ↾t 𝑢 ) ↔ ( 𝑢 ∈ 𝑗 ∧ 𝑢 ⊆ 𝑢 ) ) )
9 7 4 8 syl2anc ⊢ ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) → ( 𝑢 ∈ ( 𝑗 ↾t 𝑢 ) ↔ ( 𝑢 ∈ 𝑗 ∧ 𝑢 ⊆ 𝑢 ) ) )
10 4 5 9 mpbir2and ⊢ ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) → 𝑢 ∈ ( 𝑗 ↾t 𝑢 ) )
11 simprr2 ⊢ ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) → 𝑦 ∈ 𝑢 )
12 nlly2i ⊢ ( ( ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ∧ 𝑢 ∈ ( 𝑗 ↾t 𝑢 ) ∧ 𝑦 ∈ 𝑢 ) → ∃ 𝑣 ∈ 𝒫 𝑢 ∃ 𝑧 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) )
13 3 10 11 12 syl3anc ⊢ ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) → ∃ 𝑣 ∈ 𝒫 𝑢 ∃ 𝑧 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) )
14 restopn2 ⊢ ( ( 𝑗 ∈ Top ∧ 𝑢 ∈ 𝑗 ) → ( 𝑧 ∈ ( 𝑗 ↾t 𝑢 ) ↔ ( 𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢 ) ) )
15 7 4 14 syl2anc ⊢ ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) → ( 𝑧 ∈ ( 𝑗 ↾t 𝑢 ) ↔ ( 𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢 ) ) )
16 15 adantr ⊢ ( ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) ∧ 𝑣 ∈ 𝒫 𝑢 ) → ( 𝑧 ∈ ( 𝑗 ↾t 𝑢 ) ↔ ( 𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢 ) ) )
17 7 adantr ⊢ ( ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝒫 𝑢 ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑗 ∈ Top )
18 simpr2l ⊢ ( ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝒫 𝑢 ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑧 ∈ 𝑗 )
19 simpr31 ⊢ ( ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝒫 𝑢 ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑦 ∈ 𝑧 )
20 opnneip ⊢ ( ( 𝑗 ∈ Top ∧ 𝑧 ∈ 𝑗 ∧ 𝑦 ∈ 𝑧 ) → 𝑧 ∈ ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) )
21 17 18 19 20 syl3anc ⊢ ( ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝒫 𝑢 ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑧 ∈ ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) )
22 simpr32 ⊢ ( ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝒫 𝑢 ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑧 ⊆ 𝑣 )
23 simpr1 ⊢ ( ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝒫 𝑢 ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑣 ∈ 𝒫 𝑢 )
24 23 elpwid ⊢ ( ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝒫 𝑢 ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑣 ⊆ 𝑢 )
25 4 adantr ⊢ ( ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝒫 𝑢 ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑢 ∈ 𝑗 )
26 elssuni ⊢ ( 𝑢 ∈ 𝑗 → 𝑢 ⊆ ∪ 𝑗 )
27 25 26 syl ⊢ ( ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝒫 𝑢 ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑢 ⊆ ∪ 𝑗 )
28 24 27 sstrd ⊢ ( ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝒫 𝑢 ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑣 ⊆ ∪ 𝑗 )
29 eqid ⊢ ∪ 𝑗 = ∪ 𝑗
30 29 ssnei2 ⊢ ( ( ( 𝑗 ∈ Top ∧ 𝑧 ∈ ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ) ∧ ( 𝑧 ⊆ 𝑣 ∧ 𝑣 ⊆ ∪ 𝑗 ) ) → 𝑣 ∈ ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) )
31 17 21 22 28 30 syl22anc ⊢ ( ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝒫 𝑢 ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑣 ∈ ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) )
32 simprr1 ⊢ ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) → 𝑢 ⊆ 𝑥 )
33 32 adantr ⊢ ( ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝒫 𝑢 ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑢 ⊆ 𝑥 )
34 24 33 sstrd ⊢ ( ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝒫 𝑢 ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑣 ⊆ 𝑥 )
35 velpw ⊢ ( 𝑣 ∈ 𝒫 𝑥 ↔ 𝑣 ⊆ 𝑥 )
36 34 35 sylibr ⊢ ( ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝒫 𝑢 ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑣 ∈ 𝒫 𝑥 )
37 31 36 elind ⊢ ( ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝒫 𝑢 ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑣 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) )
38 restabs ⊢ ( ( 𝑗 ∈ Top ∧ 𝑣 ⊆ 𝑢 ∧ 𝑢 ∈ 𝑗 ) → ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) = ( 𝑗 ↾t 𝑣 ) )
39 17 24 25 38 syl3anc ⊢ ( ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝒫 𝑢 ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) = ( 𝑗 ↾t 𝑣 ) )
40 simpr33 ⊢ ( ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝒫 𝑢 ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 )
41 39 40 eqeltrrd ⊢ ( ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝒫 𝑢 ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → ( 𝑗 ↾t 𝑣 ) ∈ 𝐴 )
42 37 41 jca ⊢ ( ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝒫 𝑢 ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → ( 𝑣 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ∧ ( 𝑗 ↾t 𝑣 ) ∈ 𝐴 ) )
43 42 3exp2 ⊢ ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) → ( 𝑣 ∈ 𝒫 𝑢 → ( ( 𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢 ) → ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) → ( 𝑣 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ∧ ( 𝑗 ↾t 𝑣 ) ∈ 𝐴 ) ) ) ) )
44 43 imp ⊢ ( ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) ∧ 𝑣 ∈ 𝒫 𝑢 ) → ( ( 𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢 ) → ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) → ( 𝑣 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ∧ ( 𝑗 ↾t 𝑣 ) ∈ 𝐴 ) ) ) )
45 16 44 sylbid ⊢ ( ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) ∧ 𝑣 ∈ 𝒫 𝑢 ) → ( 𝑧 ∈ ( 𝑗 ↾t 𝑢 ) → ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) → ( 𝑣 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ∧ ( 𝑗 ↾t 𝑣 ) ∈ 𝐴 ) ) ) )
46 45 rexlimdv ⊢ ( ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) ∧ 𝑣 ∈ 𝒫 𝑢 ) → ( ∃ 𝑧 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) → ( 𝑣 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ∧ ( 𝑗 ↾t 𝑣 ) ∈ 𝐴 ) ) )
47 46 expimpd ⊢ ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) → ( ( 𝑣 ∈ 𝒫 𝑢 ∧ ∃ 𝑧 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) → ( 𝑣 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ∧ ( 𝑗 ↾t 𝑣 ) ∈ 𝐴 ) ) )
48 47 reximdv2 ⊢ ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) → ( ∃ 𝑣 ∈ 𝒫 𝑢 ∃ 𝑧 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) → ∃ 𝑣 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑣 ) ∈ 𝐴 ) )
49 13 48 mpd ⊢ ( ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝑛-Locally 𝐴 ) ) ) → ∃ 𝑣 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑣 ) ∈ 𝐴 )
50 2 49 rexlimddv ⊢ ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑣 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑣 ) ∈ 𝐴 )
51 50 3expb ⊢ ( ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 ∧ ( 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ) → ∃ 𝑣 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑣 ) ∈ 𝐴 )
52 51 ralrimivva ⊢ ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 → ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑣 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑣 ) ∈ 𝐴 )
53 isnlly ⊢ ( 𝑗 ∈ 𝑛-Locally 𝐴 ↔ ( 𝑗 ∈ Top ∧ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑣 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑣 ) ∈ 𝐴 ) )
54 1 52 53 sylanbrc ⊢ ( 𝑗 ∈ Locally 𝑛-Locally 𝐴 → 𝑗 ∈ 𝑛-Locally 𝐴 )
55 54 ssriv ⊢ Locally 𝑛-Locally 𝐴 ⊆ 𝑛-Locally 𝐴
56 nllyrest ⊢ ( ( 𝑗 ∈ 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ) → ( 𝑗 ↾t 𝑥 ) ∈ 𝑛-Locally 𝐴 )
57 56 adantl ⊢ ( ( ⊤ ∧ ( 𝑗 ∈ 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ) ) → ( 𝑗 ↾t 𝑥 ) ∈ 𝑛-Locally 𝐴 )
58 nllytop ⊢ ( 𝑗 ∈ 𝑛-Locally 𝐴 → 𝑗 ∈ Top )
59 58 ssriv ⊢ 𝑛-Locally 𝐴 ⊆ Top
60 59 a1i ⊢ ( ⊤ → 𝑛-Locally 𝐴 ⊆ Top )
61 57 60 restlly ⊢ ( ⊤ → 𝑛-Locally 𝐴 ⊆ Locally 𝑛-Locally 𝐴 )
62 61 mptru ⊢ 𝑛-Locally 𝐴 ⊆ Locally 𝑛-Locally 𝐴
63 55 62 eqssi ⊢ Locally 𝑛-Locally 𝐴 = 𝑛-Locally 𝐴